#今日のログはまだ上記のリンクにありませんでした…時差的に明日になればそこにでてくると思います
#わかりました。freenode #agda にいる人達は賢いなあ。特に Saizan さんに感謝します（@seizans さんとしばしば見間違う）
#untangled now!
#残念ながら滑り込めなかった。
#まだlogにもあがってないですね。
#しかし100人以上いるのにはじぇじぇじぇーってなった
##agda は #haskell に比べると、静かなんですけど、誰かが質問すると達人がすぐに答えてくれる印象
#「Universe がわからんよ」はもつれた紐のようで、Saizan さんに整理していただきました。少なくとも Universe は 3 種類ある
#1. Agda 内部における Universe : Set0, Set1, ... の列
#2. Martin-Löf 型理論 ITT (Intuitionistic Type Theory) における Universe : 推論規則のあつまり
#3. Agda 上で定義される record Universe u e : Set (suc (u ⊔ e)) where ... : Codes と Decoding function のふたつから成る
#cutsea さんの質問は、 3. に属するもので、繰り返すと「Universe の文脈における code と decode とは何か？」だった
#Universeって言ってる場合文脈によって全然違う話をしているということでしょうか？
#はい
#じゃあ今私が読んでたところの説明はあくまで3に関するものですね。
#なにを読んでいらっしゃるのか教えていただけませんか。
#cutsea さんの引用した the purpose of a universe construction は、引用した通りのことを意味していて、わかればわかります（こんなのばっかりやな）
#Ulf Norell and James Chapman. Dependently Typed Programming in Agda. This is aimed at functional programmers.
##これです。
#Ulfのtutorial
##p29の3.2 Universeです
#あ、DGP-Agda.pdfのスライドも引用しましたね。昨夜のは。
#Ulf のチュートリアルに従って universe construction の説明をします
#はい。よろしく。
#途中面談で席を外すかもしれませんが、かまわず進めてください。後で追いかけます。
#まず、証明とはなんだったのか？と
#いうところからはじめます。Martin-Löf の型理論に基づく一階述語論理が Agda の標準ライブラリにありますので、一階述語論理における命題の証明ができます
#例を出すと、「または」は Haskell の Either と同義なので、あたかも Haskell のプログラムのような書式で命題と証明が書けます。import Data.Sum する（ここからあとは練習問題）
#しかし、論理はいろいろあります。自分で定義した論理と書式の枠組みを提供したい。Agda は型検査/型推論してくれればそれでいい。こんなケース。
#そこで Universe construction が登場する。
#Ulf のチュートリアルは、命題論理についてどのように論理と書式を提供するかを最初の具体例として取り上げています
#data Bool : Set where true : Bool; false : Bool
#これでまず書式が決まります。Universe construction の文脈では、この Bool を code と呼びます。code の定義はまだしていないのですが、後で説明します。
#Bool 型を定義しただけでは、なにが true でなにが false なのか決まりません。そこで、Set に decode する関数を定義します。Ulf のチュートリアルの isTrue : Bool -> Set が the decoding function です。
#訂正：「命題論理」は「ブール論理」の間違いです。気がついてくださると思いますが。
#OKです。
#なんとかついていってます。
#チュートリアルで証明したかったことは Bool における「かつ」 andIntro で、Agda の型検査アルゴリズムで valid になります
#実際、パターンマッチしかしていないはずです
#脱線：Ulf のチュートリアルの record True : Set where は心なし tricky だと思います。data True : Set where tt : True でもいいじゃないか…
#チュートリアルには、Bool の他に 2 つの例が紹介されてますが、ちゃんと読んでない＆長くなりそうなので省略します
#「いろんな論理があって、その枠組みを定義したい」についてですが。
#型：命題、実装：証明という対応関係自体は鉄板だと思っていいんですよね？だからどんな論理だろうとagdaの型チェッカを使えるのだと。
#論理といってもそういろいろ知っているわけでもなく、それらがどういう関係にあるのかも知らないので。。。
#定義したいではなく提供したい、か。
#ぼくも論理学者じゃないのでよく知りませんが、Curry-Howard 対応は鉄板だと思います。「証明とはなにか？」はとても興味がある対象です…
#「どんな論理だろうと」の部分はあやしくて、証明の正当性は型検査＆停止性検査に帰着しています
#もうひとつの観点は、ゲーデルの定理に該当する件ですが『利用と誤用の不完全ガイド』に触れてしまいますのでやめておきます
#Universe constructor における code の定義は説明をする代わりに、標準ライブラリの Universe.agda を見てください。Universe polymorphism を調べたあとなら Set a の a ってなんだよ、みたいな疑問も解消されるでしょう。
#Universe.agdaですか。
#agdaでghciにおける:i的なものってありますか？
#例えばUniverse.agdaで選言的な演算子がでてるけど、これがどこ出身なのかとか、どんな型なのかとか知りたいのですが。
#agda2-modeでそのあたり問い合わせらんないのかな。
#Emacs の grep-find ですかね…
##昼飯時にふと思って確認したら
#Agda言語には宇宙の階層
Set : Set1 : Set2 : ...
が用意されている. SetはSet1の元であり,Set1はSet2の元である.
この他の値は全く定義されていないが,帰納的定義(データ型宣言)によって導入することができる.
これらは,論理の符号化において用いられることが多く,初歩のプログラミングでは殆ど必要が生じないと考えられる.
#私自身は最後の一文でスルーしたものと思われる。。。
#まぁどうせ分からなかったわけだけど。
#うーむ
#たとえば、遅延ストリームは高階論理を使って定義される（よく知られている例）のですが、それは初歩的ではないとする立場なのかな
#Agda だと標準ライブラリの Coinductive.agda と Data/Stream.agda に見られるわけですが。
#むしろ高階論理プログラミングだろう！と決意して λProlog や Abella を触るのも一興かと思います。
#遅延ストリーム自体は初歩的かもしれませんが、それをunivere使って論理を構成するのは初歩的ではないのでは？
#少くとも今の私のagda力ではそもそも何をどうすればいいのかまるで想像つかない。
##演算子とかがどこ出身かって M-. で飛ぶんじゃダメです？
#M-.は知らなかった
#ログあがんないですね
#M-. 知らなかった。ありがとう notogawa さん
#ログ？
#freenode#agda
#昨日のやりとりを読もうとおまったのですが
#その後ulfのtutとりあえず読み進めたけど、なんか面白そうではあるものの、理屈が分からないし、どんなことが出来そうか、どんなことに使えそうかがまるで想像できない。
#具体的に何ページの何行みたいなのを教えていただければ。
#IRC freenode #agda の logging が止まっているようなので、ためしにぼくの IRC client の設定を変えて、ログインしている間のログを保存するようにしました。
#Agda の応用例はいくつもあります (Hackage には遠く及ばないけど）
####agdaの応用例でなくuniverseの応用例です。
#たとえば、ulfのtutでは、そのあと総称プログラミングとかhaskellのclass的なものを紹介。
#練習問題ではXMLをなんかやってる。
#これらの例はuniverseを使わないと出来ない？のだのだと思うのですが、universeのどういう能力がそれを可能にしてるのか？
#ようは「これは○○する必要があるからuniverse!#
#universeを使う」みたいなパターンが見えない。
#プログラミングテクニックとして書かれているので、結構色んな場面で使える手筋のようなもんかと思うんですが。
haskell-ja > Archives > 2013/04/23