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. 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
On Sun, 27 May 2007, oleg@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@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
oleg@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. 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
Note that this argument can be extended to deny the need of any "sum of products" construction. In other words, even declarations like data Color = Red | Green | Blue can be implemented with typeclasses and without |. Thus, we don't need them... :) The other point is that using existentials for sums has a problem: I think it's impossible to implement many functions that take multiple arguments of the existential type. The example that comes to mind first is (==) :: Statte s a -> Statte s a -> Bool How to implement this? (Besides the fact that it's impossible to implement due to the fact that we'd need an equality on function types, but let's use a different example whose constructors don't store function types.) Regards, apfelmus
participants (3)
-
apfelmus -
oleg＠pobox.com -
Philippa Cowderoy