[Haskell-cafe] GADT and typeclasses [was: Language extensions]

[Philippa Cowderoy]

On Sun, 27 May 2007, oleg at pobox.com wrote:

> 
> Philippa Cowderoy wrote:
> > For example, GADTs let you implement monads as interpreters by defining a
> > datatype representing the abstract syntax tree that describes a
> > computation - you can't get this to type without at a minimum existential
> > types and for many monad operations you need the full power of GADTs to
> > declare a corresponding constructor.
> 
> I'm yet to see the example of that need. I have seen the examples that
> the need for GADT was _claimed_ -- but then it turns out the example
> is implementable without GADT after all.

If I remember correctly, the final result is that the full power of GADTs 
can be obtained via a sufficiently powerful type class mechanism instead. 
I'm not sure this strictly speaking contradicts what I wrote, though it's 
a point worth reiterating.

> Here are a few such
> examples: implementing State monad in a free term algebra
> 
> 	Initial (term) algebra for a state monad
> 	http://www.haskell.org/pipermail/haskell-cafe/2005-January/008241.html
> 
> Implementing an interpreter in HOAS with fix
> 
> 	Even higher-order abstract syntax: typeclasses vs GADT
> 	http://www.haskell.org/pipermail/haskell/2007-January/019012.html
> 

I would say that while these are very much doable, the GADT-based code is 
clearly a lighter-weight encoding and certainly a more natural extension 
of a beginner's techniques for implementing interpreters.

-- 
flippa at flippac.org

"The reason for this is simple yet profound. Equations of the form
x = x are completely useless. All interesting equations are of the
form x = y." -- John C. Baez