前に書いた「TypeScript使いの憂鬱：never型はプロパティを持つか」の補足をして、関連する話題を取り上げます。前の記事では
「never型の式にプロパティアクセスができない」という動作は型システムの一貫性から外れた、アドホックな（場当たり的な）動作であるということです。
と書きました。「never型の式にプロパティアクセスができる」という動作が普通の型システムでどのように正当化されるのかを掘り下げます。
TAPLこと「型システム入門」をベースに説明します。
続きを読む月別アーカイブ: 2025年7月
有限にも無限にもなれない僕らの集合
「集合\(A\)が有限集合であるとは、ある自然数\(n\)に対し、\(A\)と\(\{0,1,\dotsc,n-1\}\)の間に全単射が存在することである。一方、有限集合ではない集合は無限集合である。」
「存在量化子\(\exists\)の有限回の除去は通常の論理でできるので、選択公理が力を発揮するのはもっぱら無限集合が相手の時である。」
……本当にそうだろうか？
「集合は有限集合か無限集合のどちらかだ」という考え方は排中律的であり、構成的数学では考え直す必要がある。
この記事では、「無限」ではないが「有限」とも言えない集合について考えたい。有限集合の定義は最初に書いたものとする。無限集合のちゃんとした定義はしない。
続きを読む良いコンパイラーは親切なエラーメッセージを出さなければならない：LunarMLの場合
プログラミング言語の静的解析の良い点として、一回の解析で複数の誤りを検出できる（場合がある）点があります。実行時エラーしか出ない言語だったら、一回の実行で一個のエラーに遭遇して、修正して、またエラーに遭遇して、ということを繰り返さなければなりません。
言い換えると、遭遇した最初の誤りでコンパイルが停止してしまうようなコンパイラーは、いくら静的な型システムを備えていても、動的言語並みの貧弱な開発体験しか得られないということです。コンパイルの手間がかかる分むしろマイナスです。
コンパイラーではなく言語サーバーでも同じことで、ソースコードの最初の誤りで解析が停止してしまう言語サーバーからは貧弱な開発体験しか得られないでしょう。
検出できるエラーの個数だけではなく、エラーメッセージの親切さも、結構開発体験を左右するのではないかと思います。よくある誤りに対して的確なエラーメッセージを出すことができれば、ユーザーがエラーの原因で悩む手間が省けます。
一つの言語仕様に対して複数のコンパイラーが存在する状況で、エラーメッセージの品質はコンパイラー間での差別化の要素になり得ます。この記事では、Standard MLコードに対して良いエラーメッセージを出す工夫について考えてみます。
続きを読むLunarMLとJavaScriptの連携について
定理証明支援系についての問題意識
定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq（旧名Coq）、Agda、Lean、Isabelleなどが有名です。
この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。
続きを読む