##agdaのircログよんだ。
#読んだのに何をやり取りしてたのかわからないという致命傷
#二三度読み直して話の流れはなんとなく追えた。
#でもそもそもこの場で前提にしてる知識のレベルが違いすぎてi got it!とならない…orz
#DGP-Agda.pdfで35枚目にwe cannot inspect types directly.と書いてあるところのinspectってどういう意味だと理解すれば良いの？
#Bool -> SetやNat -> SetのようなCodeからSetを返すようなのをinterpretするとかdecodeすると言ってる感覚は分かってきたんだけど、inspectがイメージ出来てなくて。
#Data.Rational._÷_の例をやってみて差が出るのは出ますね。
#どうも「型システムがよしなにやってくれる状況が作れる」というのを誤解しているのかもしれませんが、
#Data.Rational._÷_の定義を見ていると、denominatorがzeroの時には/=記号なimplicit parameterがabsurdパターンになるので
#(+ 1) \div 0とやると型チェッカがエラーを出してくれるのかと思ってたんですが
#そういうものでも無いのですね？
#この場合型チェッカは何をしてくれるのでしょう？
#notNotId : (a : Bool) -> isTrue (not not a) -> isTrue a
notNotId true p = p
notNotId false ()
#こんなのがあるわけですが、
#そもそもaがtrueならisTrue (not not a)は自動的にTrueに決まるしfalseならFalseに決まるはずですよね。
#なので、implicitにして引数として与えずとも型システムが自動的に推論してくれるのでは？と思います。
#そこで
#notNotId : (a : Bool) -> {p : isTrue (not not a)} -> isTrue a
notNotId true {p} = p
notNotId false {()}#とするとこれは通る。
#でも、これだとagdaiとかでloadして評価すると
#Main> notNotId true
λ {p} → p#となって、まぁ事情はなんとなく分かるんだけど、暗黙の引数なんだから与えずともpにあたるttを返してくれてもいいんじゃないかと。
#それそのまま使えばいいんだと思いますよ？ttとして扱っても殆ど問題無いハズ．
#あれ、そうなんですか。
#じゃあ合ってるんだ、この理解で。
#_÷_て(Bool, {Top,Bottom})のuniverseの例で狭すぎるし反省
#「これは○○する必要があるからuniverseを使う」で言うなら「特定の幾つかの上の型の上で定義される関数を書きたいからuniverseを使う」
#s/幾つかの上の型/幾つかの型/
#この「幾つかの型」が本来欲しいものでdecodeされた後の型のあつまり，decode前のCodeである型にencodeされていると考える．
#Codeとdecodeによって，Set内任意の型とかではなく幾つかの型に制限することができている．
#ふむふむ。
#この限られた型の世界を作るから"universe construction"なんだと思います．
#おお、なるほど。それはかなり納得できる。
#と言いつつ，誰に確認したわけでもないのでこの認識で合ってるのかは不明
#もっと初歩的な質問になりますが
#「その本来欲しいもの」がなぜTrueやらFalseといったSetのメンバーなのか。
#例えば欲しいものをdata Foo where
#でfooとbarを構成子として
#この構成子がdecodeされたものという風に
#これは微妙か
#data DProp : Set where; True : DProp;False DProp
#みたいにしたものをdecodeされたものとして
#data Bool : Set where; true : Bool; false Bool;
#これをcodeとしてBool -> DPropなものをdecode functionとして構成できないものなの？
#という疑問ですが。
#Bool,isTrueの場合はそれが単に自然なencodeの上使い易いからでしょう．証明の中で明らかなBottomが出てくるととても楽ですし．
#_÷_の例で
#absurdパターンでそこから先見なくとも良し，⊥-elimで任意の命題を引き出しても良し，
#あ、それです、それ。absurdパターンが出てくるところ。
#_÷_の例でも第2引数がzeroの時には{≢0 : False (ℕ._≟_ denominator 0)}がFalse型つまり項がない。
#Falseな命題の証明がない。つまり偽だと。
#そうですね．
#それは証明として見た場合にはそこから先は考えなくて良いとなるのですね？
#普通の型と実装という見方をした場合、私はzeroを第二引数に与えたら、それは型チェッカがダメよってエラーなりなんなり上げてくれるものなのかと思ってたんですが、それは違うのでしょうか？
#見なくていいというのは，absurdパターンになったら何でも成り立つからです．
#え？何でも成り立つのですか？
#偽ってことは成立しないのでは？
#ああ，型としては満たすものは無いです．
#Data.Empty.⊥-elim の型を見てみて下さい
#あーこれ、どっかで見たような。
#あー分かった。あれだ「pならばq」で、「pでない」ことについては何も言えないからqが成立しようがしまいが問題ないんだ。
#p:宿題を終えた q:おやつが貰える
#p -> q
#宿題を終えたらおやつが貰える
#宿題を終えた かつ おやつが貰える
#ちがうな起こりえる全パターンを考えて
#4種類のパターンのうち、宿題を終えないの場合にはp->qにおいてpが偽なら「ならば
#「ならば」はそもそも成立してないからqはなんであっても良い?のか?
#それはともかく
#Vecの_!_の例のようにFin nを使ってVec A zero ! fzeroで型エラーになるように型レベルでチェックしてくれる話になるものと思ってたんですが、_÷_で 1 ÷ 0でも何も型エラーがでないのが腑に落ちないです。
#(Bool, {True,False})のuniverseの例でも同様で
#postulate _div_ : Nat -> (m : Nat){p : isTrue (nonZero m)} -> Nat
#で16 div 0とかすると型チェックがなにか言うのだと思ってたのですが、どうもそうならない。
#Here the proof obligation isTrue (nonZero 5) will reduce to True and solved automatically by the type checker.
#とあって、例としては16 div 5のコードが書いてあるからisTrue (nonZero 5)という説明になっているのですが。
#0ならisTrue (nonZero 0)がFalseになってしまう。
#あ、すみません。なんかわかったかも。。。
#これは型的には別に合ってますね。
#Falseだからこれも⊥-elimか。
#Fin nの例とは違いますね。
#型チェッカーが自動的にTrue(あるいはFalse)を導出できるよと言っているのであって、型が合ってないとは言ってないな。。。
#しかし、そうだとすると、この_div_の定義でisTrue (nonZero m)がimplicit parameterとして有ることの意味ってなんぞや？
#普通に_div_ : Nat -> Nat -> Natとするのに対してuniverseを使ってisTrueを利用したことで「型システムがよしなにやってくれる状況が作れる」のやってくれるのは一体何なのか？
#postulateされてて定義が無いのでアレですが，実際にdivを実装する段になるとpをその内部で使うハズです．
#divisorが0のときは定義できないので，0のときは自明な条件として渡ってきたpを使ってabsurdパターンでシカト決め込むように実装されるハズ
#(x div zero) ()って書くってことですね。
#(x div zero) {()}か。
#そんなカンジです
#そうすると、使うときには x = 5 div 0 とか書いた場合、何が起きますか？
#型エラーになるわけではないんですよね？
#notNotId true同様に普通に{p}を求めてくるλ式かな？
#ああnotNotId false ()というパターンの方に近いのでしょうか。
#これはnotNotId falseと入力しても何が返ってくるとかなくて、よく分からなかったんですよね。
#そうでしょうね．
#恐らく
#C-cC-nでnotNotId falseって入れたらnotNotId falseって返って(？)おしまい。
#なにが起きているのかサッパリでした。
#C-cC-dすると{⊥} → ⊥が見られるのでは
#同様に5 div 0も{⊥} → ℕかな
#おお、ほんとうだ。
#-- 停止性示せてない雑なdiv
_div_ : ℕ → (n : ℕ) {p : isTrue (nonZero n)} → ℕ
(m div zero) {()}
m div suc n with compare m (suc n)
m div suc .(m + k) | less .m k = 0
.(suc n) div suc n | equal .(suc n) = 1
.(suc (suc (n + k))) div suc n | greater .(suc n) k = 1 + (suc k div suc n)#infer (deduce) typesか
#そのコードをC-cC-lすると先頭の_div_が赤に、最後の(suc k div suc n)が黄色になるのですが、これは？
#このdivの定義ではAgdaには停止性がわからないからでしょう
#ああ、If Agda cannot see that a definition is terminating/productive it will highlight it in light salmon
#これか、停止性を示せてないってのはこのことですね。
#そうです
#ちなみにこの状態ってエラーがあるから正常にロード出きてない？それとも示せてないけど、とりあえず問題なくロードは出きてる？
#なんか評価できてるっぽいですね。
#どっちだったかな．確かemacs中ではロードはできてると思いますが，
#agdaインタラクティブモードでは--no-termination-check無いと怒られる
#あ、はい。C-cC-lしてC-cC-nで16 div 5が{True}->3ってなってるので大丈夫そうな気がします。
#ああそのオプションもどっかで見たことがある。
#なるほど、色々疑問点が解消されてきました。(まだ全然勘がつかめないけど。)
#ありがとうございました。
haskell-ja > Archives > 2013/04/25