Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能
EmptyCaseが入ってきた.absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ.
具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く.
まず,矛盾(bottom)の扱いについて.矛盾は「値を構成できない型」になればよいので,通常次のいずれかになる.
data Bottom
data Bottom = Bottom Bottom
直観主義における「矛盾からは何でも導ける(bottom elimination)」は,型としては,
bottomElimination :: Bottom -> whatever
となるが,今まではこれの実装は,
bottomElimination bot = bottomElimination bot
bottomElimination (Bottom bot) = bottomElimination bot
などにせざるをえなかった.結局のところ値を構成できない型であることを上手く使えておらず,無限ループのbottomに入り込むことによって任意の命題を引き出していたが,これがみんなの健康によくないのは明らかである.CoqやAgdaなどの定理証明系では停止性チェッカがあるため,このような実装は通常与えられない.
そして,これは「Bottomに限らず何からでもよいから何でも引き出せる」という命題を作ってよいのかという話でもある,たとえば,
getWhatYouWantFrom :: a -> whatever getWhatYouWantFrom anything = getWhatYouWantFrom anything
のように,同様にして任意の命題から任意の命題を引き出せてしまう,そのため,型を証明に使うことを重視するのであればどうみてもunsafeな実装(証明)方法になっている.
計算機においてbottomは「値を持ち得ないもの」や「計算が停止しないもの」に相当するが,証明において後者は本当に秘密道具たっぷりつまった四次元ポケット的ジョーカーなので,定理証明系は停止しない計算が慎重に排除された系として設計されている.
EmptyCaseが入ると,最早このようなunsafeな実装を使う必要は無い(といっても,Haskellである以上書けてはしまうところは変わるわけでもないのだが)
{-# LANGUAGE EmptyCase #-} data Bottom bottomElimination :: Bottom -> whatever bottomElimination bot = case bot of {}
次に,bottomを使う証明オブジェクトの作成,たとえばシンプルなところで命題の否定について.命題の否定Notは次のようになる.
type Not prop = prop -> Bottom
簡単に言うなら「propならば矛盾する」ので「propではない」である.
具体的な話として,TrueとFalseが等しくないという命題は正しいので証明が与えられるはずだ.
{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} data Bottom type Not prop = prop -> Bottom data a :==: b where -- propositional equality のようなもの Refl :: a :==: a type a :/=: b = Not (a :==: b) trueNotEqualFalse :: True :/=: False trueNotEqualFalse = 証明?
しかし,この証明(実装)を上手く与える方法は実はそんなに無い.EmptyCaseのドキュメントではerror関数を与えていたが,これが型の上で証明に用いるに相応しいものでないことは明らかだし,そのように書かれてもいる.
やるとすれば次のようにTypeFamiliesを使う方法があった.
{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} data Bottom type Not prop = prop -> Bottom data PropEq a b where -- (:==:) をメインに使っていきたいので別に定義 Refl :: PropEq a a type family (a :: k) :==: (b :: k) type instance True :==: True = PropEq True True type instance True :==: False = Bottom type instance False :==: True = Bottom type instance False :==: False = PropEq False False type a :/=: b = Not (a :==: b) trueNotEqualFalse :: True :/=: False trueNotEqualFalse = id
この方法では,PropEq True FalseがBottomと同じく値を持たないことが(Haskellにも)わかり,Not (PropEq True False)についてもその実体はBottom -> Bottomという型になるため,TrueとFalseが等しくないことをid関数で証明できる.のだが,執拗にtype instanceを作り込んでダメなケースが矛盾なんだよとHaskellに教えてあげなければならない.しかも,この(:==:)は他のものにも使えるはずだが,それらについてもイチイチ何が矛盾かと教えていたらキリが無い.
正直,他に良い方法があるならとても興味があるので教えて頂きたい.
これが,EmptyCase後では単に次のようにすればよい.
{-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE EmptyCase #-} data Bottom type Not prop = prop -> Bottom data a :==: b where Refl :: a :==: a type a :/=: b = Not (a :==: b) trueNotEqualFalse :: True :/=: False trueNotEqualFalse eq = case eq of {}
これまでは,その型には値が無いことはわかっても,それがBottomと同じ型になっているという事実を上手く使えなかったのだが,EmptyCaseによりそれを適切な形で利用できるようになっていることがわかる.