Continuation passing style representation of types

Question

Suppose we have a monad, defined by return, (>>=) and the set of laws. There is a data type

newtype C m a = C { unC ∷ forall r. (a → m r) → m r }

also known as Codensity. C m a ≅ m a given that m is a Monad, i.e. we can write two functions to ∷ Monad m ⇒ m a → C m a and from ∷ Monad m ⇒ C m a → m a

to ∷ Monad m ⇒ m a → C m a
to t = C $ \f → t >>= f

from ∷ Monad m ⇒ C m a → m a
from = ($ return) . unC

and show that to ∘ from ≡ id and from ∘ to ≡ id by equational reasoning, for example:

from . to =                                  -- by definition of `(.)'
  \x → from (to x) =                         -- by definition of `to'
  \x → from (C $ \f → x >>= f) =             -- by definition of `from'
  \x → ($ return) (unC (C $ \f → x >>= f)) = -- unC . C ≡ id
  \x → ($ return) (\f → x >>= f) =           -- β-reduce
  \x → x >>= return =                        -- right identity law
  \x → x =                                   -- by definition of `id'
  id

So far so good. My questions are

• Given a type and a bunch of laws, how do we construct corresponding isomorphic CPS representation?
• Is this representation unique (I'd guess no)?
• If it's not unique, is there always the most "simple" (in the number of →s for example :) ) one?

Answer 1

No such encoding is Unique

As you posed the question the answer is obviously "no"

a = forall r. (a -> r) -> r
a = forall s. ((forall r. (a -> r) -> r) -> s) -> s

as to which encoding is the smallest...well the underlying type is almost certainly!

Codensity might not be what you want

whats more, although Codensity is fascinating, I don't believe it is isomorphic to the underlying type. from . to = id is the easy direction.

to . from
  = \x -> to (from x)
  = \x -> C $ \f -> (from x) >>= f
  = \x -> C $ \f -> (unC x return) >>= f
  = \(C g) -> C $ \f -> (g return) >>= f

but then you get kinda stuck. The same thing happens when you try to prove a = forall r. (a -> r) -> r but you get saved by the "theorem for free" (there might be a way to do it without this, but the free theorem makes it easy). I know of no corresponding argument for Codensity, and what most papers I have read prove is rather that it preserves >>= and return, that is, if you only construct your C m a using the monadic operations and what you call to then the call to to . from is identity.

If we try hard enough we can even come up with a counter example to the isomorphism

evil :: C Maybe Int
evil = C $ \h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing


 to . from $ evil
  = (\(C g) -> C $ \f -> (g return) >>= f) evil
  = C $ \f -> ((\h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing) return) >>= f
  = C $ \f -> Nothing >>= f

so are these the same?

test 1 = Nothing
test n = Just n

unC evil test
  = Just 2
unC (C $ \f -> Nothing >>= f) test
  = Nothing >>= test
  = Nothing

I might have made a mistake in that derivation. I have not really checked it, but suffice it to say that right now I don't think C m a = m a

Another Kind of CPS

All data can be encoded as untyped lambda functions, a property discovered by Church about 70 years ago. Often we talk about "Church encoding" data structures, although Oleg has suggested that instead, at least in a typed setting, we should talk about "Boehm-Beraducci" encodings. Regardless of what you call it, the idea is

(a,b) = forall r. (a -> b -> r) -> r
Either a b = forall r. (a -> r) -> (b -> r) -> r

at least up to fast and loose reasoning. It should be obvious that this encoding provides a way to encode any ADT as a System F type. This also reveals a way of implementing functional languages: treat everything as closures under the hood, and have pattern matching just be implemented as function application.

Actually, System F even has a way of encoding existential types as universal types

exists a. f a = forall r. (forall a'. f a' -> r) -> r

which turns out to be a very important identity. Among other things, this helps us to think about the relation between type inference for higher rank types and for existential types. Since type inference is decidable up to rank 2 types, type inference is also decidable in a system with rank 1 universals and existentials. Since existential quantification is the basis for modules, this is important stuff.