types - System F 的规范实现是什么？

Question

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

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

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

Answer 1

BC Pierce的Types and Programming Languages一书以提供和讨论OCaml 中类型化 lambda 演算的实现而闻名（除其他外） 。

本书提供了 System Ffullpoly的实现，在第 25 章中调用并解释了实现细节。用布尔值fullpoly扩展了简单类型lambda 演算的实现—— simplebool。

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