OCamlで車輪を再発明する

最近研究でCoqぐらいしか書いてないので、リハビリがてらAtCoderで 開かれるコンテストにOCamlで参加して遊んでます。 僕は個人的な趣味もあってOCamlを使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要があるので新鮮な感じですね。

それに伴って有名なアルゴリズムもいくつか実装したので、 ここではそういうアルゴリズムをMLではどう書いたのか紹介したいなと思います。

SMLでコンパイラを書いた

このエントリはML Advent Calendar 2015と言語実装 Advent Calendar 2015の20日目の記事です。 言語実装 Advent Calendar 2015の19日目の記事はh_sakuraiさんのJavaのサブセットコンパイラの作成でした。

GADTを用いた二項ヒープの実装

このエントリはML Advent Calendar 2015の14日目の記事です。 13日目の記事はよんたさんの関数型プログラミングにおける再帰関数の考え方でした。

型推論の健全性の証明

このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。

手続き型言語OCaml

この記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。

Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます。 また、ML系の言語で手続き的に書いたからと言ってその言語の魅力が損なわれるわけではなく、 強い静的型付け、型推論やparametric polymorphismなどの恩恵を受けられるので、むしろ良く設計された手続き型言語のように映る事でしょう。 積極的にMLで手続き的な処理を書いていこうな。

単一化の証明

この記事はTheorem Prover Advent Calendar 2015の7日目のために書かれました。 6日目の記事はmathinkさんのCoq で環のイデアルを作ってみるです。

Coqでちょっと複雑なデータ構造を書こうと思ったらハマった

何となくMinCamlにCoqで証明を付けたいと思い立ったのでOccurrence checkの検証を証明しようと思ったのですが、ちょっとした問題に遭遇したのでメモ。