Personal tools

Generalised algebraic datatype

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (Making a link more precise: linking directly to the approporate section of the page instead to the top of the page)
m
Line 1: Line 1:
= General =
 
 
 
* 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]
   
= Example =
+
== Example ==
 
An example: it seems to me that generalised algebraic datatypes can provide a nice solution to a problem described 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]]
 
An example: it seems to me that generalised algebraic datatypes can provide a nice solution to a problem described 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,
 
* we make first an untyped language,
Line 12: Line 10:
 
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''?)
 
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 =
+
== 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.
 
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.
   

Revision as of 03:59, 31 March 2006

1 Example

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

2 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.