|
|
# Generalized Abstract Data Types
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
See [ExtensionDescriptionHowto](extension-description-howto) for information on how to write these extension descriptions. Please add any new extensions to the list of [HaskellExtensions](haskell-extensions).
|
|
|
|
|
|
|
|
|
## Brief Explanation
|
|
|
|
|
|
|
|
|
|
|
|
An alternative syntax for datatypes, giving explicit type signatures for data constructors, generalized by allowing the arguments of the result type to vary, e.g.
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
data Term :: * -> * where
|
|
|
Const :: a -> Term a
|
|
|
Pair :: Term a -> Term b -> Term (a,b)
|
|
|
Fst :: Term (a,b) -> Term a
|
|
|
Snd :: Term (a,b) -> Term b
|
|
|
```
|
|
|
|
|
|
|
|
|
The last two lines also illustrate that these definitions subsume [ExistentialQuantification](existential-quantification), because a type that appears in the argument type of the constructor doesn't appear in the result type of the constructor.
|
|
|
|
|
|
|
|
|
|
|
|
If the type takes advantage of the generalization, any function that matches on it must be given a signature.
|
|
|
|
|
|
|
|
|
|
|
|
However, more specific result types for constructors allows type refinement in pattern matching. For example, in the second branch, we know that a is a pair type, so it is correct to return a pair for that branch.
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
eval :: Term a -> a
|
|
|
eval (Const x) = x
|
|
|
eval (Pair t1 t2) = (eval t1, eval t2)
|
|
|
eval (Fst t1) = fst (eval t1)
|
|
|
eval (Snd t1) = snd (eval t1)
|
|
|
```
|
|
|
|
|
|
## References
|
|
|
|
|
|
|
|
|
- [ GHC Documentation](http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html)
|
|
|
- [ Simple unification-based type inference for GADTs](http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm) by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005.
|
|
|
|
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
<table><tr><th>[\#37](https://gitlab.haskell.org//haskell/prime/issues/37)</th>
|
|
|
<td>add GADTs</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
## Pros
|
|
|
|
|
|
|
|
|
- New syntax for datatypes makes the types of data constructors clear, though may be adopted independently from GADTs. (Convenient for [ExistentialQuantification](existential-quantification))
|
|
|
- permits convenient expression of many properties—-one (baby) step towards dependently-typed languages
|
|
|
|
|
|
## Cons
|
|
|
|
|
|
|
|
|
- relatively new
|
|
|
- even if old-style datatype declarations are removed, that special case remains important, e.g. in saying when function signatures are required.
|
|
|
- complex interactions with type classes |