投稿者「mod_poppo」のアーカイブ

良いコンパイラーは親切なエラーメッセージを出さなければならない:LunarMLの場合

プログラミング言語の静的解析の良い点として、一回の解析で複数の誤りを検出できる(場合がある)点があります。実行時エラーしか出ない言語だったら、一回の実行で一個のエラーに遭遇して、修正して、またエラーに遭遇して、ということを繰り返さなければなりません。

言い換えると、遭遇した最初の誤りでコンパイルが停止してしまうようなコンパイラーは、いくら静的な型システムを備えていても、動的言語並みの貧弱な開発体験しか得られないということです。コンパイルの手間がかかる分むしろマイナスです。

コンパイラーではなく言語サーバーでも同じことで、ソースコードの最初の誤りで解析が停止してしまう言語サーバーからは貧弱な開発体験しか得られないでしょう。

検出できるエラーの個数だけではなく、エラーメッセージの親切さも、結構開発体験を左右するのではないかと思います。よくある誤りに対して的確なエラーメッセージを出すことができれば、ユーザーがエラーの原因で悩む手間が省けます。

一つの言語仕様に対して複数のコンパイラーが存在する状況で、エラーメッセージの品質はコンパイラー間での差別化の要素になり得ます。この記事では、Standard MLコードに対して良いエラーメッセージを出す工夫について考えてみます。

続きを読む

LunarMLとJavaScriptの連携について

久しぶりにLunarMLの話題です。LunarMLは、私が作っているStandard MLコンパイラーです。

最近は、JavaScriptとの連携に関する機能を追加しています。Webで使えるようにするのと、Promise/async/await周りの統合をいい感じにすることを目標にしています。

続きを読む

定理証明支援系についての問題意識

定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq(旧名Coq)、Agda、Lean、Isabelleなどが有名です。

この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。

続きを読む

「関数型まつり」に行ってきた

去る6月14日・15日に東京・中野で開催されたイベント「関数型まつり」に行ってきました。と言っても、14日は地元で予定があったので、参加したのは15日だけです。

関数型まつり

3つの部屋でセッションが同時進行しており、どれも面白そうだったので、分身の術を習得しておかなかったのが悔やまれます。

直接聞いた発表に限らず、資料のみ見た発表についても、いい機会だと思って思ったことを書かせてもらいます。

続きを読む

可算選択公理と実数

構成的数学に基づいて解析学を展開し、プログラミングでそれを実装するようなコンテンツを作れないかなあと去年ぐらいから考えています。

構成的数学と一口に言っても、選択公理をどのくらい認めるかによっていくつか流儀があります。Bishopの構成的数学は従属選択公理 (dependent choice) を認めていますが、人によっては可算選択公理 (countable choice) すら使いたくないかもしれません。

Bishop流の構成的数学では、古典数学とそう変わらない実数論が展開されています。これは可算選択公理が使える、という点が大きそうです。

それでは、可算選択公理を仮定しない構成的数学だと実数の概念がどうなるか気になるのが人情だと思います。

続きを読む

「関数の副作用の有無」よりも大事なもの

プログラミングをやっていると、「関数に副作用がある」とか「副作用がない」あるいは「純粋である」という話をちょいちょい耳にする。そして、「外界の状態を読み取るけど変更はしない関数」、例えば

function getTime() {
    return Date.now();
}

のような関数に副作用があるか?みたいな議論が始まったりする。

くだらない議論だ。

何か概念を定義するときは、それが「役に立つ」場面を提示できる必要がある。「関数の副作用」を定義するときは、「関数の副作用」がわかったときに何をしたいのかをはっきりさせる必要がある。「関数のどういう側面に注目したいか」を決めずに「副作用の有無」を論じるのはナンセンスだ。

ここでは、言語処理系(コンパイラー)を実装する者の立場で、関数の副作用について論じてみたい。

続きを読む

記事を書くときに気をつけていること、読んでもらうための工夫について

少し前(4月)に、「防御力の高い技術ブログを書こう」という記事が話題になった。

防御力の高い技術ブログを書こう – じゃあ、おうちで学べる

便乗というにはいささか時間が経ってしまったが、私も記事を書くときに気をつけていることを書いてみようと思う。

続きを読む

自動車を買った/車は移動を自由にするか

人生をやっていると、大きな出費の瞬間が何回か訪れる。自動車の購入はその一つだ。

私が今住んでいる場所は都会というほどではないが大きな駅の徒歩圏内で、正直言って大人二人で生活する分には自動車はそんなに必要ない。自動車が必要ならカーシェアやレンタカーを使えば良い。だから自動車はこれまで持っていなかった。

しかし、色々あって今回自動車を購入することにした。

続きを読む

GHCデバッグ日誌 CI編

私はHaskell処理系であるGHCに趣味で貢献しています。詳しいことは過去の記事を見てください:

今回は、GHCのCIの問題を追求した話をします。前に「GHCデバッグ日誌」という記事を書いたので、今回は「CI編」としました。

続きを読む