Is there any good resource on real use of Generalized Abstract Data Type?
The example given in the haskell wikibook is too short to give me an insight of the real possibilities of GADT.
Thanks
+1
A:
This is a short answer, but consult the Haskell Wikibook. It walks you though a GADT for a well-typed expression tree, which is a fairly canonical example: http://en.wikibooks.org/wiki/Haskell/GADT
GADTs are also used for implementing type equality: http://hackage.haskell.org/package/type-equality. I can't find the right paper to reference for this offhand -- this technique has made its way well into folklore by now. It is used quite well, however, in Oleg's typed tagless stuff. See, e.g. the section on typed compilation into GADTs. http://okmij.org/ftp/tagless-final/#tc-GADT
sclv
2010-10-04 23:15:25
It's basically 3 times the same example, and as I've told it in my question, it's not satisfactory.
Raoul Supercopter
2010-10-05 08:26:24
Sorry, I didn't realize I was redirecting you to the same link from your question -- for some reason I thought you were referring to the GHC docs. I don't see where you're coming from though. If you need a GADT, you'll probably know. And at that point, the wikibook summarizes pretty much how you would work with one. A more specific question would help.
sclv
2010-10-05 14:19:13
+2
A:
I have found the "Prompt" monad (from the "MonadPrompt" package) a very useful tool in several places (along with the equivalent "Program" monad from the "operational" package. Combined with GADTs (which is how it was intended to be used), it allows you to make embedded languages very cheaply and very flexibly. There was a pretty good article in the Monad Reader issue 15 (http://themonadreader.files.wordpress.com/2010/01/issue15.pdf) called "Adventures in Three Monads" that had a good introduction to the Prompt monad along with some realistic GADTs.
mokus
2010-10-05 14:45:19
+1
A:
I like the example in the GHC manual. It's a quick demo of a core GADT idea: that you can embed the type system of a language you're manipulating into Haskell's type system. This lets your Haskell functions assume, and forces them to preserve, that the syntax trees correspond to well-typed programs.
When we define Term, it doesn't matter what types we choose. We could write
data Term a where
...
IsZero :: Term Char -> Term Char
or
...
IsZero :: Term a -> Term b
and the definition of Term would still go through.
It's only once we want to compute on Term, such as in defining eval, that the types matter. We need to have
...
IsZero :: Term Int -> Term Bool
because we need our recursive call to eval to return an Int, and we want to in turn return a Bool.
keegan
2010-10-08 00:13:51