CLTT
読むかなぁ
Categorical Logic and Type Theory, Volume 141 (Studies in Logic and the Foundations of Mathematics)
- 作者: B. Jacobs
- 出版社/メーカー: Elsevier Science
- 発売日: 2001/07/01
- メディア: ハードカバー
- 購入: 2人 クリック: 86回
- この商品を含むブログ (12件) を見る
Santa Claus problem
{-# LANGUAGE TypeOperators #-} import Data.List import Data.Pseudo (Pseudo, (:->),randomDelayList,merger,probe,embedPseudo) data Colleague = Elf Int | Reindeer Int deriving (Eq,Show) elf :: Int -> [Colleague] -> [Colleague] elf n (x:xs) = case x of Elf m | n == m -> randomDelayList (Elf n: elf n xs) _ -> elf n xs reindeer :: Int -> [Colleague] -> [Colleague] reindeer n (x:xs) = case x of Reindeer m | n == m -> randomDelayList (Reindeer n: reindeer n xs) _ -> reindeer n xs colleagues :: [Colleague] -> ([Colleague] :-> [Colleague]) colleagues rrs@(r:rs) = merger $ [elf i rrs | i <- [1..10]] ++ [reindeer i rrs| i<-[1..9]] santa :: [Colleague] -> ([[Colleague]] :-> [Colleague]) santa cs@(_:_) = case partition isElf cs of (es,rs) -> concat . map (probe task) . merger [waiting 3 es, waiting 9 rs] where isElf (Elf _) = True isElf _ = False waiting :: Int -> [Colleague] -> [[Colleague]] waiting = splits task :: [Colleague] -> String task cs = concat $ intersperse "\n" $ (greeting ++ msg (head cs)) : map show cs where greeting = "----------\nHo! Ho! Ho! let's " msg (Elf _) = "meet in my study" msg _ = "deliver toys" ini :: [Colleague] ini = [Elf i | i <- [1..10]] ++ [Reindeer i | i <- [1..9]] company :: ([Colleague] -> ([[Colleague]] :-> [Colleague])) -- server -> ([Colleague] -> ([Colleague] :-> [Colleague])) -- client -> (([[Colleague]],[Colleague]) :-> ([Colleague],[Colleague])) -- interaction company santa colleagues oracles = case embedPseudo oracles of (css,cs) -> (comings, returnings) where returnings = santa comings css comings = colleagues (ini++returnings) cs pmain :: ([[Colleague]],[Colleague]) :-> ([Colleague],[Colleague]) pmain = company santa colleagues main :: IO () main = mapM_ return $ snd $ pmain oracle oracle :: Pseudo ([[Colleague]],[Colleague]) oracle = undefined -- Utility splits :: Int -> [a] -> [[a]] splits n = unfoldr phi where phi [] = Nothing phi xs = Just $ splitAt n xs