On Mon, Jan 17, 2011 at 10:36 PM, Tyson Whitehead
On January 17, 2011 19:24:12 Jan-Willem Maessen wrote:
join (CPS f) = CPS $ \k -> unCPS (f id) k
<snip>
Using these definitions, and join = (>>= id), we obtain:
join (CPS cca) = CPS (\k -> cca (\ca -> unCPS ca k))
That is the same. The key is that the final computation here is unCPS ca k. Delaying the application of k (returning unCPS ca and then applying k gives the same result as directly applying unCPS ca k and returning it) we get
join (CPS cca) = CPS (\k -> cca (\ca -> unCPS ca k)) join (CPS cca) = CPS (\k -> cca (\ca -> unCPS ca) k)
Now, delaying the transformation by unCPS (returning ca and then forming unCPS ca gives the same result as directly forming unCPS ca and returning it) we get
join (CPS cca) = CPS (\k -> unCPS (cca (\ca -> ca)) k) join (CPS cca) = CPS (\k -> unCPS (cca id) k)
which brings us back to the above.
How are you defining CPS? In order to use id as a continuation in
these circumstances, you pretty much need
newtype CPS a = CPS { unCPS :: forall w. (a -> w) -> w }
But that's (mostly) isomorphic to the Identity monad (i.e., you can't
define callCC).
The advantage of Jan-Willem's definition is that you can use it with
the more-familiar Cont monad. I'd argue that it's truer to the sense
of continuation passing as well.
--
Dave Menendez