#Agda の Set a はなんでしょうという質問に対するコメントです。
#Set 0, Set1, Set 2, ..., Set n, ... の列を Universe といいます。
#a がレベル型であるとき、 Set a と書きます。これは Agda では Universe polymorphism といいます。
#検索の助けになるとよいのですが。たとえば B. Nordström らの "Programming in Martin-Löf type theory" に載っています。
#Universe とは何かが載っています。PMLTT は Agda については触れていない（はず）です。
#Windowsの人でもLost_dogさんのようにWindowsインストーラ版をそのまま使ってるとフォントについては気にならないようです
#Windows 版インストーラを作られた方の残業時間を知っています（号泣
#うわぁ
#Agda のドットパターンがわからないという質問に対するコメントです。
##2.4 節で長さ付きのリスト（しばしば Vec と呼ばれる）に対する内積 inner を定義するときに dot patterns を知らないとハマることが紹介されています。
#二つのベクトルの内積を考えるとき、それらの長さは同じでないと、内積の計算に困ります
#zipWith もそうですね
#内積の定義は、いつものように長さによる帰納法で書くわけですが、左のリストの長さと右のリストの長さを書く必要があって、人間の感覚では同じ n を使いたいのですが、直感に反して Agda はパターンマッチに失敗する
#そこで . の登場です
#Andreas Abel の順でした、すまぬ。あとは上に挙げた Andreas のドキュメントをどうぞ。
#dot patterns は = の左側にあらわれる .pat のことです
#おお、ありがとうございます。
#現在子守り中なので、そらも後でつまみ読みしませう。
#混乱しないでほしいのですが、型の定義に . がつくことがあります。 foo : .A -> B のように。これは最近入った proof irrelevance という機能ですが、わからなくなった時点で聞いてください。Agda wiki にあります
#agda2 の巻き戻しは、一度実装されて、その後亡くなりました。Emacs の undo と同時に背後で動いている ghci を記憶喪失させる必要がありますが、それはヤバいです。
##これも内容としては非常に平易なところを説明してて良かったのですが、誤字とかいくつもあって、内容の読み取りに影響しそうな誤字が複数あるだけに残念。
#ikegami__ さんの挙げてくれたpaperも短かいですね。これならなんとか。
#Lost_dogさんが書いてたパラメータとインデックスの違い。
#Vectors are lists over a certain element type A of a certain length n.
#While the parameter A remains fixed for the whole list, the index n varies for each sublist.
#とあるんだけど、これだな。
#パラメータAは全てのリストで固定されたままなのに対して、インデックスnはそれぞれのサブリストで異なる。
#Aだって別に変化できるやろ。型変数なんだし。
#って思ってたけど、「それぞれのサブリスト」ってのはあれですね。
#Vec A (suc n)のtailはVec A nでAは固定だけどnは部分リストと全体リストで変化するという。
#そういう理解であってんのかな。
#長さを持ったベクトルについて、長さ n + 1 のベクトルから長さ n のベクトルを
#tail はつくります
#手続き型言語の最初のプログラムが Hello, world だとすると、関数型言語では階乗 n! で、依存型は長さ付きリスト Vec な気がします。これらはどれも一番シンプルでかつ特徴がでている
#Lost_dog_ さんは Thorsten さんからもアドバイスをもらえたようでなによりです。Agda ML は Haskell-cafe と同じくらい親切な人が多いので勇気を出して聞いてみましょう
haskell-ja > Archives > 2013/04/20