エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
Haskell+GADTで定理証明 その1: 型レベル自然数の等価性 - keigoiの日記
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
Haskell+GADTで定理証明 その1: 型レベル自然数の等価性 - keigoiの日記
実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全で... 実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないことになっているらしい。やっぱりHaskellを使うものとして型安全性くらいは保証したい。でも、かといって普通のHaskellではうまく型を付けられない。(Typeableクラスのキャストを使っても解決にはならない。) そこで、魔法のGADT。 この型とこの型はぜったい等しいのにーというのが文脈から明らかなとき、それを表現できるのがGADTだ…というのが私の理解。まさしく私のケースにぴったりだ。これを使えばunsafeCoerceなんか要らんかもしれない。 いいかえれば、いわゆる定理証明をGADTつきのHaske