#http://oxij.org/note/BrutalDepTypes/ のThe magic of dependent typesにあるdiv2eについてなんですが． #div2e 4を与えた時点でagdaは型としてはeven 4 -> NatつまりT -> Natとなることを推論してはいないのでしょうか？
#何が言いたいかと言うと，第一引数の(n : Set)に依存するeven nという第二引数ってそもそも与える必要とかあるのが不思議なんです．
#4なら4と与えた時点で自動的に第二引数の型はTと分かるのでpとか与えることの意味がどうも分かりません．
#実際最初の条件節はdiv2e zero _ = zeroで，
#二番目の条件節はdiv2e (suc zero) ()になる．odd numberの場合にはeven 3などとなって_|_だから項がないしそれでいい．
#最後の条件節の場合のpはこれはpってのはttなり()なり分かるのではないの？
#第二引数のeven nをinplicitにできるんじゃないの？と思って，{p : even n}としようとしたら，最後の条件節で
#div2e (suc (suc n)) = suc (div2e n)ではエラーになる．最後の(div2e n)がyellow扱い．
#:loadするとUnsolved metas at the following locations:と出る．
#div2e (suc (suc n)) {p} = suc (div2e n {p})とすると回避できる．
#この辺の事情がなんでなのかよく分からないのです．
#"div2eはnが4ならeven nがtopと理解してよしなにttにしてくれる"ではなく"div2eはnが4ならeven nがeven 4がtopである根拠も一緒に要求する"
#だからeven nに相当する証明オブジェクトも無いと"div2e nは呼び出せない"
#おお，分かりやすい．
#ということが"From the caller side, we are not able to call the function with an odd n"として書かれています．
#「そこは呼び出す側からすると，odd nで関数を呼び出すことはできません．」と，そのまんま読んでました．
#なるほど，じわじわくるな
#A->B->CをAならば，BならばCと考えると
#Aの証明のひとつとして4を与えて4はNatである
#BがAの証明に依存していて4がevenであるという命題になるから
#even 4の証明オブジェクトとしてttを与えると
#Cの命題となってその証明オブジェクトとしてdiv2を意味するNatになる証明オブジェクトを作っている．
#とするとeven nをimplicit argumentにすることの意味はあまりないのか．
#プログラムにdiv2e 3 _な式を書いてたとしますよね．
#この時agdaはエラーでコンパイルできねぇって言いますが
#これは3はNatである．even 3の証明は無いってことを示せないのでabsurd patternに落ちるからってことでストップする？
#これはevenの第二条件節even (suc zero) = _|_に到達してそれで(3 : Nat) -> even 3 -> Natな型を満足する証明オブジェクトが無いことを理解してコンパイルエラーを出すと思っていいのかな？
#つまりコンパイル時にevenな計算が走る？
#その場合，プログラマがコンパイルの処理に口を出せているってことになると思うけど．
haskell-ja > Archives > 2013/05/14