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?
haskell continuations continuation-passing
Edit
Report