haskell - 如何制作约束蕴涵函数（||-）？（关联类型同义词）

我只是一个不主修计算科学与工程的业余爱好者。

最近做了一个微小的函数式编程语言：https ://github.com/mecheng98/nabi

但是 nabi 是无类型的，所以我想给它添加一个类型检查器。

我实现一个基于 haskell98 但支持唯一扩展“关联类型同义词”的类型检查器是一个具体目标。

我立即阅读了Associated Type Synonyms论文，然后尝试制作约束-蕴涵函数 (||-)。

但我没能做到，因为我很难让 (||-) 应用推理规则“EQ_subst”而不陷入无限循环。

您能否给我一个提示（||-）并教我如何实现我的目标？

+) 我希望以THIH风格表示类型。

非常感谢您阅读我的问题。新年快乐。

标签： haskellcompiler-constructiontype-constraints

我立即阅读了 Associated Type Synonyms 论文，然后尝试制作约束-蕴涵函数 (||-)。

但我没能做到，因为我很难让 (||-) 应用推理规则“EQ_subst”而不陷入无限循环。

这听起来像是试图直接实现类型规则（图 2），但仅靠这些并不能提供有效的类型检查过程。该论文还提出了一种类型推断算法（第 5 节；图 4、5），这就是应该实现的。要遵循该部分，您可能需要首先很好地掌握 Hindley-Milner 类型推断和统一。