purescript - PureScript 类型系统名称

Question

PureScript 中使用的类型系统的正确学术名称是什么？我正在寻找有关它的文件和证明它是合理的。

特别是，当人们想要抛出私有异常类型的实例并通过有效的计算将其传递给 catch 处理程序时，类型系统允许将异常作为隐藏的通信通道问题解决，而无需将类型暴露给计算和可能性在那里捕捉它，很高兴确认这是正确的。

Answer 1

PureScript 类型检查器并不特别基于任何一种类型系统。在我实现它时，我从几篇论文中获得了灵感，包括：

• Joshua Dunfield 和 Neelakantan R. Krishnaswami 的“用于高级多态性的完整且简单的双向类型检查”
• “HMF：一流多态性的简单类型推断”，作者 Daan Leijen
• Daan Leijen 的“Koka：使用行多态效果类型进行编程”

没有健全性证明。在某些时候，我有兴趣返回并基于具有健全性保证的某些系统重新实现类型检查器，但最初的目标是生成具有我想要的功能的实用类型系统：行多态性、类型类和等级 N类型。