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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
