[Haskell-cafe] more thoughts on "Finally tagless"
carette at mcmaster.ca
Mon Mar 8 21:34:15 EST 2010
Stephen Tetley wrote:
> The finally tagless style is an implementation of the TypeCase pattern
> (Bruno C. d. S. Oliveira and Jeremy Gibbons):
One part of our work does that, yes.
> The authors of the "Finally Tagless" note in the long version of their
> paper that the GADT TypeCase had some problems with non-exhaustive
> pattern matching (last paragraph, page 14) - if I'm understanding it
> correctly, in order to be total, the interpretation function stills
> needs to introduce pattern matching clauses in some circumstances for
> values that the GADT actually prevents occurring.
You understand correctly. By using plain HM, augmented with either type
classes or functors (to pass a higher-order dictionary around), all the
redundant cases can be eliminated in a way that is transparent to the
To me, the parametricity in the 'interpreter' buys you more than what
GADTs do. This was most definitely unexpected.
More information about the Haskell-Cafe