メモリたくさん欲しいです
http://blog.livedoor.jp/geek/archives/50888709.html
- 作者: 小野田博一
- 出版社/メーカー: イーグルパブリシング
- 発売日: 2009/09/25
- メディア: 単行本（ソフトカバー）
- 購入: 5人 クリック: 172回
- この商品を含むブログ (7件) を見る
アキバblogのPopに1問目が載っていて、これを何とか実行せずして順位を決めたいなーという強い願望の元に次のようなプログラムを書きます。
実行せずだったら、多分GHCiで:typeつかうまでなら大丈夫ですよね・・・とかそういう・・・。
{- 全組合せを作って それを調べる方針 -} {-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE OverlappingInstances #-} import Prelude hiding (Nothing,Maybe) class Force a b | a -> b where getType :: a -> b u = undefined -- -- Nat -- data Zero = Zero data Succ a = Succ a type One = Succ Zero type Two = Succ One type Three = Succ Two type Four = Succ Three type Five = Succ Four instance Force Zero Zero instance (Force a a') => Force (Succ a) (Succ a') data NatEq a b data NatEqProxy a b instance Force (NatEqProxy a a) True instance (Force False false) => Force (NatEqProxy a b) false instance (Force a a',Force b b',Force (NatEqProxy a' b') z) => Force (NatEq a b) z data Less a b instance Force (Less Zero Zero) False instance Force (Less Zero (Succ a)) True instance Force (Less (Succ a) Zero) False instance (Force (Less a b) z) => Force (Less (Succ a) (Succ b)) z data Add a b instance (Force a a',Force b b',Force (TAdd a' b') z) => Force (Add a b) z type family TAdd a b :: * type instance TAdd Zero b = b type instance TAdd (Succ a) b = Succ (Add a b) --- --- List --- data Nil data Cons a b type a :<: b = Cons a b infixr 7 :<: instance Force Nil Nil instance (Force a a',Force b b') => Force (Cons a b) (Cons a' b') data Append a b type TAppend a b = Foldr Cons b a instance (Force (TAppend a b) z) => Force (Append a b) z data Length l type family TLength l :: * type instance TLength Nil = Zero type instance TLength (Cons a b) = Succ (TLength b) instance (Force a a',Force (TLength a') z) => Force (Length a) z data Map (f :: * -> *) l type family TMap (f :: * -> *) l :: * type instance TMap f Nil = Nil type instance TMap f (Cons a b) = Cons (f a) (TMap f b) instance (Force a a',Force (TMap f a') z) => Force (Map f a) z data Filter (f :: * -> *) l type family TFilter (f :: * -> *) l :: * type instance TFilter f Nil = Nil type instance TFilter f (Cons a b) = IfThenElse (f a) (Cons a (TFilter f b)) (TFilter f b) instance (Force a a',Force (TFilter f a') z) => Force (Filter f a) z data Search (f :: * -> *) l type family TSearch (f :: * -> *) l type instance TSearch f Nil = Nothing type instance TSearch f (Cons a b) = IfThenElse (f a) (Maybe a) (TSearch f b) instance (Force a a',Force (TSearch f a') z) => Force (Search f a) z data Foldr (f :: * -> * -> *) a b type family TFoldr (f :: * -> * -> *) z xs :: * type instance TFoldr f z Nil = z type instance TFoldr f z (Cons a b) = f a (TFoldr f z b) instance (Force a a',Force b b',Force (TFoldr f a' b') z) => Force (Foldr f a b) z data Concat l type family TConcat v :: * type instance TConcat Nil = Nil type instance TConcat (Cons a b) = Append a (TConcat b) instance (Force a a',Force (TConcat a') z) => Force (Concat a) z data Perm a type family TPerm a :: * type instance TPerm Nil = Nil :<: Nil type instance TPerm (a :<: b) = Concat (Map (Insert a) (TPerm b)) instance (Force a a',Force (TPerm a') z) => Force (Perm a) z data Insert a b type family TInsert a b :: * type instance TInsert a Nil = (a :<: Nil) :<: Nil type instance TInsert a (b :<: c) = (a :<: (b :<: c)) :<: (Map (Cons b) (TInsert a c)) instance (Force a a',Force b b',Force (TInsert a' b') z) => Force (Insert a b) z -- -- Maybe -- data Nothing data Maybe a instance Force Nothing Nothing instance (Force a a') => Force (Maybe a) (Maybe a') -- -- Pair -- data Pair a b instance (Force a a',Force b b') => Force (Pair a b) (Pair a' b') -- -- Bool -- data True data False instance Force True True instance Force False False data IfThenElse i t e instance (Force t t') => Force (IfThenElse True t e) t' instance (Force e e') => Force (IfThenElse False t e) e' instance (Force i i',Force (IfThenElse i' t e) z) => Force (IfThenElse i t e) z data BoolEq a b instance Force (BoolEq a a) True instance (Force False false) => Force (BoolEq a b) false data (:||:) a b instance Force (True :||: a) True instance (Force a a') => Force (False :||: a) a' instance (Force a a',Force b b',Force (a' :||: b') z) => Force (a :||: b) z type family Kawaii a :: * type instance Kawaii (a :<: b :<: c :<: d :<: Nil) = ((Kotori a) :<: (Naru b c) :<: (Suzu c) :<: (Ayu d) :<: Nil) type family TJudge a :: * type instance TJudge (a :<: b :<: c :<: d :<: Nil) = NatEq (Length (Filter (BoolEq False) (Kawaii (a :<: b :<: c :<: d :<: Nil)))) One data Judge a instance (Force a a',Force (TJudge a') z) => Force (Judge a) z type Kotori a = NatEq a One type Naru a b = Less a b type Suzu a = (NatEq a One) :||: (NatEq a Two) type Ayu a = (NatEq a One) :||: (NatEq a Two) type All = Perm (One :<: Two :<: Three :<: Four :<: Nil) type Ans = (One :<: Three :<: Four :<: Two :<: Nil) perm = (u :: All) ty = (u :: Search Judge All) -- checkfail = (u :: Filter Judge All) {- ことりちゃんが1位だし なるさんは3位だし すずさんは4位だし あゆさんは2位です。 -} ans :: Maybe (One :<: Three :<: Four :<: Two :<: Nil) ans = getType ty
で、checkfailが本当はやりたかった事なのですが、GHCが大量のメモリを喰ってしまって(ghc: memory allocation failed (requested 2097152 bytes)などとおっしゃる)ダメなので大量にメモリが載ってるマシンを使っている方はなんかFunDepsとかTypeFamiliesとか使ってやってみてください・・・。
一応正しい答えは出ています。
この本はパンツ穿いて無い問題とかもあって、萌えは救いなのです！！
上のバージョンはForceという型クラスに押し込んでいますが、FunDepsを使った方がType Families使うよりも速いような気がするので(Call-By-Nameな何かを型上で構築したり色々したのですが大して変わらなかった気もします)、こっちを張りました。
