Is it possible to convert a HOAS function to continuation passing style?

Question

Mind the following Haskell program:

-- A HOAS term, non-polymorphic for simplicity
data Term
  = Lam (Term -> Term)
  | App Term Term
  | Num Int

-- Doubles every constant in a term
fun0 :: Term -> Term
fun0 (Lam b)   = Lam (\ x -> fun0 (b x))
fun0 (App f x) = App (fun0 f) (fun0 x)
fun0 (Num i)   = Num (i * 2)

-- Same function, using a continuation-passing style
fun1 :: Term -> (Term -> a) -> a
fun1 (Lam b)   cont = undefined
fun1 (App f x) cont = fun1 f (\ f' -> fun1 x (\ x' -> cont (App f' x')))
fun1 (Num i)   cont = cont (Num (i * 2))

-- Sums all nums inside a term
summ :: Term -> Int
summ (Lam b)   = summ (b (Num 0))
summ (App f x) = summ f + summ x
summ (Num i)   = i

-- Example
main :: IO ()
main = do
  let term = Lam $ \ x -> Lam $ \ y -> App (App x (Num 1)) (App y (Num 2))
  print (summ term)                 -- prints 3
  print (summ (fun0 term))          -- prints 6
  print (fun1 term $ \ t -> summ t) -- a.hs: Prelude.undefined 

Here, Term is a (non-polymorphic) λ-term with numeric constants, and fun0 is a function that doubles all constants inside a term. Is it possible to rewrite fun0 in a continuation-passing style? In other words, is it possible to complete the undefined case of the fun1 function such that it behaves identically to fun0 and such that the last print outputs 6?

Answer 1

If you want to convert this function to CPS, you need to also convert the function within the data type:

data Term' a
  = Lam' (Term' a -> (Term' a -> a) -> a)
  | App' (Term' a) (Term' a)
  | Num' Int

Then you can write your fun1 accordingly:

fun1 :: Term' a -> (Term' a -> a) -> a
fun1 (Lam' b)   cont = cont (Lam' (\ x cont' -> b x cont'))
fun1 (App' f x) cont = fun1 f (\ f' -> fun1 x (\ x' -> cont (App' f' x')))
fun1 (Num' i)   cont = cont (Num' (i * 2))

And with the appropriate tweak to summ:

summ' :: Term' Int -> Int
summ' (Lam' b)   = b (Num' 0) summ'
summ' (App' f x) = summ' f + summ' x
summ' (Num' i)   = i

As well as a CPS term:

term' = Lam' $ \ x k -> k $ Lam' $ \ y k' -> k' $ App' (App' x (Num' 1)) (App' y (Num' 2))

You can run the computation just fine:

> fun1 term' summ'
3

Answer 2

If you are trying to define terms in HOAS the way it is usually used, you are doing it wrong. You shouldn't pattern match on the constructors except for in your interpreter. The identity in HOAS looks like:

id2 :: Term
id2 = Lam (\x -> x)

In fact it is pretty common to disallow pattern matching altogether, using an interface like

class HOAS t where
    lam :: (t -> t) -> t
    app :: t -> t -> t

Notice also that the var case is missing -- because vars are always provided as an argument to lam.

The trick in HOAS is to use Haskell's lambda to implement the target language's lambda, so you can essentially write terms in bare lambda calculus (plus some extra syntax).

---

If you must have your question answered, there are lots of ways to do it. Both of your identity functions are not HOAS implementations of the lambda calculus identity function in your target language, but implementations of the Haskell identity function acting on Terms. Your first id0 is literally equal to

id0' :: Term -> Term
id0' = id

And your second is shaping up to be equal to

id1' :: Term -> (Term -> a) -> a
id1' t cont = cont t

(this latter case will differ in strictness, I think)

Notice these have nothing to do with the Term type, so you are just working hard for no reason.

I don't believe it is possible to fill in the missing case of id1 with anything other than

id1 (Lam b) cont = cont (Lam b)

because the Term -> Term does not provide as "escape mechanism" for the a continuation result type -- a could be something that Term cannot represent, such as IO ().