この記事は言語実装 Advent Calendar 2020 の5日目の記事です．
一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです．
本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証明していて， あとは対象言語を参照で拡張するだけという話もありますが．
続きを読む今年はそれらしきアドベントカレンダーが無いので，この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます． ML って本を正せば定理証明支援系由来ですし．最後にちょっと OCaml を使ってますし．
Coq によって検証された正規表現エンジンは既に存在していて，探せば他にもいくつもあると思うのですが， それらの実装は主として検証の簡単さに重きが置かれており，OCaml のコードを extract して使ってみると実用に堪えないものが多いように思います． 本記事では，以前 OCaml で書いた効率的な実装を Coq に移植して検証します． 加えて，extract によって OCaml のコードを再び生成し， AtCoder の問題に投げてみても TLE にならないことを確認します．
続きを読む今となっては少々昔のことですが，AtCoder Beginner Contest 167のD問題で数列の循環検出が必要になった事がありました（問題の制約的にはダブリングでも解けますが）．
数列の循環検出はナイーブにに実装すると，循環している部分に至るまでの長さを，循環の長さを
とすると
のメモリが必要になってしまいますが，これを
で計算するアルゴリズムとして，フロイドの循環検出法が知られています．
中々巧妙なアルゴリズムなもので，これを実装して本当に循環検出ができているのか少々不安に思うところもありますし，この際Coqで正当性を保証してやりましょう．
OCamlでAtCoderの問題を解くのに昔書いたダイクストラ法の実装を使っていたんですが， どうも定数倍でTLEすることが多く，もどかしい気持ちになることもしばしばでした． 本記事では行儀の良いスタイルに囚われず以前の実装に定数倍高速化を施し，実際のコンテストでの使用に堪える実装を得ることを目標とします．
続きを読むこれは型 Advent Calendar 2019 15日目の記事です． 交差型についてのよく知られた事実——交差型を持つ単純型付きλ計算において，強正規化する項は型付け可能であることを解説します．
続きを読む