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

[Jacques Carette]

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.

Jacques