[Haskell-cafe] pointers for EDSL design

[Dominique Devriese]

2010/10/12  <oleg at okmij.org>:
>> 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