# Generalised algebraic datatype

### From HaskellWiki

EndreyMark (Talk | contribs) (Adding link to Existential type at the example where this concept is mentioned) |
EndreyMark (Talk | contribs) (Copying a link from Research papers/Type systems#Generalised Algebraic Data Types to here in section - →Papers: (a paper on translating GADT's to system F)) |
||

Line 1: | Line 1: | ||

+ | == Papers == |
||

+ | |||

+ | See also [[Research papers/Type systems#Generalised Algebraic Data Types|research papers on type systems]]. |
||

+ | |||

* A short descriptions on generalised algebraic datatypes here [http://haskell.org/ghc/docs/latest/html/users_guide/gadt.html as GHC language features]. |
* A short descriptions on generalised algebraic datatypes here [http://haskell.org/ghc/docs/latest/html/users_guide/gadt.html as GHC language features]. |
||

* Another description with links on [http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs Haskell' wiki]. |
* Another description with links on [http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs Haskell' wiki]. |
||

Line 4: | Line 8: | ||

* [http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf Stratified type inference for generalized algebraic data types] by François Pottier and Yann Régis-Gianas. It contains also a lot of links to other papers on GADTs. |
* [http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf Stratified type inference for generalized algebraic data types] by François Pottier and Yann Régis-Gianas. It contains also a lot of links to other papers on GADTs. |
||

* [http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs] by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. (Revised April 2006.) |
* [http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs] by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. (Revised April 2006.) |
||

+ | * [http://www.comp.nus.edu.sg/~sulzmann/simple-translate-gadts.ps Translating Generalized Algebraic Data Types to System F] written by [http://www.comp.nus.edu.sg/~sulzmann/ Martin Sulzmann] and Meng Wang. [http://www.comp.nus.edu.sg/~sulzmann/2005.html Many other papers]. |
||

== Motivating example == |
== Motivating example == |

## Revision as of 07:56, 5 May 2006

## 1 Papers

See also research papers on type systems.

- A short descriptions on generalised algebraic datatypes here as GHC language features.
- Another description with links on Haskell' wiki.
- First-Class Phantom Types by James Cheney and Ralf Hinze
- Stratified type inference for generalized algebraic data types by François Pottier and Yann Régis-Gianas. It contains also a lot of links to other papers on GADTs.
- Simple unification-based type inference for GADTs by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. (Revised April 2006.)
- Translating Generalized Algebraic Data Types to System F written by Martin Sulzmann and Meng Wang. Many other papers.

## 2 Motivating example

Generalised Algebraic Datatypes (GADTs) are datatypes for which a constructor has a non standard type. Indeed, in type systems incorporating GADTs, there are very few restrictions on the type that the data constructors can take. To show you how this could be useful, we will implement an evaluator for the typed SK calculus. Note that the K combinator is operationally similar to and, similarly, S is similar to the combinator which, in simply typed lambda calculus, have types and Without GADTs we would have to write something like this:

data Term = K | S | Term :@ Term infixl 6 :@

With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so:

data Term x where K :: Term (a -> b -> a) S :: Term ((a -> b -> c) -> (a -> b) -> a -> c) Const :: a -> Term a (:@) :: Term (a -> b) -> (Term a) -> Term b infixl 6 :@

now we can write a small step evaluator:

eval::Term a -> Term a eval (K :@ x :@ y) = x eval (S :@ x :@ y :@ z) = x :@ z :@ (y :@ z) eval x = x

Since the types of the so-called object language, being the typed SK calculus, are mimicked by the type system in our meta language, being haskell, we have a pretty convincing argument that the evaluator won't mangle our types. We say that typing is preserved under evaluation (preservation.) Note that this is an argument and not a proof.

This, however, comes at a price: let's see what happens when you try to convert strings into our object language:

parse "K" = K parse "S" = S

you'll get a nasty error like so:

Occurs check: cannot construct the infinite type: c = b -> c Expected type: Term ((a -> b -> c) -> (a -> b) -> a -> b -> c) Inferred type: Term ((a -> b -> c) -> (a -> b) -> a -> c) In the definition of `foo': foo "S" = SOne could, however, reason that parse has type:

## 3 Example with lists

here's another, smaller example:

data Empty data NonEmpty data List x y where Nil :: List a Empty Cons:: a -> List a b -> List a NonEmpty safeHead:: List x NonEmpty -> x safeHead (Cons a b) = a

now safeHead can only be applied to non empty lists, and will never evaluate to bottom. This too comes at a cost; consider the function:

silly 0 = Nil silly 1 = Cons 1 Nil

yields an objection from ghc:

Couldn't match `Empty' against `NonEmpty' Expected type: List a Empty Inferred type: List a NonEmpty In the application `Cons 1 Nil' In the definition of `silly': silly 1 = Cons 1 Nil