Personal tools

Generalised algebraic datatype

From HaskellWiki

Revision as of 00:26, 2 May 2006 by Palomer (Talk | contribs)

Jump to: navigation, search

Motivating example

We will implement an evaluator for a subset of the SK calculus. Note that the K combinator is operationally similar to \lambda\;x\;y\;.\;x 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
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 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 [ paper] (see PostScript version) on the [ 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 [ 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 [ 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]].