From 356b0d0f6250f9ebd1d76e8b2a36e787bea3bcb7 Mon Sep 17 00:00:00 2001 From: simonpj Date: Fri, 1 Oct 2004 16:04:23 +0000 Subject: [PATCH] [project @ 2004-10-01 16:04:23 by simonpj] First-cut documentation for GADTs --- ghc/docs/users_guide/glasgow_exts.xml | 103 +++++++++++++++++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml index 36958c9..9733a6f 100644 --- a/ghc/docs/users_guide/glasgow_exts.xml +++ b/ghc/docs/users_guide/glasgow_exts.xml @@ -3291,6 +3291,109 @@ instances is most interesting. + + + +Generalised Algebraic Data Types + +Generalised Algebraic Data Types (GADTs) generalise ordinary algebraic data types by allowing you +to give the type signatures of constructors explicitly. For example: + + data Term a where + Lit :: Int -> Term Int + Succ :: Term Int -> Term Int + IsZero :: Term Int -> Term Bool + If :: Term Bool -> Term a -> Term a -> Term a + Pair :: Term a -> Term b -> Term (a,b) + +Notice that the return type of the constructors is not always Term a, as is the +case with ordinary vanilla data types. Now we can write a well-typed eval function +for these Terms: + + eval :: Term a -> a + eval (Lit i) = i + eval (Succ t) = 1 + eval t + eval (IsZero i) = eval i == 0 + eval (If b e1 e2) = if eval b then eval e1 else eval e2 + eval (Pair e1 e2) = (eval e2, eval e2) + +These and many other examples are given in papers by Hongwei Xi, and Tim Sheard. + + The extensions to GHC are these: + + + Data type declarations have a 'where' form, as exemplified above. The type signature of +each constructor is independent, and is implicitly univerally quantified as usual. Unlike a normal +Haskell data type declaration, the type variable(s) in the "data Term a where" header +have no scope. Indeed, one can write a kind signature instead: + + data Term :: * -> * where ... + +or even a mixture of the two: + + data Foo a :: (* -> *) -> * where ... + +The type variables (if given) may be explicitly kinded, so we could also write the header for Foo +like this: + + data Foo a (b :: * -> *) where ... + + + + +There are no restrictions on the type of the data constructor, except that the result +type must begin with the type constructor being defined. For example, in the Term data +type above, the type of each constructor must end with ... -> Term .... + + + +You cannot use a deriving clause on a GADT-style data type declaration, +nor can you use record syntax. (It's not clear what these constructs would mean. For example, +the record selectors might ill-typed.) However, you can use strictness annotations, in the obvious places +in the constructor type: + + data Term a where + Lit :: !Int -> Term Int + If :: Term Bool -> !(Term a) -> !(Term a) -> Term a + Pair :: Term a -> Term b -> Term (a,b) + + + + +Pattern matching causes type refinement. For example, in the right hand side of the equation + + eval :: Term a -> a + eval (Lit i) = ... + +the type a is refined to Int. (That's the whole point!) +A precise specification of the type rules is beyond what this user manual aspires to, but there is a paper +about the ideas: "Wobbly types: practical type inference for generalised algebraic data types", on Simon PJ's home page. + + The general principle is this: type refinement is only carried out based on user-supplied type annotations. +So if no type signature is supplied for eval, no type refinement happens, and lots of obscure error messages will +occur. However, the refinement is quite general. For example, if we had: + + eval :: Term a -> a -> a + eval (Lit i) j = i+j + +the pattern match causes the type a to be refined to Int (because of the type +of the constructor Lit, and that refinement also applies to the type of j, and +the result type of the case expression. Hence the addition i+j is legal. + + + + + +Notice that GADTs generalise existential types. For example, these two declarations are equivalent: + + data T a = forall b. MkT b (b->a) + data T' a where { MKT :: b -> (b->a) -> T a } + + + + + + -- 1.7.10.4