gotoとカリーハワードと限定継続と排中律
いいタイトルが思いつきませんでした・・・
Scalaだとこのあたりにそういう話が
https://github.com/scalaz/scalaz/blob/v7.1.0-M3/core/src/main/scala/scalaz/Forall.scala
http://d.hatena.ne.jp/leque/20111226/p1
続きを読む
-
- いいね！0
Masaki Hara
@qnighy
@___yuni 型は無矛盾だけど正規化性は成立しないってことですよね。もやもやの原因はわかりました。例外は挙動は同じでも型の付き方が違うので古典論理との対応を主張するのは難しそうですね。
2013-10-05 15:59:47
わさびず
@___yuni
@qnighy 単純型付きラムダ計算に例外を入れればいいかというとそうでもなくて型システムをもうちょっと拡張してやる必要があります。scalaはsubtype多相でその辺を頑張ってます。
2013-10-05 16:02:06
Masaki Hara
@qnighy
@___yuni Scalaの例外の型って⊥ですよね。(subtypingは型強制意味論だと思って論理との対応を考えるとすると) 単に矛盾した論理に対応するのでは。
2013-10-05 16:10:03