1

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

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

似乎不适用于拥抱。

  1. GADT 真的不能在 Hugs 中定义吗？我在 Haskell 课堂上的助教说拥抱是可能的，但他似乎不确定。
  2. 如果不能，是否可以使用 Hugs 支持的其他语法或语义对 GADT 进行编码，就像 GADT 可以在 ocaml 中编码一样？
4

2 回答 2

7

GADT 没有在 Hugs 中实现。

相反，如果您尝试使用 GADT 运行代码，则应使用GHC 端口进行 mips 。请注意，由于在更奇特的架构上缺乏字节码加载，您将无法在所有平台上使用 ghci。

于 2012-06-22T14:50:19.390 回答
4

关于您的问题 2（如何在 Haskell 98 中编码 GADT 用例），您可能需要查看 Sulzmann 和 Wang 在 2006 年发表的这篇论文：Haskell 98 中的 GADTless 编程。

就像您所指的 OCaml 工作一样，它通过相等类型分解 GADT 来工作。有多种定义相等类型的方法；他们使用一种类似于 OCaml 的 Leibniz 等式形式，它允许通过 kind 类型运算符的任何应用程序进行替换* -> *。

根据给定类型检查器对 GADT 相等性的推理方式，这可能不足以表达以涵盖 GADT 的所有示例：检查器可能会实现此定义不一定捕获的相等性推理规则。例如，如果只在a*b = c*dkind应用类型构造函数a = c，b = d就不会出现这种形式的分解* -> *。2010 年晚些时候，Oleg 讨论了如何使用类型族通过 Leibniz 等式应用“类型解构器”，从而获得该定义的分解属性——当然这又在 Haskell 98 之外。

对于类型系统设计者来说，这是要牢记的：你的语言对于莱布尼茨等式是否完整，从某种意义上说，它可以表达专门的等式求解器可以做什么？

即使你找到了一个足够表达的相等类型的编码，你也会遇到非常实用的方便问题：当你使用 GADT 时，所有相等见证的使用都是从类型注释中推断出来的。使用这种显式编码，您将有更多工作要做。

最后（没有双关语），GADT 的许多用例都可以通过无标记最终嵌入（同样由 Oleg 再次表示）来表达，IIRC 通常可以在 Haskell 98 中完成。Martin Van Steenbergen的博客文章指出在其回复的评论中是本着这种精神，但奥列格已经大大改进了这种技术。

于 2012-06-24T10:25:05.823 回答