如何在Hugs中使用GADT

我想编写一个Haskell程序，它在GHCi（即mipsel上的GNU/Linux）不支持的平台上交互使用GADT。问题是，可用于在GHC定义GADT，例如结构：如何在Hugs中使用GADT

data Term a where 
    Lit :: Int -> Term Int 
    Pair :: Term a -> Term b -> Term (a,b) 
    ...

似乎并不在拥抱的工作。

在Hugs中不能定义GADT吗？我在一个哈斯克尔班的助教表示，在拥抱中是可能的，但他似乎并不确定。
如果没有，GADT可以使用Hugs支持的其他语法或语义进行编码，就像GADT可以用ocaml编码一样？

来源

2012-06-22 Pteromys

@ is7s：我该怎么做？目前我用选项'-98'运行拥抱。 – Pteromys

拥抱者 - GHC特定的语言扩展在Hugs中不可用。 –

GADTs并未在Hugs中实现。如果您试图使用GADT运行代码，则应该使用a port of GHC to mips。请注意，由于在更奇特的体系结构上缺少字节码加载，您将无法在所有平台上使用ghci。

来源

2012-06-22 14:50:19

谢谢，我会在完成写代码后使用ghc。然而，当你半途而废时，有一位翻译可能会很有用。你对Haskell'98编码GADTs的问题2有答案吗？ – Pteromys

一些GADT示例可以翻译成类型类，http://martijn.van.steenbergen.nl/journal/2009/11/12/gadts-in-haskell-98/ –

关于你的问题2（如何在Haskell 98中编码GADT用例），你可能想看看2006年的这篇论文：Sulzmann和Wang：GADTless programming in Haskell 98。

就像你指的OCaml工作一样，这个工作通过一个相等类型来分解GADTs。有多种方法可以定义相等类型;他们使用类似于OCaml的Leibniz平等形式，它允许通过* -> *类型的任何类型运算符的应用来进行替换。

根据给定类型检查器有关GADT均等的原因，这可能不足以涵盖GADT的所有示例：检查器可能实现不一定由此定义捕获的平等推理规则。例如，a*b = c*d意味着a = c和b = d：如果仅应用类型构造函数* -> *，则不会出现此分解形式。在2010年后期，Oleg discussed如何使用类型族通过莱布尼兹等式应用“类型解构器”，获得此定义的分解属性 - 但当然这又是在Haskell 98之外。

这是要记住的内容类型系统设计师：您的语言是否完整适用于莱布尼茨平等，因为它可以表达专业平等问题解决者可以做什么？

即使您找到足够表达的相等类型的编码，您也会遇到非常实用的便利问题：当您使用GADT时，从类型注释推断等同见证的所有用法。有了这个明确的编码，你就有更多的工作要做。

最后（不是双关语），很多GADTs的使用情况可以同样受到tagless-final embeddings（再由奥列格）表示，该IIRC往往可以在Haskell 98. blog post由马丁·斯滕贝亨做到这一点穿上点在其答复评论中有这种精神，但Oleg已经大大改进了这项技术。

来源

2012-06-24 10:25:05 gasche

如何在Hugs中使用GADT

回答

相关问题