我只是一个业余爱好者，专业不是计算科学与工程。
最近，我做了一个小型的函数式编程语言:https://github.com/mecheng98/nabi
但是 nabi 是无类型的，所以我想为其添加一个类型检查器。
我的一个具体目标是实现一个基于 haskell98 但支持唯一扩展“关联类型同义词”的类型检查器。
我读了这篇论文Associated Type Synonyms然后尝试创建约束蕴涵函数(||-)。
但是我没有做到这一点，因为对我来说太难了(||-)应用推理规则“EQ_subst”而不陷入无限循环。
您能否给我一个提示，让我制作(||-)并教我如何实现我的目标？
+) 我希望代表 THIH 中的类型风格。
非常感谢您阅读我的问题。新年快乐。
最佳答案
I read the paper Associated Type Synonyms right then tried to make the constraint-entailment function (||-).
But I failed to do it, because it is too hard for me to have (||-) apply the inference rule "EQ_subst" and not fall into infinite loop.
这听起来像是尝试直接实现类型规则(图 2)，但仅靠这些并不能提供有效的类型检查过程。本文还提出了一种类型推断算法(第 5 节；图 4、5)，这就是应该实现的算法。要遵循该部分，您可能需要首先很好地掌握 Hindley-Milner 类型推断和统一。
关于haskell - 如何制作约束蕴涵函数(||-)？ (关联类型同义词)，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/59540558/