久しぶりにLunarMLの話題です。LunarMLは、私が作っているStandard MLコンパイラーです。
最近は、JavaScriptとの連携に関する機能を追加しています。Webで使えるようにするのと、Promise/async/await周りの統合をいい感じにすることを目標にしています。
続きを読む定理証明支援系についての問題意識
定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq（旧名Coq）、Agda、Lean、Isabelleなどが有名です。
この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。
続きを読む「関数型まつり」に行ってきた
可算選択公理と実数
構成的数学に基づいて解析学を展開し、プログラミングでそれを実装するようなコンテンツを作れないかなあと去年ぐらいから考えています。
構成的数学と一口に言っても、選択公理をどのくらい認めるかによっていくつか流儀があります。Bishopの構成的数学は従属選択公理 (dependent choice) を認めていますが、人によっては可算選択公理 (countable choice) すら使いたくないかもしれません。
Bishop流の構成的数学では、古典数学とそう変わらない実数論が展開されています。これは可算選択公理が使える、という点が大きそうです。
それでは、可算選択公理を仮定しない構成的数学だと実数の概念がどうなるか気になるのが人情だと思います。
続きを読む「関数の副作用の有無」よりも大事なもの
プログラミングをやっていると、「関数に副作用がある」とか「副作用がない」あるいは「純粋である」という話をちょいちょい耳にする。そして、「外界の状態を読み取るけど変更はしない関数」、例えば
function getTime() {
return Date.now();
}のような関数に副作用があるか？みたいな議論が始まったりする。
くだらない議論だ。
何か概念を定義するときは、それが「役に立つ」場面を提示できる必要がある。「関数の副作用」を定義するときは、「関数の副作用」がわかったときに何をしたいのかをはっきりさせる必要がある。「関数のどういう側面に注目したいか」を決めずに「副作用の有無」を論じるのはナンセンスだ。
ここでは、言語処理系（コンパイラー）を実装する者の立場で、関数の副作用について論じてみたい。
続きを読む記事を書くときに気をつけていること、読んでもらうための工夫について
自動車を買った／車は移動を自由にするか
人生をやっていると、大きな出費の瞬間が何回か訪れる。自動車の購入はその一つだ。
私が今住んでいる場所は都会というほどではないが大きな駅の徒歩圏内で、正直言って大人二人で生活する分には自動車はそんなに必要ない。自動車が必要ならカーシェアやレンタカーを使えば良い。だから自動車はこれまで持っていなかった。
しかし、色々あって今回自動車を購入することにした。
続きを読むGHCデバッグ日誌 CI編
技術同人誌執筆の自分の流儀
自分が出している技術系同人誌の執筆の話を書いておく。
続きを読む技術書典18に「作ってわかるTeX言語」を出します
今度の6月1日に池袋で開催される技術同人誌即売会・技術書典18に、サークル「だめぽラボ」として新刊「作ってわかるTeX言語」を出します。既刊も、在庫のあるものは頒布します。
続きを読む