什么是GADT？ [英] What are GADTs?

问题描述

我正在阅读Haskell Wiki上的 GADTs for dummies 页面，我仍然不'了解如何以及为什么要使用它们。作者提供了一个激励性的例子：

  data T a where 
 D1 :: Int  - > T字符串
 D2 :: T Bool 
 D3 ::（a，a） - > T [a] 
  

这段代码究竟做了什么，它为什么有用？

如果这个问题有点过于含糊，可能有一个相关的问题是：GADT可以用来实现成员函数吗？

解决方案

可以说你想模拟一个水果袋。这个包可以有苹果或桔子。所以作为一个很好的haskeller，您可以定义：

  data Bag = Oranges Int |苹果Int 
  

这看起来不错。让我们看看 Bag 类型，而不必查看数据构造函数。仅仅是 Bag 类型可以告诉你是橙色包还是苹果包。那么不是静态的，我的意思是在运行时，一个函数可以匹配 Bag 类型的值来检测它是桔子还是苹果，但是在编译时间/类型检查时间本身，所以一个只适用于苹果包的功能根本无法传递橘子包。

这是GADT可以帮助我们的地方，基本上可以让我们对我们的类型更精确：

  data Orange = ... 
 data Apple =。 ... 
 
数据包a a 
 OrangeBag :: [Orange]  - >包[Orange] 
 AppleBag :: [Apple]  - > Bag [Apple] 
  

现在我可以定义一个只适用于苹果包的函数。

  giveMeApples :: Bag [Apple]  - > ... 
  

I was reading the GADTs for dummies page on the Haskell Wiki, and I still don't understand how and why they should be used. The author provided a motivating example:

data T a where
    D1 :: Int -> T String
    D2 :: T Bool
    D3 :: (a,a) -> T [a]

What exactly does this code do and why is it useful?

If this question is a little too vague, perhaps a related question is: can GADTs be used to implement member functions?

解决方案

Lets say you want to model a Fruit bag. This bag can have apple or oranges. So as a good haskeller you define:

data Bag = Oranges Int | Apples Int

That looks nice. Let's see that Bag type alone without looking at the data constructors. Does Bag type alone gives you any indication whether it is orange bag or apple bag. Well not statically, I mean at runtime a function could pattern match on value of Bag type to detect whether it is oranges or apples but won't it be nice to enforce this at compile time / type check time itself, So that a function that only works with Bag of apples cannot be passed bag of oranges at all.

This is where GADTs can help us, basically allows us to be more precise about our types:

data Orange = ...
data Apple = ....

data Bag a where
    OrangeBag :: [Orange] -> Bag [Orange]
    AppleBag :: [Apple] -> Bag [Apple]

Now I can define a function which only works with bag of apples.

giveMeApples :: Bag [Apple] -> ...

这篇关于什么是GADT？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！