GADT's - applications and usefulness?

问题:

I'm covering GADT's using learnyouahaskell and I'm interested in their possible uses. I understand that their main characteristic is allowing explicit type setting.

Such as:

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)

Apart from adding additional type safety when working with these data types, what are the other uses of GADT's?

回答1:

Glambda

Richard Eisenberg makes a very compelling case for GADTs in glambda a simply typed lambda calculus interpreter which uses GADTs to make sure ill-typed programs simply cannot be constructed. Phil Wadler has something similar and simpler here, from which the following sample was taken

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

The idea is that the type of the expression (in the interpreter) is encoded in the type of the expression as represented in the Haskell program.

Vectors typed according to their lengths

By using GADTs, we can add a phantom type that tells us keeps track of the length of the vector we have. This package has a nice implementation. This can be reimplemented in a bunch of ways (for example using GHC.TypeLits type-level natural numbers). The interesting data type (copied from the source of the package linked) is

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

Then, I can write a safe version of head' :: Vector a (S n) -> a.

Constraints

I don't have a good example demonstrating the usefulness of this, but you can tack on constraints to individual constructors in the GADT. The constraints you add on the constructors are enforced when you construct something and are available when you pattern match. This lets us do all sorts of fun stuff.

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