なんだかよくわからないながらも型で遊ぶ

数理論理学の試験勉強していて触発されて、少し遊んでみた。自分でもいまいちよくわからない。
なんか適当にやってても、インタプリタがいろいろアドバイスしてくれる 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>