Stephen Tetley wrote:

The finally tagless style is an implementation of the TypeCase pattern (Bruno C. d. S. Oliveira and Jeremy Gibbons):

http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/typecase.pdf

The finally tagless style is slightly more general. The TypeCase paper emphasizes that TypeCase is a pattern to define a _closed_ type-indexed function -- the indexed family is fixed but the collection of functions is extensible. This is in contrast to type classes, where the collection of functions is fixed (by the class declaration) but the indexed family is extensible (more type class instances can be defined at any time). The tagless final approach permits the definition of an extensible family of open type-indexed functions. For example, we can define a `data type' of expressions and extend it at any time with more expression forms *and* more processing functions (e.g., a new way to print or compile an expression). With the tagless final approach, we have the extensibility in both dimensions. I'll be talking about this extensibility at some length in two weeks, at the Spring School on Generic and Indexed Programming.