Generalised algebraic datatype

(Difference between revisions)
 Revision as of 00:32, 2 May 2006 (edit)← Previous diff Revision as of 00:35, 2 May 2006 (edit) (undo)Next diff → Line 15: Line 15: data Term = K | S | :@ Term Term data Term = K | S | :@ Term Term - infixl :@ 6 + infixl 6 :@ With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so: With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so: Line 33: Line 33: eval x = x 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.) + 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.) Note that this is an argument and not a proof. - This, however, comes at a price: see what happens when you try to convert strings into our object language: + 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 "K" = K Line 47: Line 47: In the definition of foo': foo "S" = S In the definition of foo': foo "S" = S + One could, however, reason that parse has type: String -> exists a. Term a == Example == == Example ==

1 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 $\lambda\;x\;y\;.\;x$ and, similarly, S is similar to the combinator $\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.) 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" = S

One could, however, reason that parse has type: String -> exists a. Term a

2 Example

An example: it seems to me that generalised algebraic datatypes can provide a nice solution to a problem described in the documentation of 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?)

3 Related concepts

There are other developed tricks with types in Type, and another way to a more general framework in Dependent types. 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 Self-replication, quines, reflective programming of the page Combinatory logic.</haskell>