Initial and Final Embeddings

[This was posted on behalf of Oleg by Walid]

I must confess that I didn't mean to cause so much controversy. My presentation of the initial and final embeddings was intentionally simplified: I removed the parts that were not relevant as far as Ken's paper was concerned. In that simplified introduction, the final embedding indeed looks very much like the `shallow' embedding. However, generally we want to interpret a term in several ways. Therefore, in the full definition, the final embedding includes the parameterization over the 'repr' type, and, crucially, repr is a type constructor.

The extensive discussion of the final embedding can be found in the paper, written with Jacques Carette and Chung-chieh Shan: http://okmij.org/ftp/Computation/tagless-typed.html#tagless-final please also see the JFP paper http://www.cas.mcmaster.ca/~carette/publications/jfp.pdf The paper describes multiple interpretations of the same term in detail. Recently we found that we could express several abstract interpretations and program analyses as instantiations of the final embedding. The related work section of the JFP paper discusses the encoding of terms in elimination form, as a coalgebraic structure, and
the categorical interpretation.

Is the co-algebraic structure final, that is, does it correspond to the terminal object in some category? It seems that could be the case at least in simple cases; for example, see http://okmij.org/ftp/Computation/tagless-typed.html#in-fin Relating Final and Initial typed tagless representations