fetburner.core

コアダンプ

2020-12-05から1日間の記事一覧

ML のサブセットの型推論器を Coq で検証する

この記事は言語実装 Advent Calendar 2020 の5日目の記事です. 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実…