PureScript类型系统名称

Question

PureScript中使用的类型系统的正确学术名称是什么？我正在寻找有关这方面的文件，并证明它是正确的。

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

Answer 1

PureScript类型检查器并不特别基于任何一种类型的系统。我把灵感来自于数篇论文，我实现了它，包括：

• “完整而简单的双向类型检查 为较高等级多态性”约书亚Dunfield和Neelakantan R.瓦米
• “HMF：简单类型推断一流的多态性”的 大安Leijen
• ‘科卡：具有行多态性影响类型的节目’，由大安Leijen

有没有合理性的证明。在某些时候，我会有兴趣回到并重新实现类型检查器，它基于一些有保证的系统，但最初的目标是生成一个具有我想要的特性的实用类型系统：行多态，类型类和等级N类型。