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
{-----------------------------------------------------------------------------
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
