haskell - 如何在与 Haskell 的 System-Fw 不匹配的类型系统中进行编程？

Question

我正在研究 λ 演算的最佳实现。 lambda 项有一个非常高效的特定子集。它对应于带有定点的基本仿射逻辑类型系统。为了测试该算法的实现，我必须在该系统上编写适度复杂的术语。如果没有基础设施，这是很困难的。我必须使用无类型 lambda 演算，然后手动添加类型；无需检查、统一、无类型错误。

一个想法是用 Haskell 编写程序 - 受益于其成熟的类型检查器 - 然后转换为 EAL。不幸的是，System-Fw 和 EAL 之间不匹配。例如，由于缺少类型级别的修复，如果没有newtype，您就无法在 Haskell 中表达 Scott 编码的 ADT。此外，Haskell 是一种复杂的语言，编写 Haskell->EAl 编译器并非易事。

是否有任何快速/肮脏的方法来获得该系统的工作类型检查器/推理器/统一器 - 或者至少足够接近的东西 - 而不必自己编程？

Answer 1

可能最快、最简单的方法是将您的系统作为 EDSL 嵌入到 Haskell 中。 finally, tagless方法可能是理想的，并且有一个 example of encoding a linear type system用它。特别是，我建议使用 HOAS variation by Jeff Polakow 。这将为您提供如下语法:

*Main> :t eval $ llam $ \x -> add x (int 1)
eval $ llam $ \x -> add x (int 1) :: Int -<> Int

这并不算太可怕。最后，无标签方法的一个方面是，您可以对同一个术语有多种解释，因此您可以有一种解释将该术语转换为表示 EAL 的某个 AST，或者有一种解释可以执行一些额外的类型检查(如果您不这样做)无法在 Haskell 的类型系统中捕获所有内容。