実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないことになっているらしい。やっぱりHaskellを使うものとして型安全性くらいは保証したい。でも、かといって普通のHaskellではうまく型を付けられない。(Typeableクラスのキャストを使っても解決にはならない。) そこで、魔法のGADT。 この型とこの型はぜったい等しいのにーというのが文脈から明らかなとき、それを表現できるのがGADTだ…というのが私の理解。まさしく私のケースにぴったりだ。これを使えばunsafeCoerceなんか要らんかもしれない。 いいかえれば、いわゆる定理証明をGADTつきのHaske
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
