こわくない Idris (6) 補足

プログラミング


こわくない Idris (6) - M59のブログ
1年前に書いた記事を読み返していたら、証明がすぐには理解できなかった。証明の内容を言葉で分かるように書いておきたいと思う。

次のコードのMyHead.headは、全域函数だ。

%default total

namespace MyHead
  head : (l : List a) -> (isCons l = True) -> a
  head Nil prf = FalseElim (replace {P=P} prf ())
    where
      P : Bool -> Type
      P False = ()
      P True = _|_
  head (x :: xs) _ = x

head函数は、最初の引数のリストの先頭の要素を返す函数だ。head函数の2番目の引数に、リストが空でないことの証明を取る。リストが空でない証明を要求することで、空のリストから先頭の値を取り出す操作を防いでいる。

最後の行のhead (x :: xs) _ = xは、空でないリストの最初の要素を取り出すだけのコードで、何の問題もない。証明は単純に無視している。

問題は、head Nil prf = ...となっている部分が何をしているかだ。この部分は、最初の引数にNilが渡されてきたにも関わらず、そのリストが空でないという証明も渡されてきた場合についての記述だ。「そんなの、あり得ないじゃないか。」そう、あり得ない。矛盾だ。

headが全域函数であることを示すには、すべての場合でa型の値を返すということを示せば良いのだけれども、引数に矛盾がある時にはどうすればいいのか。実は、矛盾がある場合には、どのような型の値も作ることができる。その事実を表すのが、FalseElimだ。

FalseElim : _|_ -> a

FalseElimのFalseが指しているのは、Bool型のFalseではなく_|_のこと。_|_は矛盾だとか偽だとか、そういう意味だと思える。もし矛盾がある（偽が恒真だと示せる）ならば、そこから任意の命題が導ける。この規則があれば、矛盾から任意の型の値を「作る」ことができる。そんな場合はあり得ないのだけれども、あり得ないがゆえに。

最初の引数がNilのとき、次の引数の型はFalse = Trueになる。ここから、矛盾を導こう。

replace函数は、次の型を持つ。

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

直感的には、x = yが成り立つ場合には、命題P xとP yは同値だから、P xをP yに置き換えても問題はないというふうに読める。ここでPを

P : Bool -> Type
P False = ()
P True = _|_

とすれば、replace {x=False} {y=True} {P=P}の型が

False = True -> P False -> P True

すなわち

False = True -> () -> _|_

となることが分かるだろう。そこにprf : False = Trueと() : ()を渡せば、望んだ型の値replace {P=P} prf () : _|_が得られる。

分かりやすくなるように書こうとしたけど、あんまり分かりやすくならなかった。

現在のIdris

現在のバージョン Idris 0.9.14 では、headは次のように定義されている。

||| Get the first element of a non-empty list
||| @ ok proof that the list is non-empty
head : (l : List a) -> {auto ok : isCons l = True} -> a
head []      {ok=Refl}   impossible
head (x::xs) {ok=p}    = x

impossibleを使えば、引数が[]で、暗黙の引数okがReflであるケースが不可能であるという指定になる。Refl : x = xとisCons [] = Trueで型がユニフィケーションできないので、確かにこのケースが不可能であると型推論器は判断できるし、(=)はコンストラクタがReflだけなので、これで全部のケースを尽くしているので、結局totalだということになる。つまり、1年前に書いたややこしいコードは本当は必要なかった。