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によりそれを適切な形で利用できるようになっていることがわかる.