# Generalised algebraic datatype

### From HaskellWiki

(Difference between revisions)

DonStewart (Talk | contribs) (category language) |
|||

Line 1: | Line 1: | ||

* 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] |
||

+ | |||

+ | == Motivating example == |
||

+ | |||

+ | We will implement an evaluator for a subset of the SK calculus. Note that the K combinator is operationally similar to |
||

+ | <math>\lambda\;x\;y\;.\;x</math> |
||

+ | and, similarly, S is similar to the combinator |
||

+ | <math>\lambda\;x\;y\;\z\;.\;x\;z\;(\;y\;z\;)</math> |
||

+ | which, in simply typed lambda calculus, have types |
||

+ | a -> b -> a |
||

+ | and |
||

+ | (a -> b -> c) -> (a -> b) -> a -> c |
||

+ | Without GADTs we would have to write something like this: |
||

+ | <haskell> |
||

+ | data Term = K | S | :@ Term Term |
||

+ | infixl :@ 6 |
||

+ | <\haskell> |
||

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

+ | <haskell> |
||

+ | 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 :@ |
||

+ | <\haskell> |
||

+ | 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 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.) |
||

== Example == |
== Example == |
||

Line 15: | Line 48: | ||

The more general problem (representing the terms of a language with the terms of another language) can develop surprising things, e.g. ''quines'' (self-replicating or self-representing programs). More details and links on quines can be seen in the section [[Combinatory logic#Self-replication, quines, reflective programming|Self-replication, quines, reflective programming]] of the page [[Combinatory logic]]. |
The more general problem (representing the terms of a language with the terms of another language) can develop surprising things, e.g. ''quines'' (self-replicating or self-representing programs). More details and links on quines can be seen in the section [[Combinatory logic#Self-replication, quines, reflective programming|Self-replication, quines, reflective programming]] of the page [[Combinatory logic]]. |
||

− | [[Category:Language]] |
+ | [[Category:Language]]</haskell> |

## Revision as of 00:26, 2 May 2006

- A short descriptions on generalised algebraic datatypes here as GHC language features
- Another description with links on Haskell' wiki

## Motivating example

We will implement an evaluator for a subset of the SK calculus. Note that the K combinator is operationally similar to
and, similarly, S is similar to the combinator
**Failed to parse (unknown function\z): \lambda\;x\;y\;\z\;.\;x\;z\;(\;y\;z\;)**

which, in simply typed lambda calculus, have types a -> b -> a and (a -> b -> c) -> (a -> b) -> a -> c Without GADTs we would have to write something like this:

data Term = K | S | :@ Term Term infixl :@ 6 <\haskell> With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so: <haskell> 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 :@ <\haskell> 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 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.) == Example == An example: it seems to me that generalised algebraic datatypes can provide a nice solution to a problem described in the documentation of [[Libraries and tools/Database interfaces/HaskellDB|HaskellDB]] project: in Daan Leijen and Erik Meijer's [http://www.haskell.org/haskellDB/doc.html paper] (see PostScript version) on the [http://www.haskell.org/haskellDB/ original HaskellDB] page: making typeful (safe) representation of terms of another language (here: SQL). In this example, the problem has been solved in a funny way with [[Phantom type]] * we make first an untyped language, * and then a typed one on top of it. So we we destroy and rebuild -- is it a nice topic for a myth or scifi where a dreamworld is simulated on top of a previously homogenized world to look like the original? But solving the problem with GADTs seems to be a more direct way (maybe that's why [http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs] mentions that they are also called as ''first-class phantom types''?) == Related concepts == There are other developed tricks with types in [[Type]], and another way to a more general framework in [[Dependent type]]s. Epigram is a fully dependently typed language, and its [http://www.e-pig.org/downloads/epigram-notes.pdf Epigram tutorial] (section 6.1) mentions that Haskell is closely related to Epigram, and attributes this relatedness e.g. exactly to the presence of GADTs. The more general problem (representing the terms of a language with the terms of another language) can develop surprising things, e.g. ''quines'' (self-replicating or self-representing programs). More details and links on quines can be seen in the section [[Combinatory logic#Self-replication, quines, reflective programming|Self-replication, quines, reflective programming]] of the page [[Combinatory logic]]. [[Category:Language]]