[Haskell-cafe] Re: Different choice operations in a continuation monad

[Heinrich Apfelmus]

Heinrich Apfelmus wrote:
> Sebastian Fischer wrote:
>
>> For example, the implementation of
>> `callCC` does not type check with your changed data type.
> 
> [snip]
> 
> As for the interaction: what should
> 
>   ((callCC ($ 0) >> mzero) `orElse` return 2) >>= return . (+3)
> 
> be? If the scope of  callCC  should not extend past  orElse , then this
> evaluates to  return 5 . But this choice of scope dictates the type that
> Holger mentioned.
> 
> If the the scope of  callCC  should extend beyond the  orElse , so that
> the whole thing evaluates to  mzero ,  orElse  will have the type of
> mplus . But then, I think that your implementation type  CMaybe  needs
> to be more sophisticated because  orElse  now needs to detect whether
> the argument contains a call to  callCC  or not in order to distinguish
> 
>   ((callCC ($ 0) >> mzero) `orElse` return 2) >>= return . (+3)
> 
>   ==> mzero
> 
> from
> 
>   (mzero `orElse` return 2) >>= return . (+3)
> 
>   ==> return 5

Out of curiosity, I've implemented these semantics with  operational .
Code attached.

Took me a while to figure out how to implement  callCC , but it turns
out to be straightforward if you simply carry around the current
continuation as an additional parameter.

It doesn't seem to be possible to implement this with just the  CMaybe r
a  type, in particular since the implementation I gave cannot be
refunctionalized to said type. In other words, there is probably no
associative operation

    orElse :: CMaybe r a -> CMaybe r a -> CMaybe r a

with identity `mzero` that satisfies the cancellation law. I don't have
a proof, but the argument that it doesn't interact well with the default
implementation of  callCC  seems strong to me.


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com
-------------- next part --------------
{-----------------------------------------------------------------------------
    A small language with both a choice operationa  orElse  and  callCC
    
    In response to
    http://www.haskell.org/pipermail/haskell-cafe/2010-June/079029.html
------------------------------------------------------------------------------}
{-# LANGUAGE GADTs, RankNTypes, TypeSynonymInstances, FlexibleInstances #-}
import Control.Monad.Identity
import Control.Monad

import Control.Monad.Operational

{-----------------------------------------------------------------------------
    Language definition
------------------------------------------------------------------------------}
    -- primitive instructions
data Instruction r a where
    CallCC :: ((forall b. a -> M r b) -> M r a) -> Instruction r a
    Jump   :: M r r -> Instruction r a
    OrElse :: M r a -> M r a -> Instruction r a
    MZero  :: Instruction r a

jump   = singleton . Jump -- not exported, needed to implement  callCC
callCC = singleton . CallCC
orElse m n = singleton (OrElse m n)

instance MonadPlus (ProgramT (Instruction r) Identity) where
    mzero = singleton MZero
    mplus = undefined -- ignore

    -- main type
type M r a = Program (Instruction r) a

    -- examples
example1, example2 :: M Int Int
example1 = ((callCC (\k -> k 0) >> mzero) `orElse` return 2) >>= return . (+3)
example2 = (mzero `orElse` return 2) >>= return . (+3)

{-----------------------------------------------------------------------------
    Interpreter
------------------------------------------------------------------------------}
    -- global interpreter
interpret :: M r r -> Maybe r
interpret m = case (eval return . view) m of
    JumpR mr  -> interpret mr
    ReturnR a -> Just a
    MZeroR    -> Nothing

    -- helper type for the interpreter
data Result r a where
    ReturnR :: a -> Result r a
    MZeroR  :: Result r a
    JumpR   :: M r r -> Result r a

    -- local interpreter
    -- Passes around the current continuation  kk  so that we can 
    -- implement  callCC , but never continues evaluation with  kk
eval :: (a -> M r r) -> ProgramView (Instruction r) a -> Result r a
eval kk (Return a)          = ReturnR a
eval kk (CallCC f   :>>= k) = (eval kk . view) $ f (jump . kk') >>= k
    where kk' = k >=> kk
eval kk (OrElse n m :>>= k) = case (eval kk' . view) n of
        ReturnR a -> (eval kk . view) (k a)
        JumpR  mr -> JumpR mr
        MZeroR    -> (eval kk . view) (m >>= k)
    where kk' = k >=> kk
eval kk (MZero      :>>= k) = MZeroR
eval kk (Jump mr    :>>= k) = JumpR mr