haskell - GADT的用途和实用性？

我正在介绍GADT使用learningyouahaskell的情况，并且对它们的可能用途很感兴趣。我知道它们的主要特征是允许显式类型设置。

如：

data Users a where
  GetUserName :: Int -> Users String
  GetUserId :: String -> Users Int

usersFunction :: Users a -> a
usersFunction (GetUserName id)
   | id == 100      = "Bob"
   | id == 200      = "Phil"
   | otherwise      = "No corresponding user"
usersFunction (GetUserId name)
   | name == "Bob"      = 100
   | name == "Phil"     = 200
   | otherwise          = 0

main = do
   print $ usersFunction (GetUserName 100)

除了在使用这些数据类型时增加其他类型安全性之外，GADT的其他用途是什么？

最佳答案

Glambda

理查德·艾森伯格（Richard Eisenberg）在glambda中使用GADT来确保不能构造出错误类型的程序的简单类型的lambda演算解释器中，对GADT提出了非常有说服力的理由。菲尔·瓦德勒（Phil Wadler）具有相似且更简单的here，从中获取以下示例

data Exp e a where
  Con :: Int -> Exp e Int
  Add :: Exp e Int -> Exp e Int -> Exp e Int
  Var :: Var e a -> Exp e a
  Abs :: Typ a -> Exp (e,a) b -> Exp e (a -> b)
  App :: Exp e (a -> b) -> Exp e a -> Exp e b

这个想法是，表达式的类型（在解释器中）被编码为如Haskell程序中表示的表达式的类型。

根据长度输入的向量

通过使用GADT，我们可以添加幻像类型，该幻像类型告诉我们跟踪所拥有向量的长度。 This包有一个不错的实现。可以通过多种方式重新实现（例如，使用GHC.TypeLits类型级自然数）。有趣的数据类型（从链接的包的源复制）为

data Vector (a :: *) (n :: Nat)  where
  Nil  :: Vector a Z
  (:-) :: a -> Vector a n -> Vector a (S n)

然后，我可以编写一个安全版本的head' :: Vector a (S n) -> a。

约束条件

我没有一个很好的例子来证明这一点的用处，但是您可以在GADT中对各个构造函数施加约束。当构造某些东西时，在构造函数上添加的约束会强制执行，而在进行模式匹配时可用。这使我们可以做各种有趣的事情。

data MyGADT b where
  SomeShowable :: Show a => a -> b -> MyGADT b     -- existential types!
  AMonad :: Monad b => b -> MyGADT b

关于haskell - GADT的用途和实用性？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/39930569/