#cutsea さんは「サルでも書ける Agda 入門」を探しておられますが、stackoverflow はごらんになりましたか : http://stackoverflow.com/questions/9455786/how-to-learn-agda #あーこれ見た気がする。いきなりCoqとなっててスルーしたけど。
#今読んでるのはUlfのtutorialです。
##それ見たとき"Step One: Learn Haskell"で爆笑しました
#これまだ未完成なんだと思うんですが、止まってますよね、たぶん。
#止まってそうですね
#これのためにhakyll入れましたよ。
#いろいろ分からないことが多すぎるんですが
#Haskellで言うところのclassってのはSet1になるんですか？
#Monadの定義がdata Monad (M : Set -> Set) : Set1 where
#みたいな感じになってたのを見たのですが。
#Set1って型の型ですよね．
#そう説明されてますね。
#Set aみたいなのも読んでて出てきたな。これはなんだ？と。
#Set1になるというよりMのものより一段メタな何かになるという感じだと思いますが
#んー、わかるようなわからないような。
#もう少し基本的そうなところを聞いてみるか。
#ドットパターンが分からない。どういう時に.を付けるのか。
#なんで必要になるのか。
#ドットパターンは大抵自分で付けるのではなく，付けてもらうのがよいです．
#c-c c-c等で
#C-cC-cってcase分けですよね
#そうです．
#でもドットパターンってleft handにしか付かないのでは？
#hole使うのright handのような。
#まさかどっちでも使えるのでしょうか？
#えっと，holeに制約相当の仮定を入れてc-c c-cすると
#その制約相当の仮定をcase分けすると同時に，その制約に入っている依存型を適切にドットパターン化してくれます．
#あぁそうか。場合分けされた結果として.付きのものがcaseとして出てくるですね。
#s/依存型/依存型の値/
#じゃあ、テキストの.使ってるやつをC-cC-cで誘導してみればいいのか。
#それは試せそう。
#今読んでるUlfのpaperでは The rule for when an argument should be dotted is: if there is a unique type correct value for the argument it should be dotted.
#とあります。
#いくつかの引数の間に同じものを指している関係(依存している関係？)があれば付けるのかなと、思ったのですが。
#そうですね．
#たとえば，
#drop-suc : ∀ m n → suc m ≡ suc n → m ≡ n を示すときに
#drop-suc m n Sm≡Sn = { }0 を
#drop-suc m n Sm≡Sn = {Sm≡Sn }0 して
#c-c c-c
#drop-suc .n n PropEq.refl = { }0 なります
#ドットパターンが出ましたね．
#drop-suc .n n PropEq.refl = PropEq.refl で完了です．
#すみません。今のを試したかったら何をopen importすればいいですか？
#あ，すいません
#open import Data.Nat
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)
#あ，reflもusingしておけばよかった
#おお、きたー。
#あれ？reflをusingするとエラーになる
#open PropEq using (_≡_; refl)
#あ、;か。
#drop-suc .n n refl = refl 最後このカタチでよくなるので
#C-cC-tとしたら n\==nになるからreflで良さそうだと考えていいのかな。
#そうですね
#ちょっと逸れますけど、refineした後でなんか違うと思って一つまきもどしたい事とかあったんですが、どうすればいいんでしょう。
#まきもどし…ってあるのかな？
#みあたらなかったんだけど、そういうことって無いですか？
#慣れないせいか、ちょっと戻してみたいって思うことがちょくちょくあるんですが。。。
#ま、いいや。
#あんまり思い当たりませんですね．
#data Parity : ℕ -> Set where
even : (k : ℕ) -> Parity (k * 2)
odd : (k : ℕ) -> Parity (1 + k * 2)
parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (suc n) with parity n
parity (suc .(k * 2)) | even k = odd k
parity (suc .(1 + k * 2)) | odd k = even (suc k)
half : ℕ -> ℕ
half n with parity n
half .(k * 2) | even k = k
half .(1 + k * 2) | odd k = k
#こういうのがあるんですが、このドットパターンは何と同じと言っているのかが自信がないです。
#withパターンによるparity nがkの偶奇に関する性質を与えるので，それをc-c c-cで分解するとわかると思います．
#parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (suc n) with parity n
parity (suc n) | even-or-odd = {even-or-odd }0#まで書いてc-c c-cですかね．
#ぬぬ。
#k * 2とか1 + k * 2ってのはHaskellのn+kパターンのようなものですよね？それでパターンマッチできていると。
#どこまで進めてからc-cc-cするのかの勘が働かないです。
#今のはお手本を見せてもらったら、それしか無いじゃんって感じなんですが。
#with parity nを使うのは自分で気付かないとダメなのかな。
#with使う場合はそうですね．その後に何を使うかは自分で考えることです
#(suc n)のnでC-cC-cしたら(suc zero)と(suc (suc n))になって、そらそうだキリがないわ。って感じだったのでダメダメでした。
#ちなみに{!!}はなんに使うのでしょう？
#しかもテキストとかでは{! !}みたいになってるのに、私の環境では{!!}となるのです(汗
#中に何か入れつつも?と同じくgoalに変えられるものだと認識してるんですが違うのかな
#?にしてc-c c-lで{ }0に変わるように，{!foobar!}にしてc-c c-lで {foobar }0
#んー、別に使わなくてもよさげ？ですか。
#私はあまり使わないですが，私が知らないだけで何かあるのかな？よくわかりません
#ゴールのテキスト表現が{! !}なのかな？emacs上だと緑色になるけれど
#まだまだ疑問やまもり。
#dataとrecordってどう違うんでしょう。
#今非常に気になっているのは
#data False : Set where
#record True : Set where
#ってやつです。
#c-c c-x c-d でロード状態をとくと、ゴールが全部 {! !} に落ちるあたり、そうなのかと思ってた
#False=⊥ True=⊤のことでいいのかな？
#まぁ{!!}はgoal(hole?)でいいよね
#ぬ？C-cC-xC-dはこっちの環境では動作しないっぽい？
#isTrue : Bool -> Set
#isTrue true = True
#isTrue false = False
#として、Setの世界でごにゅごにゅ使うみたいです。
#なので偽である=_|_なのか。
#False(⊥)は"その型に対応する値
#あ，切れた
#False(⊥)は"その型に対応する値が無い型"なので"ありえない命題"ですね．
#はい
#その型の実装(証明)が存在しないってことね。
#ああ、recordにしてるとrecord {} とかで値が作れてしまう？
#はい．で，True(⊤)は"構成要素が何も無くて良いレコード"なのでその反対ですね．
#dataでconstructorを無しにしておくとボトムになって、recordでfieldやconstrouctorを無しにしておくとトップになるのか。トップって常に真という理解でいいですか？(命題と証明の見方をした場合)
#トップのほうはconstructorあっていいですけどね
#そうか、constructできる分には問題ないからか。
#fieldがあったらマズいんですか？
#レコードは空集合が許されるので、フィールドのないレコードはただひとつの値を持つ、的な説明があったような
#ほうほう。
#フィールドがあったらただひとつの値にならないのか。
#そらそうだ。
#あとですね、reflの定義がなんか飲みこめないです。
#data _==_ {A : Set}(x : A) : A -> Set where
refl : x == x#あ、その前にパラメータとインデックスって単に構成子の型のスコープから見えるかどうかの違いだけですか？
#最初の出てきたのがVec A nの例だったので、Setなものがパラメータで(A : Set)のAなもの(項)になるのがインデックスかと思ってたんですが、そういう区別はないのですね？
##パラメーターとインデックスの違いは、CPDTで熱く語られていた
#が、そのリンクをすぐにだせない＞＜
#すでに上から読まないと？なtermがあるものの日本語の解説があるのはよさそうですね。
#ちょっと読んでみます。遅くまでありがとうございました。> notogawa,Lost_dog
###これかぁ、370pもある。。。
#お、4.4ですね。
#僕もわかんなかったから、わかったら教えてくださいｗ
#x ≡ _ のトコロまでは先に決まっていて，2つめのxの部分の条件を縛っている(同じものが入るときの型だけコンストラクトできる)ようなイメージで
#はい。
#それで実は最初 data _==_ {A : Set}(x : A) : x -> Set where とか書けないのか？と思ったのですが。
#なんか、それもちょっと奇妙。
#やはり項を取って型を構成できるのがまだ頭がすんなりついていかないです。
#よしんばそれが意図通りにできたとすると，x ≡ xという型しか書けなくなっちゃうですよね？
#そうなんですよね。
#パラメーターの値は、型にかいてあるものしか使えないが、インデックスのほうは変数的な気分なので何をいれてもよい
#じゃあ引数2つ必要なのかよ？と。
#x ≡ y という型も書きたいのです．でも値が存在するのは x ≡ x のときだけにしたいのです
#ふむ。
#その空気はなんとなく感じてました。でも言葉にはならなかったけど。
#「パラメーターの値は、型にかいてあるものしか使えない」ってのは？
#型に書いてあるものしかってどういう意味だろう。
#あれ？もしかしてパラメータって常に(x : A)とか{x : A}みたいな形式でAとかって書けないんでしたっけ？？
#x ≡ y 型だったら、かならず左側が x のコンストラクタしか使えない
#おおー、それかぁ!!
#といいつつ僕は間違ってるかもしれないのでｗ
#何その簡単な話は。テキストに書いてくれてもよさげなのに、一文ですむだろうｗ
#確かにAとかはあるけど、それは前に(A : Set)由来だな。
#Agdaには我々一般人にとってわかりやすい入門資料があんまり無い気がする…
#Coqも型システムとしては同じようなもの？マーチンレーフだっけ
#もしそうならCoqを学んでAgdaで対応を取った方が近道なのかな。
##その道も割と修羅の道な気がする > Coqを学んでAgdaで対応
#Predicativity: Coq is based on the Calculus of Inductive Constructions, an extension of Coquand and Huet’s Calculus of Constructions, an impredicative version of Martin-Löf type theory. Agda is a predicative extension of Martin-Löf type theory. Since Coq 8.2, however Set is by default predicative.
#とあるな。
#マジすか。。
#「CoqのtacticがAgda上でのどんな式変形に対応するのか」を把握できるかどうかにかかってますからね．
#まぁまだUlfのpaperも途中だし、まずは通して読んでみますけどね。短かいし。
#あとは数百ページのばっかでとてもじゃないけど最初に読む気になれなかった。
#手前味噌というか別に誰かに見せるツモリでやったものではないのですが，
#お、なんか出てきます？wktk
#Software Foundations日本語版を途中までAgdaで焼き直したものが
#おおーーーー
##参考になるかわかりませんし変な説明が入ってるかもしれないのでそのへんはまぁゴニョゴニョ
#さっそくwatch&cloneしてみました。
#やはりこのくらいやらないと身には付かないのね。。。
#すばらしい。
#色々ポインタももらったのでしばらく粘ってみます。
#thanx!!
#おやすみなさい＞＜
#やっぱ僕の説明おかしいなｗ だめだｗ
#昨晩はおたのしみでしたね
#これからなにか書こうとしていますが、そのまえに Chaton で Latin-1 を書くことができるかな。テストします : oe ---> ö
#Latin-1 は問題ないようですね。では、Unicode の文字用記号の N by bold type ℕ や、mathematical symbol ≺ はどうでしょうか。
#見ている側のフォントさえ表示できれば、ここでも使えることができるようです。ありがとうございます。
#Agda 用のフォントについて、notogawa さんは Windows で苦労しておられるようですが、MacOSX でもいくつか追加インストールする必要があります。
#MacOSX では「梅ゴシック」を新たに導入しました。Agda と the standard library については、これで問題はありません。
#Snow Leopard の Terminal は、Unicode の表示に難がある、とくに文字幅の扱いがだめです。色もたりません。
#そこで、iTerm2 の "Double-Width-Characters : Treat ambiguous-with characters as double with" を有効にします。これで terminal 上の Emacs が快適になります。256 色なので、highlight も綺麗に決まります。UTF-8 enabled な GNU screen とも共存します。
#ここ chaton の haskell-ja で Agda は off-topic ですけど、許していただけると思っています。
#一方で、Agda を知らないひとや Haskell の初心者がこのログを見て、ここに参加するのをためらうようなことは起きてほしくありません。どんな質問でも、割り込んで話をすればいいですよ。
#Agda のみならず、pandoc など Haskell 謹製のアプリケーションや、lens などのライブラリの話題をしてもよいと考えています。
haskell-ja > Archives > 2013/04/19