Typical tricks for lifting a generalized multi-parameter function

Question

I want to raise the Haskell function to a higher order lambda calculus encoding. This is taken almost verbatim from Oleg Tipid without the inscriptions Final Encoding.

class Lam r where emb :: a -> ra (^) :: r (ra -> ra) -> (ra -> ra) lam :: (ra -> ra) -> r (ra -> ra) 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 in Lam using emb , but I cannot use (^) for the application. In addition, the features raised will behave lazily. Instead, I have to pick up their application by application.

 emb1 :: ( Applicative r, Lam r ) => (a -> b) -> r (ra -> rb) emb1 f = lam $ \ra -> f <$> ra emb2 :: ( Applicative r, Lam r ) => (a -> b -> c) -> r (ra -> r (rb -> rc)) emb2 f = lam $ \ra -> lam $ \rb -> f <$> ra <*> rb emb3 :: ( Applicative r, Lam r ) => (a -> b -> c -> d) -> r (ra -> r (rb -> r (rc -> rd))) emb3 f = lam $ \ra -> lam $ \rb -> lam $ \rc -> f <$> ra <*> rb <*> rc >>> eval $ emb2 (+) ^ emb 1 ^ emb 2 3 

These are many patterns. I would like to create a general lift function that will work for any arity function. I feel that it would be possible to use something like Printf PrintfType or fixed-vector Cont types. I can specify what I want using functions like

 type family Low ho type instance Low () o = o type instance Low (a, h) o = a -> Low ho type family Lift rho type instance Lift r () o = o type instance Lift r (a, h) o = ra -> r (Lift rho) class Emb rho where embed :: Low ho -> r (Lift rho) instance ( Lam r ) => Emb r () o where embed = emb instance ( Lam r, Applicative r, Emb rho ) => Emb r (a, h) o where embed = ? 

But I am very stuck with this method, usually due to injection problems. I was able to resolve injectivity with a truly disgusting combination of newtype wrappers and scope type variables, but I never really checked the type.

Can this be expressed in Haskell?

Answer 1

You can take a look at Conventional and single-pass CPS conversion in the style of the decoderless version. The trick is to generalize the type of arrow in the language of objects. The fact that we often use Haskell's constructor type -> for function types in the object language (for embedding) is a coincidence and convenience. Typically, object functions are not just mapped to Haskell functions. The code in this 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 ab) app :: repr (Arr repr ab) -> repr a -> repr b 

We now have enough freedom to interpret Ap, depending on the particular representative. The mentioned article interprets Arr for the CPS instance.

Edit: The result is the same effect - overriding the arrow value for the object language - without introducing the Arr type (with its problems during injection) and without ESemantics. The above link to regular and one-pass CPS conversions shows the new code using standard semantics and reinterpreting the value of a functional type constructor. Injection problems no longer arise.