Duplicator Interpreter with HOAS

Question

In section 2.3 of these really cool notes on tagless final interpreters for DSLs, Oleg Kiselyov shows how to solve the problem of parsing a serialized DSL expression once, and interpreting it multiple times.

Briefly, he shows that "fake first-class polymorphism" with the types

newtype Wrapped = Wrapped (∀ repr. ExpSYM repr ⇒ repr)
fromTree :: String → Either ErrMsg Wrapped

is not satisfactory because it is not extensible: we have to have a different Wrapper/fromTree for every set of constraints on repr. Thus I'm inclined to use his solution of a duplicator interpreter. This question is about how to use that interpreter with HOAS.

Specifically, consider the following language for target language bindings:

class Lam repr where
  lam :: (repr a -> repr b) -> repr (a -> b)
  app :: repr (a -> b) -> repr a -> repr b

I'm having trouble giving a sound instance of the Lam class for my duplicator interpreter. Here's what I have:

data Dup repr1 repr2 a = Dup {unDupA :: repr1 a, unDupB :: repr2 a}

instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
  lam f = Dup (lam $ unDupA . f . flip Dup undefined) (lam $ unDupB . f . Dup undefined)
  app (Dup fa fb) (Dup a b) = Dup (app fa a) (app fb b)

Is there some way to give a recursive instance of Lambda for something like my Dup type that doesn't involve undefined?

I've also tried using the more powerful version of lam from this paper, which permits monadic interpreters with HOAS, though I didn't see how it would help me with my instance for Dup. A solution using either version of lam with HOAS would be great!

---

_{*: Oleg showed how to define a sound instance using de Bruijn indices, but I'm really interested in a solution for HOAS.}

    class Lam repr where
      lam :: repr (a,g) b -> repr g (a -> b)
      app :: repr g (a->b) -> repr g a -> repr g b

    data Dup repr1 repr2 g a = Dup{d1:: repr1 g a, d2:: repr2 g a}

    instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
      lam (Dup e1 e2) = Dup (lam e1) (lam e2)
      app (Dup f1 f2) (Dup x1 x2) = Dup (app f1 x1) (app f2 x2)

Answer 1

This is impossible.

To show an example, I'll first make a very simple instance of Lam:

newtype Id a = Id a

instance Lam Id where
    lam (Id f) = Id (\x -> let Id r = f x in r)
    app (Id f) (Id x) = Id (f x)

Now I'll make a function that operates on Dups:

f :: Dup Id Id Int -> Dup Id Id Int
f (Dup (Id x) (Id y)) = Dup (Id x*y) (Id y)

I would, from a Lam instance, be able to do lam f :: Dup Id Id (Int -> Int). This might look like

Dup (Id (\x -> x*y)) (Id (\y -> y))

which couldn't be made, because y is not available from the x-lambda. (Using undefineds replaces the y with undefined here, throwing run-time errors whenever it doesn't work nicely.) This is not a rare occurrence: it happens any time you use one of the variables in the other's result.

I'm not sure quite what you're asking with the stronger Monad-generalized one, but this happens with other Monads, too: for example, with Maybe, you couldn't turn the following into a Maybe (Int -> Int) because it depends on the value given:

f :: Maybe Int -> Maybe Int
f m = m >>= \x -> if x > 5 then Just x else Nothing

(You could use fromJust on it and hope no one does this, but it's the same as the undefined solution.)

The undefineds only throw an error if the function needs to look at the other variables, though. If you're absolutely certain that it will never be run on anything like this, (e.g. you restrict unwrapping/creation to an extensively-tested hidden-away module,) then the undefined way would work.

Just one more recommendation for it: use a more verbose error message instead of undefined, in case something does go wrong.