日々の流転

λ. 型を返す関数

「型を返す関数」ってのは言い換えれば「値をパラメータとする型」で、ご存じかも知れませんが、一般に依存型(dependent type)と呼ばれてます。Haskell98の型システムでは依存型を直接表現することは出来ませんが、拡張機能を使ってよいのなら HaWiki:SimulatingDependentTypes のような事は一応出来ます(2006-04-23追記: GADT(2004-11-03参照)を使うことも出来ます)。また、Haskellに本物の依存型を追加しようという試みもあることはあって、こっちはJohn Hughesのスライド"Dependent Types in Haskell"(PPT,PDF)を見ると、きっとイメージがわくと思います。

【2006-04-23追記】 依存型を直接サポートする他の関数型言語にはAgda(カテゴリ:agda参照)やEpigram(2004-09-27参照)があります。 また、依存型をサポートする型理論はカリーハワードの同型対応(Curry-Howard isomorphism, Curry-Howard correspondence)によって、ある種の述語論理に対応します。そのような型理論には例えばCC(Calsulus of Construction)やITTがあります。

関連エントリ

• Pattern matching with dependent types.
• Lectures on the Curry-Howard Isomorphism

λ. 萩野服部研合宿

今日明日と修善寺。

λ. 『蕎麦ときしめん』, 清水 義範

を読んだ。