System F 的规范实现是什么？答案

【问题标题】：What is the canonical implementation of System F?System F 的规范实现是什么？
【发布时间】：2016-06-25 02:38:31
【问题描述】：

System F 是在编写原型时简单推理类型的好方法。除了自己实现之外，我还想使用现有的实现。

在寻找实现时，似乎没有 - 我不知道为什么。

我的问题是：System F 的规范实现是什么？

【问题讨论】：

【解决方案1】：

B.C. 的 Types and Programming Languages 书Pierce 因在 OCaml 中提供和讨论 implementations 的类型化 lambda 演算而闻名。

本书提供了 System F 的实现，称为 fullpoly，并在第 25 章中解释了实现细节。fullpoly 扩展了 simply-typed lambda 演算的实现，带有布尔值 -- simplebool。

可以在here找到构建和执行这些类型检查器和解释器的说明。

【讨论】：