前に書いた「TypeScript使いの憂鬱：never型はプロパティを持つか」の補足をして、関連する話題を取り上げます。前の記事では
「never型の式にプロパティアクセスができない」という動作は型システムの一貫性から外れた、アドホックな（場当たり的な）動作であるということです。
と書きました。「never型の式にプロパティアクセスができる」という動作が普通の型システムでどのように正当化されるのかを掘り下げます。
TAPLこと「型システム入門」をベースに説明します。
続きを読む「プログラミング」カテゴリーアーカイブ
良いコンパイラーは親切なエラーメッセージを出さなければならない：LunarMLの場合
プログラミング言語の静的解析の良い点として、一回の解析で複数の誤りを検出できる（場合がある）点があります。実行時エラーしか出ない言語だったら、一回の実行で一個のエラーに遭遇して、修正して、またエラーに遭遇して、ということを繰り返さなければなりません。
言い換えると、遭遇した最初の誤りでコンパイルが停止してしまうようなコンパイラーは、いくら静的な型システムを備えていても、動的言語並みの貧弱な開発体験しか得られないということです。コンパイルの手間がかかる分むしろマイナスです。
コンパイラーではなく言語サーバーでも同じことで、ソースコードの最初の誤りで解析が停止してしまう言語サーバーからは貧弱な開発体験しか得られないでしょう。
検出できるエラーの個数だけではなく、エラーメッセージの親切さも、結構開発体験を左右するのではないかと思います。よくある誤りに対して的確なエラーメッセージを出すことができれば、ユーザーがエラーの原因で悩む手間が省けます。
一つの言語仕様に対して複数のコンパイラーが存在する状況で、エラーメッセージの品質はコンパイラー間での差別化の要素になり得ます。この記事では、Standard MLコードに対して良いエラーメッセージを出す工夫について考えてみます。
続きを読むLunarMLとJavaScriptの連携について
定理証明支援系についての問題意識
定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq（旧名Coq）、Agda、Lean、Isabelleなどが有名です。
この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。
続きを読む「関数の副作用の有無」よりも大事なもの
プログラミングをやっていると、「関数に副作用がある」とか「副作用がない」あるいは「純粋である」という話をちょいちょい耳にする。そして、「外界の状態を読み取るけど変更はしない関数」、例えば
function getTime() {
return Date.now();
}のような関数に副作用があるか？みたいな議論が始まったりする。
くだらない議論だ。
何か概念を定義するときは、それが「役に立つ」場面を提示できる必要がある。「関数の副作用」を定義するときは、「関数の副作用」がわかったときに何をしたいのかをはっきりさせる必要がある。「関数のどういう側面に注目したいか」を決めずに「副作用の有無」を論じるのはナンセンスだ。
ここでは、言語処理系（コンパイラー）を実装する者の立場で、関数の副作用について論じてみたい。
続きを読むGHCデバッグ日誌 CI編
Intel SDMの誤植を直してもらった
Intelはコンピューターの頭脳、CPUを作っている会社です。CPUで動作するプログラムを書くためには、プログラムを低レベルな命令の列に変換し、その命令の列を特定の規則に従って変換したバイナリー（機械語）を用意しなければなりません。IntelのCPUが提供する命令や機械語について、Intelが用意しているマニュアルがIntel 64 and IA-32 Architectures Software Developer’s Manual、略してIntel SDMです。
Intel SDMの最新版は「Intel® 64 and IA-32 Architectures Software Developer Manuals」から入手できます。全部合わせて5000ページ以上あります。
Intel SDMも人間が書いているマニュアルなので、時々誤植等があります。容易にそれとわかる誤植なら可愛いものですが、時にはわかりにくいものもあります。
December 2024の版における、CVTSS2SI命令の説明を見てみましょう。これは単精度浮動小数点数（Scalar Single-precision）を符号付き整数（Signed Integer）に変換する命令です。
続きを読むGHCのSIMDサポートの進捗：整数ベクトルの演算
ブログ等にちょいちょい書いていますが、私はこの数ヶ月ほどGHCのSIMDサポートの改善を進めています。
- Haskell/GHCのSIMDについて考える（2023年8月）
- HaskellでEDSLを作る：SIMD編（2024年12月）
- GHCへの私の貢献2024（2024年12月）
- 言語処理系にSIMD命令を実装することについて（主にx86向け）（2025年2月）
この3ヶ月間はx86 NCGで整数のSIMD演算を使えるようにするパッチを書いており、数日前にマージされました。一つのマイルストーンだと思うので記事にしておきます。
続きを読む数学とプログラムはどちらが易しいか／数学とプログラムの違い
最近、某所で「数学とプログラムはどちらが易しいか」という話題が出ました。その場ではあまり上手い返しができなかったので、ブログ記事の題材にして供養します。
もちろん、この質問の答えは人によって違うでしょうし、人によって違うからこそ質問として意味があると言えるでしょう。この記事に書くのは私の見方、私の意見です。
短い答えが欲しい人向けに2択で答えておくと「私にとってはプログラムの方が易しい」となりますが、以下に長い答えを書きます。
続きを読むTypeScript使いの憂鬱：never型はプロパティを持つか
never型とプロパティアクセス
TypeScriptにはneverという型があります。先日も記事にしましたが、簡単に言うとこれは「値を持たない型」です。
never型は、あらゆる型に対してその部分型として振る舞います。例えば、never が number の部分型であることは次のコードでわかります：