日々の流転

λ. section

Haskellで中置演算子の部分適用がsectionと呼ばれるのは何故だろうか? カテゴリ論と関係ある?

λ. ヒープ

豊田さんにヒープというデータ構造を教えてもらった。主にPriorityQueueで使うらしい。名前はヒープソートからきてるのかな。

[2005-04-19 追記] 関数型言語でのヒープの実装には Binomial Heap 等がある。Purely Functional Data Structures を参照。

λ. 数学と論理

やっぱり「ならば」の定義はちょっとつまずきやすいよね。

後半に演習を問題をやるときに巡回する予定だったのだけど、そこまで進まずに仕事が無くなってしまった。

それから、現代数学の4本柱は「代数」「位相」「順序」「測度」なのか。

λ. ところで話は変わるのだけど、この授業に限らず、関連する概念が言及されたときに、現在学んでいる事が意外なほど多くの分野に関わっている事を知って興味を増す人と、飛びまくる話に戸惑ってしまう人とがいるのね。

教える側にしてみれば、これを学ぶ事で何が出来るのかというのを教えてあげたいし、一歩先に進んだ高いところからの景色を少しでも見せてあげたいと思うのだろうけど、そのためのトピックで戸惑ってしまう人がいるのは、もうちょっとうまい方法がないかと思ったりする。

λ. ストック経済論

会計学の知識はやはり欲しいな。

λ. アルゴリズム論

だいぶ眠い。しかし「魔女裁判の流れ図」とかは是非見てみたいものだ。

λ. Thread by callcc

callccを使ってThreadもどきを作ったことがある人は多いと思うけど、こんなシンプルに出来るとは知らなかった。

λ. Enumerable::Product

例によって逃避目的。enum-product.rb

λ. 博麗神社 例大祭

に行ってきた。10:30ごろに着いたのだが予想を遥かに越える長蛇の列が出来ててびびった。それでも、開場後15分くらいで中に入れた。カタログも当日買ったし全然事前にチェックしてなかったので、まずは永夜抄の体験版をゲットしてそれから他のサークルをぶらぶらと適当にまわった。12:30ごろには大半のサークルが完売状態だったようなので、そこで撤退。

ゲットしたもの:

『東方永夜抄 〜 Imperishable Night. 体験版Plus』

上海アリス幻樂団

『西行寺庭園厄災録 従者達の硝子細工』

『Thought of Dolls』

葉庭の出店

『東方 - TOUHOU』

VISIONNERZ

『林檎飴』

農村 (味噌煮,ひはる)

『花祀(HANA-MATSURI)』

びいどろぼっくす

『東方勘違い本　ロックでPinkでパンクで玩具で凡愚で瀟洒な僕らのメイド』

みょふ〜会

『幽々子様が見てる』

石津 忠, 浅野 ちこ 日置

『東方奇闘劇』

AQUA STYLE

『冥土行進曲』

チルノ・ピック

Fragile Online

λ. インターネットの進化と可能性 (2)

Fred Baker キター。今ならライブで見れるよ。

• インターネットの進化と可能性 Class Page (SOI)

λ. 『失踪日記』, 吾妻 ひでお

を読んだ。壮絶だなぁ。しかし、失踪してホームレスになっても見捨てないなんて、奥さん良い人ですな。

λ. GHC-6.4ソースコードハッキング

.

λ. 体内時計：「試験管の中で」世界初の成功−−名大教授らグループ

へぇ。そうだったのー。凄いな。

そのうち化学的に時差ぼけを直せたりするようになったらいいな。

• 名古屋大学理学研究科生命理学専攻近藤孝男研究室

λ. Building SVG-based Interactive Web-Estimated System

• <URL:http://www.pfu.fujitsu.com/techreview/no29/pdf/29-8.pdf>

λ. 「Objective Caml NG集 − 型推論とオブジェクト指向の複雑な関係」. Jacques Garrigue

<URL:http://www.math.nagoya-u.ac.jp/~garrigue/papers/ocaml-ng.pdf>

を読んだ。バグの実例が面白い。

λ. ジャンプが読めるのは萩野・服部研だけ!

「ジャンプが読めるのは萩野・服部研だけ!」らしい。 みんな研究室にジャンプを読みにやってきています(ぉぃ

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

(以下書きかけ)

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

以下は個人的メモ。

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>

.