GADT的 - 应用和实用性？

Question

我正在使用learnyouahaskell报道GADT,我对它们的可能用途很感兴趣.我知道它们的主要特征是允许显式类型设置.

如:

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的其他用途是什么？

Answer 1

Glambda

Richard Eisenberg在glambda一个简单类型的lambda演算解释器中为GADT做了一个非常引人注目的案例,该解释器使用GADT来确保简单地无法构造不良类型的程序.Phil Wadler 在这里有类似和简单的东西,从中获取以下样本

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,我们可以添加一个幻像类型,告诉我们跟踪我们所拥有的矢量的长度.这个包有一个很好的实现.这可以通过多种方式重新实现(例如使用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