2010/10/12 :

...

An alternative approach to model sharing at the object level is the technique I use for modelling context-free grammars in my PADL 2011 paper "Explicitly Recursive Grammar Combinators"...  Using ideas from the Multirec generic programming library and some recent Haskell type system extensions (most importantly GADTs and type families), you can do this in a well-typed way for sets of mutually recursive object-level expressions.

I guess you are using what I call `the initial embedding' of an object language. Somehow I prefer the final embedding.

No. In the library, I use both embedding styles for different purposes, but what I was referring to here (the construction of production rules) is actually implemented using what you call a typed tagless-final embedding. I see the technique as an encoding of *recursion* in a typed tagless final object language in such a way that the recursion is observable in the host language. Suppose you have the following (logically inconsistent ;)) code (in Haskell notation): term1 :: Int term1 = if term2 then 1 else 2 term2 :: Bool term2 = term1 == 2 and you want to model it in the typed tagless final encoding of simply typed lambda calculus from the examples in your online typed tagless final lecture notes [1] extended with implicit arbitrary recursion. Then you could do data Term1 data Term2 data TermDomain ix where Term1 :: TermDomain Term1 Term2 :: TermDomain Term2 data family TermVal ix newtype instance TermVal Term1 = TV1 {unTV1 :: Int} newtype instance TermVal Term2 = TV2 {unTV2 :: Bool} class ExtraSymantics repr where if_ :: repr h Bool -> repr h a -> repr h a -> repr h a eq_int :: repr h Int -> repr h Int -> repr h Bool class RecSymantics repr phi | repr -> phi where ref :: phi ix -> repr h (TermVal ix) terms :: (Functor (repr h), Symantics repr, ExtraSymantics repr, RecSymantics repr TermDomain) => TermDomain ix -> repr h (TermVal ix) terms Term1 = fmap TV1 $ if_ (fmap unTV2 (ref Term2)) (int 1) (int 2) terms Term2 = fmap TV2 $ eq_int (fmap unTV1 (ref Term1)) (int 2) In this way, the embedding models the object language recursion in such a way that the recursion remains observable in the host language because you can implement it the way you want in your RecSymantics instance. Possible needs for this observable recursion could be that you want to do some form of recursion depth-bounded evaluation or some form of static analysis or whatever... Such modifications are fundamentally impossible if you model object language recursion naively using direct host language recursion. For my parsing library, I need these techniques to get a good view on the recursion in the grammar. This allows me perform grammar transformations and analysis. Dominique Footnotes: [1] http://okmij.org/ftp/tagless-final/course/#infin1