証明とか無視であぐだ
Agdaにはさん付けが良いのか、くんづけが良いのか、その他(って言っても)が良いのか分かりません。
あとAgdaは定理証明系の属という呼び方が普通で、それはPrologが人工知能向けだとかっていう(まぁLispが人工知能界隈向きというよりはマシな気がするんですけど)一言で見たものを戦かせるフレーズはどうかなと思うんですが、多分こういう系は修行僧以外にはやってほしく無いだろうっていうのがそうだと思うので、真意はわれわれ修行僧が見出さなければ成りませんね。
http://wiki.portal.chalmers.se/agda/
Wikiさん。
つぎに、処理系をなんとかして入れます。
Windowsはやはりバイナリ配布があって、修行向けなのかなーという気がするんですが、Macも前の記事の通りほぼ一発なので、Linuxも問題無く入るんじゃないでしょうか。(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download)
なにか資料をゲットする
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials
http://unit.aist.go.jp/cvs/tr-data/PS2008-014.pdf
私は日本人∧英語読めない系なので、日本語の資料が望まれます。
素晴らしい事に、AgdaのWikiに日本語の資料が置かれてて、これが「取りあえず置かれている日本人向けなんとか」みたいな酷い直訳のソレとかでは無くて「とても良いもの」であるというところが良いなーって感じですね。
修行しよう！修行！！ドガーッ！
Agdaが証明支援系である事を完全に忘れます
変な思い込み排除キャンペーンですよ。です。
Agdaのベースにしている型理論はMartin-LöfのIntuitionistic Type Theory(ITT)、直観主義型理論らしいです。ぼくは作ってないので知らないんですけど。
(Standard)MLや、Haskellは(多分)型付きλ計算という時の「型」をベースにしたもので、割とそうでない型理論としてITTとCalculus of Constructionsがあって以下略。
詳細については
http://ci.nii.ac.jp/naid/110002717101/
http://ci.nii.ac.jp/naid/110003743618/
などを。
Agdaで、ITTを用いていて(CoqはCCの拡張らしいですが)、普通に型付きλ計算でCurry-Howard対応/Formulae-as-Typesを利用してDependent-Typeっぽくやらないのかは分かりません。
多分、もとから直観主義一階述語論理を指向(厳密に言うと全然違うと思うんですけど。ダメじゃん)してるっていう意味でITTとCCの方が良いんじゃないですかね。多分。
本質的な部分とか魂の差みたいな。哲学。
あとこういう難しい話をろくに理解してないのに書こうとすると酷い。止めです。
やる
「Agda言語は函数型プログラミング言語である. 」なので、証明とかは気にしません。
あと型が無い方が良いよーって人は、読んでも、やっぱり型が無い方がいいじゃーんてなってそれは修行にならないし時間の無駄なのでこんなの読まない方が良いです。
それどころか、SML,Haskell,OCamlあたりを使った事が無いと、細かい説明を省くので、苦しいと思いますが、なんか雰囲気だけでも味わえると良いんじゃないかなーとか。
そんな事は0ミリも考えてます。
「依存型付函数プログラミング言語として」
依存型ってなんじゃらーっていうのがあるんですけど、
パラメータ付の型を完全に一般な形 で取り扱うことができる. 型も値と同じように計算の対象とすることができ, 型をやりとりする函数を書くこともできる.
という事です。
ふいんきは割と大事なので、
module Hatena where data Nat : Set0 where zero : Nat succ : Nat -> Nat add : Nat -> Nat -> Nat add a zero = a add (succ a) b = succ (add a b) data Adder : Nat -> Set0 where adder : (a : Nat) -> (b : Nat) -> Adder (add a b)
Natというのは、自然数を表す型です。
とりあえずこれを読み込んで見ます。
読み込みはコマンド表を見ると
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations
C-c C-l Load a file
ふぁいるをよみこむ って感じだと思います。たぶんこれぐらいの英語は大学生なら読めます。
これで「Nat型の値」をどうやって作るかというと
one = succ zero two = succ one ...
て感じですね。
実際に型をチェックします。
コマンド表を見ると
C-c C-d Infer (deduce) type
とか書いてるので、型を調べます。値は調べませんよ・・・。まぁoneとかtwoとかはトリビアルですけど・・・。
これはsplitされた下の方に"Inferred Type"なんて書いてるのがチャーミングです。
Natが出とります。
twoも同様。
ここまでは依存型なんて一切使ってません。使ってるのは、Adderの方ですね。
そもそも、このAdder、単純な関数addと完全に被っていて、その存在意義が全く分からないって感じだと思います。
これは私もそう思ってるんですが、Agdaで値を出力する方法が分からんので無理矢理作りました。
例えば！お分かりだと思いますが、Agdaには0とか1とか2とか、定義されてませんし、そのようなものを出力する関数も在りません。
putStrという文字列を出力する関数はあるのですが、面倒臭い・・・。というか尋常じゃないです。
普通の言語だと、処理系を対話モードで開いて式投げ込めば結果として値を得ますけど、分からん。
今回は、自然数の足し算の結果が欲しいなーって成ったケースを想定してください。
勿論
four = add two two
は出来ます。出来ますけど、これを型推論した所で、four : Natしか出ません。使い物に成らない。
要するに型しか表示出来ないみたいなもので、訓練された人達はここで、じゃあ型レベルでやれば良いんじゃないか、例えば
data Zero : Set0 where ぜろ : Zero data Succ (A : Set0) : Set0 where さっく : A -> Succ A
これは確かに
ぜろ : Zero さっく ぜろ : Succ Zero さっく (さっく ぜろ) : Succ (Succ Zero)
で良いんですけど、じゃあどうやって加算を定義するか、となった時に、さてどうするんでしょうか・・・。
色々やろうとするんですけど、Agdaがちょっと意味分からん感じなので、出来るようにしてみたら、結局それが「依存型」を使うそれだったって事です。ご都合主義です。
add : Nat -> Nat -> Nat add a zero = a add (succ a) b = succ (add a b) data Adder : Nat -> Set0 where adder : (a : Nat) -> (b : Nat) -> Adder (add a b)
addに関しては良いと思います。良く無いよーって人は、ペアノさんの算術に関する公理眺めてください。
Adderは、代数データ型(みたいなもん)なんですが、奇妙な事に、こいつ「値」を取るんですよね。
余りに自然に出て来てるのでなんですが、Haskellやってる人は
data Adder :: Int -> * where MkAdder :: (a :: Int) -> (b :: Int) -> Adder (a + b)
が果たして出来るだろうかっていう事でもっと簡単には
data Hoge :: Char -> * where MkHoge :: (c :: Char) -> Hoge c
とかって出来ますかねみたいな。型コンストラクタが値を取るのは出来る(ので、MkHoge Intは違法じゃない)ですが、Hoge :: Char -> *でダメだっつー事です。
これが出来ると
:t MkHoge '0' => Hoge '0'
みたいな感じで嬉しいですけど、ダメです。
型に対しての値を型シグネチャで操作出来る。パラメータ付きの型を持てる
みたいな感じですね。一階述語論理ゆえんです。
ですから
val = adder (succ (succ zero)) (succ (succ (succ zero)))
とかして、C-c C-dでvalの型を推論させると、
Adder (succ (succ (succ (succ (succ zero)))))
とかでやったなーって気持ちになります。
おいなんでvalに型を書かない?
val : ? val = adder (succ (succ zero)) (succ (succ (succ zero)))
とかをやると、ちょっとした定理証明支援系みたいな匂いをだすんですが、分からないので分からない事には黙します。
ListとArray
上みたいな実に下らない例はどうでも良いんですが、ListとかArrayはどうやって書くんだーみたいなのは、多相らしきことをやるにもお役立ち！！って感じですよ。多分。
data List (A : Set0) : Set0 where [] : List A _::_ : A -> (List A) -> List A
楽勝過ぎです。
で、これ何が良いかって言うと「A と リストAのCons」って所が良いんです。つまり、要素の型が違う場合は結合出来ない。
ちょっとやってみると
data Bool : Set0 where true : Bool false : Bool nil = [] -- この型を見ると面白いです list1 = one :: nil -- この型 は List Nat list2 = true :: list1 -- ??
最後のlist2の構築は型的な意味で有効でしょうか、失望されちゃうでしょうか。
あとヘテロリストも出来て。出来てっていうか・・・まぁ
data HList : Set1 where Nil : HList Cons : (A : Set0) -> A -> HList -> HList hval = Nil hval' = Cons Nat one hval hval'' = Cons Bool true hval'
Cons Nat one hvalのNatとか、Cons Bool true hval'のBoolとかがださ過ぎる。型は適当に推論しれ！！って言う人向きの為に(向きの為にじゃないですけど。知りませんけど。)
どこまで推論してくれるか知りませんけど、こういう明らかにそうだっぽいのは。まぁ何が明らかにそうだなのかって分かりませんけど。
data HList : Set1 where
Nil : HList
Cons : {A : Set0} -> A -> HList -> HList
hval = Nil
hval' = Cons Nat one hval
hval'' = Cons Bool true hval'優れてる！！って感じです。でも相変わらず値の出力方法は知らんので勘弁ですね。
配列もちょーらくしょーって感じです。眠くても出来ます。
data Array (A : Set0) : Nat -> Set0 where
* : Array A zero
_++_ : {n : Nat} -> A -> Array A n -> Array A (succ n)
ここまでのまとめ
ろんりがちょっとわかるなーって人にへたくそに説明すると : 直観主義一階述語論理っぽいよ！！あとユニバーサルな型があります！！
それと、このPDFの4章「論理の符号化」で力づく証明っぽいなーっていうのが出て来ます。そこまでやるかどうかは知りません。ヒャッコの新刊まだかなー。
ちゃんと型の付いた関数型言語(とか書くと物議を醸すらしいんですが、ぼくは寝ます)やってるひとにへたくそに説明すると : 依存型という、型レベルで値レベルな操作が出来る/型がパラメータを持つ、ような事が出来ます。型の階層があって(Set0とかSet1とかSet2...)、これを使えば、「ぽりもるふぃずむ」な事も出来ちゃう！！
C++でテンプレート使える系 : C++のテンプレートも大概だと思います
Dでなんかやってる人 : Dさんのこと、今度紹介してください。
PCASTLやってる人 : んっふっふ〜
