日々の流転

λ. 型レベルプログラミングの会

(以下書きかけ)

参加した。 稲葉さんのまとめ

以下は個人的メモ。

Scala

• 型レベルプログラミングの会 - Onion開発再開しつつある日記(2009-04-18)

チャーチエンコーディングするまえに普通の表現を考えようよw　演算結果の型を type member として表現するのはちょっとC++っぽいな。あと、型レベルVisitorパターンはなるほどという感じだった。

型レベルの再帰の上限を-Yrecursionオプションで指定するという話に対して、「terminationチェッカを使うような方向性はないのか?」という質問をしたが、考えてみたらこの辺りは他の言語でも同じ話だし、開いた関数に対してはあまりうまくいかないのかも知れず。

C++

• 可変引数テンプレートでの型リストまとめ - Faith and Brave - C++で遊ぼう

C++というだけで身構えてたけど、案外わかりやすそうだった。

Haskell

• 型レベルプログラミング会議 - keigoiの日記

今井さんのFunDepsとTCastの説明は分かりやすかった。TCastのココロ「なんでもいいからお前とりあえずマッチさせろ」。 Prologは節のheadとunificationするのに対して、型クラスのインスタンスはheadでmatchingしかしなくて、……

Haskell (type function 派)

• 型レベルプログラミングの会に参加 - 星の贈り物(2009年4月の日記

libolegわろた。

型族はGADTと組み合わせて使えるけど、関数従属性はGADTとうまく相互作用しないというのが、型族の関数従属性に対する優位点として語られているので、shelarcyさんに聞いてみたが、本質的な問題というよりは実装の手間的な感じだった。 本当かな。 どうも、この辺りは私は良くわからないんだよなぁ。 多引数型クラス＋関数従属性と型族の表現力は等価、という話もあるが、理論的に等価にすることは可能としても、実装は違ってるし*1。 (参考: sized-list の append - ヒビルテ(2008-03-08))

shelarcyさんの日記に書かれている 「長さ付きリストに対する型安全な filter 関数は、unsafeCoerce など（邪悪な方法）を使わない限りやはり書けそうにない」という話は、そもそも「型安全な filter 関数とは何か?」というそもそもの問題がきちんと定義されていないように感じた。あるいは、型というのは不変条件を静的に保証するためにあるものなのに、保証したい不変条件は何なのかが決まっていないというか。

D

• <URL:http://www.kmonos.net/pub/Presen/tlp/>
• 型レベルプログラミングの会 - d.y.d.

D言語はこんなに面白い言語だとは知らなかった。static if とか定数畳み込みの保証とかいいな。 あと、「がんばれば、適当にいじっていれば、そのうちコンパイルが通ります」は名言。

依存型

• 型レベルプログラミングの会 - イネムリネズミ日記(2009-04-18)

池上さんの発表は最高だった。ああいう風に人生を楽しめるようになりたい。

AgdaやCoqでは、停止性が構文から明らかでない関数でも、再起呼び出しの引数が整礎な順序関係で減少してることを証明できるなら、定義可能です(参考: Wellfounded induction in Agda2)。 あと、サーバーなどのように停止しないものについては、codataを使ってモデル化するのではないかと思います。 ただし、codataを生成する関数は、再帰が停止する必要が無い代わりに、値がきちんと生成され続けることを保証する必要があります。 (> 末永さん)。

Agdaで外部のProverを使う場合、Proof term を返すのか、それともpostulateと同じでOpaqueな扱いなのか、と聞いたら、両方出来るらしい。この辺りは流石に「Agdaプラグイン機構」(ヒビルテ (2005-09-23))のころとは随分変わっていそうだ。

次世代Nuprl*2というのがあるらしい。 Nuprlって僕の先生が学生だったときからあったような気がするし、しぶとすぎじゃないか。

あと、最近ではRussellとかGuruのように、コードと証明を分離することで依存型をより軽量にしようという試みが、少し流行っているような印象が個人的にはあったが、その辺りどうなのかなぁ。

Russelのアプローチについては<URL:http://mattam.org/research/publications/Program-ing_in_Coq-proval-090307.pdf>のスライドの絵が分かりやすかったので、以下に引用しておく。

Guruのアプローチについては、<URL:http://cl.cse.wustl.edu/talks/verify07.pdf> が分かりやすかった。

GCaml

• <URL:http://panathenaia.halfmoon.jp/alang/typelevel/>
• <URL:http://d.hatena.ne.jp/ytqwerty/20090422#p1>

.