A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell
A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell
复制标题
测量单位的类型检查器插件：GHC Haskell 中的特定领域约束求解
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Adam Gundry
中科院分区：
文献类型：
--
作者：
Adam Gundry
正如 F# 巧妙地证明的那样，类型化函数编程和度量单位是自然的组合。然而，在 Haskell 类型系统中对静态检查单元进行编码不可避免地会导致最终系统的可用性令人失望。扩展语言本身会产生更好的结果，但工作量很大！在本文中，我演示了 Glasgow Haskell 编译器中的类型检查器插件如何允许用户定义特定于域的约束求解行为，从而可以将度量单位实现为类型系统扩展，而无需重建编译器。这为 GHC 中约束求解的更加模块化的处理铺平了道路。
Typed functional programming and units of measure are a natural combination, as F# ably demonstrates. However, encoding statically-checked units in Haskell’s type system leads to inevitable disappointment with the usability of the resulting system. Extending the language itself would produce a much better result, but it would be a lot of work! In this paper, I demonstrate how typechecker plugins in the Glasgow Haskell Compiler allow users to define domain-specific constraint solving behaviour, making it possible to implement units of measure as a type system extension without rebuilding the compiler. This paves the way for a more modular treatment of constraint solving in GHC.