Haskell+GADTで定理証明 その1: 型レベル自然数の等価性

Haskell

実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないことになっているらしい。やっぱりHaskellを使うものとして型安全性くらいは保証したい。でも、かといって普通のHaskellではうまく型を付けられない。(Typeableクラスのキャストを使っても解決にはならない。)
そこで、魔法のGADT。 この型とこの型はぜったい等しいのにーというのが文脈から明らかなとき、それを表現できるのがGADTだ…というのが私の理解。まさしく私のケースにぴったりだ。これを使えばunsafeCoerceなんか要らんかもしれない。
いいかえれば、いわゆる定理証明をGADTつきのHaskellでやったろうじゃんということになると思う。私がHaskell上に構築したセッション型の型システムのsubject reductionをHaskellとGADTで証明するのだ…。

その一環としてまずは自然数が等しい(等しくない)ことの証明を表す型をデザインした。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

-- 型レ自然数
data Z = Z deriving Show
data S n = S n deriving Show

-- 自然数の等価性を保持するGADT。
data EqNat n n' where
  EqNat :: Nat n => n -> n -> EqNat n n   -- 等しい。パターンマッチでこれが出るとその後の文脈でn=n'と型がrefineされて嬉しい
  NeqNat :: (Nat n, Nat n') => n -> n' -> EqNat n n' -- 等しくない。残念。

instance Show (EqNat n n') where
  show (EqNat n _)   = "EqNat ("++show n++")"
  show (NeqNat n n') = "NeqNat ("++show n++") ("++show n'++")"

-- 等価性はシンメトリックです
sym :: EqNat n n' -> EqNat n' n
sym (EqNat n n')  = EqNat n' n
sym (NeqNat n n') = NeqNat n' n

-- n=nならn+1=n+1です
succeq :: EqNat n n' -> EqNat (S n) (S n')
succeq (EqNat n n')  = EqNat (S n) (S n')
succeq (NeqNat n n') = NeqNat (S n) (S n')

続いて、このEqNat n n'型を返す等価性判定のメソッドを実装した。もちろん型クラスを使っている。
このへんのテクニックは変態的に見えるかもしれないが、シグネチャさえ思いつけば型を合わせるように適当にプログラムを書けばうまくできてしまうのがMLやHaskellとかの静的型付け関数型言語の強みだ。

-- 型レ自然数を表す型クラス。もう一つの自然数を食わせるとEqNatを返してくれるメソッドをもつ。
class Show n => Nat n where
  eqz :: n -> Z -> EqNat n Z -- nはZと等しいか？
  eqs :: Nat n' => n -> (S n') -> EqNat n (S n') -- nは(S n')と等しいか？
  eq  :: Nat n' => n -> n' -> EqNat n n' -- nはn'と等しいか？

instance Nat Z where
  eqz n n' = EqNat n n'  -- Z == Z.   等しい
  eqs n n' = NeqNat n n' -- Z /= S n. 等しくない
  eq n n' = sym (eqz n' n)
instance Nat n => Nat (S n) where
  eqz n n' = NeqNat n n'       -- S n /= Z. 等しくない
  eqs (S n) (S n') = succeq (eq n n')
  eq n n' = sym (eqs n' n)

では使ってみよう。

Main> eq Z Z -- 等しい
EqNat (Z)

Main> eq Z (S Z) -- 等しくない
NeqNat (Z) (S Z)

Main> eq (S Z) (S (S Z)) -- 等しくない
NeqNat (S Z) (S (S Z))

Main> eq (S (S Z)) (S Z) -- 等しくない
NeqNat (S (S Z)) (S Z)

Main> eq (S (S Z)) (S (S Z)) -- 等しい
EqNat (S (S Z))

超うまくいっている。やったぜ。

...さっさとAgdaかCoq使えという諸兄のツッコミをお待ちしております。