Mai*_*tor 2 haskell types type-systems functional-programming
我正在研究λ演算的最佳实现.有一个特定的lambda术语子集是非常有效的.它对应于具有固定点的基本仿射逻辑的类型系统.为了测试我对该算法的实现,我必须在该系统上编写适度复杂的术语.没有基础设施,这很困难.我必须使用无类型的lambda演算,然后手动添加类型; 没有检查,统一,没有类型错误.
一个想法是在Haskell中编写程序 - 从其成熟的类型检查器中获益 - 然后转换为EAL.不幸的是,System-Fw和EAL之间存在不匹配.例如,newtype由于缺少类型级别,您无法在Haskell中表达Scott编码的ADT fix.而且,Haskell是一种复杂的语言,编写Haskell->EAl编译器并不是一件容易的事.
有没有快速/脏的方法来获得该系统的工作类型检查器/推理器/统一器 - 或者至少足够接近 - 而不必自己编程？
可能最快捷,最简单的方法是将您的系统作为EDSL嵌入到Haskell中.的最后,无标签的方法可能是理想的和有一个编码直线型系统的示例它.特别是,我建议使用Jeff Polakow的HOAS变体.这将为您提供如下语法:
*Main> :t eval $ llam $ \x -> add x (int 1)
eval $ llam $ \x -> add x (int 1) :: Int -<> Int
这不太可怕.最终,无标记方法的一个方面是你可以对同一个术语有多种解释,所以你可以有一个解释,将术语翻译成代表EAL的某个AST,或者如果你不是,你可以使用一种解释来执行一些额外的类型检查.能够在Haskell的类型系统中捕获所有这些内容.
| 归档时间： |
|
| 查看次数： |
168 次 |
| 最近记录： |