Typeclass tricks for generalized multi-parameter function lifting

Question

I want to lift a Haskell function into in a higher-order lambda calculus encoding. This is taken almost verbatim from Oleg's Typed Tagless Final encoding.

class Lam r where
  emb :: a -> r a
  (^) :: r (r a -> r a) -> (r a -> r a)
  lam :: (r a -> r a) -> r (r a -> r a)

instance Lam Identity where
  emb   = Identity
  f ^ x = f >>= ($ x)
  lam f = return (f . return =<<) -- call-by-value

 eval = runIdentity

I can embed arbitrary Haskell types into Lam using emb, but I can't use (^) for application then. Further, the lifted functions would behave lazily. Instead, I have to lift them application by application.

emb1 :: ( Applicative r, Lam r ) 
     => (a -> b) -> r (r a -> r b)
emb1 f = lam $ \ra -> f <$> ra

emb2 :: ( Applicative r, Lam r ) 
     => (a -> b -> c) -> r (r a -> r (r b -> r c))
emb2 f = lam $ \ra -> lam $ \rb -> f <$> ra <*> rb

emb3 :: ( Applicative r, Lam r ) 
     => (a -> b -> c -> d) 
     -> r (r a -> r (r b -> r (r c -> r d)))
emb3 f = lam $ \ra -> lam $ \rb -> lam $ \rc -> f <$> ra <*> rb <*> rc

>>> eval $ emb2 (+) ^ emb 1 ^ emb 2
3

That's a lot of boilerplate, though. I'd like to create a generic lifting function that would work for any arity function. I feel like it'd be possible using something akin to Printf's PrintfType or fixed-vector's Cont types. I can specify what I want using type functions

type family   Low    h      o
type instance Low    ()     o =   o
type instance Low    (a, h) o =   a ->    Low    h o

type family   Lift r h      o
type instance Lift r ()     o =   o
type instance Lift r (a, h) o = r a -> r (Lift r h o)

class Emb r h o where
  embed :: Low h o -> r (Lift r h o)

instance ( Lam r ) => Emb r () o where
  embed = emb

instance ( Lam r, Applicative r, Emb r h o ) => Emb r (a, h) o where
  embed = ?

But I get very stuck via this method, usually due to injectivity issues. I was able to resolve injectivity with a truly hideous combination of newtype wrappers and scoped type variables, but it never actually type checked.

Is this possible to express in Haskell?

Hipparchus

I don't know the answer, but next link could be helpful : hackage.haskell.org/package/layers-0.1/docs/… – Overlying

Answer 1

You may want to look at the Ordinary and one-pass CPS transformation in the tagless-final style. The trick is to generalize the Arrow type in the object language. The fact that we often use Haskell's type constructor -> for function types in the object language (to be embedded) is a coincidence and convenience. Generally, object functions do not map to Haskell functions simply. The code in the referred article contains ESymantics

-- How to interpret arrows and other types
type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *

class ESymantics repr where
    int :: Int  -> repr Int
    add :: repr Int  -> repr Int -> repr Int

    lam :: (repr a -> repr b) -> repr (Arr repr a b)
    app :: repr (Arr repr a b) -> repr a -> repr b

Now we have enough freedom to interpret Arr depending on a particular repr. The referred article interpret Arr for the CPS instance.

Edit: In turns out we can achieve the same effect -- redefine the meaning of the arrow for an object language -- without introducing the Arr type (with its injectivity problems) and without ESemantics. The above link, to ordinary and one-pass CPS transformations, shows the new code, using the standard Semantics and re-interpreting the meaning of the function-type constructor. There are no longer any injectivity problems.

Chandless

I looked at this last night and found it to be really informative, but I need to figure out how best to work through the type family non-injectivity. I think I generally was having too great of expectations that Haskell arrows would persist in the object language representation. Thanks for responding! – Hipparchus