Scalaで論理体系を作る話 - 1. 命題論理その1 - Qiita

Scalaの型システムには興味深い型が存在します。Scalaの型で述語論理を表現できないか、表現できるとしたら集合論をScalaで書けてしまわないだろうか、という興味から、Scala-proofsというプロジェクトを立ち上げて実験をしています。この記事は、Scala-proofsの中で使用する論理体系の表現手法について解説します。 Scalaのバージョン間で細かい話が変わってくるようですが、この記事はScala 2.12を前提とします。また、後述する理由から、Dotty/Scala3への移植性をできるだけ高めるために、Dottyで廃止される(予定?)の以下の機能を極力縛ることにします： 抽象HKT1へのワイルドカード_の適用 例えば、F: * -> *の実装が具体的に与えられていない場合、F[_]は型として違法 存在型 F[A] forSome { type A } 抽象型Tからの型投影T

[zyzy]

Scalaはあとは停止性の証明が出来ればいいんだろうけど……と思っていたけど、これDottyの具体的な型が必要っていうので多少マシに成ったのかな？