[Haskell-cafe] more thoughts on "Finally tagless"

Jacques Carette 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
type system. 

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 mailing list