如何使用拥抱GADTs(How to use GADTs in Hugs)

2019-09-18 09:54发布

我想编写不GHCI(即GNU / Linux的上mipsel体系)所支持的平台上交互使用GADTs一个Haskell程序。 问题是,可被用来定义在一个GHC GADT,例如构建体:

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

似乎并不在拥抱的工作。

  1. 不能GADTs真正拥抱界定? 我的TA在哈斯克尔类说,这是可能的拥抱,但他似乎不确定。
  2. 如果没有,可以GADT通过使用支持拥抱其他语法或语义编码,就像GADTs在ocaml的编码?

Answer 1:

GADTs没有在拥抱实施。

相反,你应该使用GHC的端口MIPS如果您正试图使用GADTs运行代码。 请注意,您将无法使用ghci的所有平台上,由于对更奇特的结构缺乏字节码加载。



Answer 2:

Regarding your question 2 (how to encode GADT use cases in Haskell 98), you may want to look at this 2006 paper by Sulzmann and Wang: GADTless programming in Haskell 98.

Like the OCaml work you're referring to, this works by factoring GADTs through an equality type. There are various ways to define equality type; they use a form of Leibniz equality like for OCaml, which allows to substitute through any application of a type operator at kind * -> *.

Depending on how a given type checker reason about GADT equalities, this may not be expressive enough to cover all examples of GADTs: the checker may implement equality reasoning rules that are not necessarily captured by this definition. For example, a*b = c*d implies a = c and b = d: this form of decomposition does not come if you only apply type constructors at kind * -> *. Later in 2010, Oleg discussed how you can use type families to apply "type deconstructors" through Leibniz equality, gaining decomposition properties for this definition -- but of course this is again outside Haskell 98.

That's something to keep in mind for type system designers: is your language complete for leibniz equality, in the sense that it can express what a specialized equality solver can do?

Even if you find an encoding of the equality type that is expressive enough, you will have very practical convenience issues: when you use GADTs, all uses of equality witness are inferred from type annotations. With this explicit encoding you'll have much more work to do.

Finally (no pun intended), a lot of use cases of GADTs can be equally expressed by tagless-final embeddings (again by Oleg), that IIRC can often be done in Haskell 98. The blog post by Martin Van Steenbergen that dons points to in its reply's comment is in this spirit, but Oleg has considerably improved this technique.



文章来源: How to use GADTs in Hugs