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

Question

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

一个想法是用 Haskell 编写程序——从其成熟的类型检查器中受益——然后翻译成 EAL。不幸的是，System-Fw 和 EAL 之间存在不匹配。例如，由于缺少类型级别的fix，如果没有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 的类型系统中捕获所有内容。