The Thoralf plugin: for your fancy type needs
The Thoralf plugin: for your fancy type needs
复制标题
Thoralf 插件：满足您的奇特类型需求
DOI：
10.1145/3242744.3242754
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Eisenberg, Richard A.
中科院分区：
文献类型：
--
作者：
Otwani, Divesh;Eisenberg, Richard A.
许多奇特的类型（例如，广义代数数据类型、类型族）需要类型检查器插件。这些奇特的类型具有具有相等关系的类型索引（例如，类型级别的自然数），使用GHC的内置类型相等性很难或不可能表示。表示这些相等关系的最实用的方法是通过断言相等约束的插件。然而，这样的插件很难编写和推理。在本文中，我们(1)提出了一种关于类型索引的类型检查器插件正确性的形式化推理理论，并且(2)将该理论应用于创建Thoralf，这是一种用于类型索引的通用和可扩展插件，可将GHC约束问题转换为对外部SMT求解器的查询。通过“泛型和可扩展”，我们的意思是扩展Thoralf的限制很小，并且，如果某些类型索引可以编码为SMT排序，那么程序员可以通过提供这个编码函数来扩展Thoralf。
Many fancy types (e.g., generalized algebraic data types, type families) require a type checker plugin. These fancy types have a type index (e.g., type level natural numbers) with an equality relation that is difficult or impossible to represent using GHC's built-in type equality. The most practical way to represent these equality relations is through a plugin that asserts equality constraints. However, such plugins are difficult to write and reason about.In this paper, we (1) present a formal theory of reasoning about the correctness of type checker plugins for type indices, and, (2) apply this theory in creating Thoralf, a generic and extensible plugin for type indices that translates GHC constraint problems to queries to an external SMT solver. By "generic and extensible", we mean the restrictions on extending Thoralf are slight, and, if some type index could be encoded as an SMT sort, then a programmer could extend Thoralf by providing this encoding function.