なんだかよくわからないながらも型で遊ぶ
数理論理学の試験勉強していて触発されて、少し遊んでみた。自分でもいまいちよくわからない。
なんか適当にやってても、インタプリタがいろいろアドバイスしてくれる GHC は素晴らしい。なんと付けるべきオプションまで教えてくれるんですよ。意味わからんのだけどね。そのうち調べよう。
型で計算を行う(?)プログラム。(微妙に修正しました)
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances -fno-monomorphism-restriction #-} data ZERO data Succ a class Plus x y z | x y -> z where plus :: x -> y -> z plus _ _ = undefined class Mult x y z | x y -> z where mult :: x -> y -> z mult _ _ = undefined type ONE = Succ ZERO type TWO = Succ ONE type THREE = Succ TWO instance Plus a ZERO a instance Plus a b c => Plus a (Succ b) (Succ c) instance Mult a ZERO ZERO instance (Mult a b c, Plus a c r) => Mult a (Succ b) r instance Show ZERO where show _ = "O" instance Show a => Show (Succ a) where show x = 'S' : show (dec x) dec :: Succ a -> a dec _ = undefined inc :: a -> Succ a inc _ = undefined zero = undefined :: ZERO one = inc zero two = inc $ inc zero three = inc $ inc $ inc zero mult3 :: (Mult a THREE b) => a -> b mult3 _ = undefined mult9 = mult3 . mult3
Plus のインスタンス宣言のとこで迷っていたら、id:syd_syd さんが教えてくれました。さすが。
Mult のインスタンス宣言のとこはちょっと怪しい。いろいろ試してたら(偶然)わりとすんなりできてしまったので…。自分でもいまいちわかってないです。
*Main> one SO *Main> two SSO *Main> plus two three SSSSSO *Main> mult zero three O *Main> mult three two SSSSSSO *Main>