-- Haskell98!
-- | Implementation of the calculus lambda-sr-let
--
-- > Polymorphic delimited continuations
-- > Asai and Kameyama, APLAS 2007
-- > http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf
-- > hereafter, AK07
--
-- This embedding of the AK07 calculus into Haskell is another
-- proof that AK07 admit type inference algorithm.
-- In all the tests below, all the types are inferred.
module Control.ShiftResetGenuine where
import Prelude hiding ((^))
-- | Parameterized monad. This is almost the same monad used in
-- the Region-IO and TFP07 paper
-- See also
--
-- > Robert Atkey, Parameterised Notions of Computation, Msfp2006
-- > http://homepages.inf.ed.ac.uk/ratkey/param-notions.pdf
--
-- and
--
-- > http://www.haskell.org/pipermail/haskell/2006-December/018917.html
class Monadish m where
ret :: tau -> m a a tau
bind :: m b g sigma -> (sigma -> m a b tau) -> m a g tau
-- | Inject regular monads to be monadish things too
newtype MW m p q a = MW{ unMW:: m a }
instance Monad m => Monadish (MW m) where
ret = MW . return
bind (MW m) f = MW (m >>= unMW . f)
-- | some syntactic sugar
--
infixl 1 +>>
vm1 +>> vm2 = bind vm1 (const vm2)
infixl 1 >==
m >== f = bind m f
-- | The continuation monad parameterized by two answer types
-- We represent the the effectful expression e, whose type is
-- characterized by the judgement
--
-- > Gamma; a |- e:tau; b
--
-- as a parameterized monad C a b tau. We represent an effectful function
-- type sigma/a -> tau/b of the calculus as an arrow type
-- sigma -> C a b tau.
-- Incidentally, this notational `convention' expresses the rule `fun' in AK07
newtype C a b tau = C{unC:: (tau -> a) -> b}
-- | Fortunately, the rule app in AK07 (Fig 3) is expressible as
-- the composition of two binds
instance Monadish C where
ret x = C (\k -> k x)
bind (C f) h = C (\k -> f (\s -> unC (h s) k))
-- | The rules from AK07 as they are (see Fig 3)
reset :: C sigma tau sigma -> C a a tau
reset (C f) = C(\k -> k (f id))
-- | shift.
shift :: ((tau-> C t t a) -> C s b s) -> C a b tau
shift f = C(\k -> unC (f (\tau -> ret (k tau))) id)
run :: C tau tau tau -> tau
run (C f) = f id
-- | The append example from AK07, section 2.1
--
appnd [] = shift (\k -> ret k)
appnd (a:rest) = appnd rest >== (\r' -> ret (a:r'))
-- inferred type
-- appnd :: [t] -> C a ([t] -> C t1 t1 a) [t]
-- It is the same type as described in the paper, after Fig 3.
appnd123 = reset (appnd [1,2,3])
-- :t appnd123
-- appnd123 :: C a a ([Integer] -> C t t [Integer])
test1 = run (appnd123 >== (\f -> f [4,5,6]))
-- [1,2,3,4,5,6]
-- | The sprintf test: Sec 2.3 of AK07
-- The paper argues this test requires both the changing of the answer type
-- and polymorphism (fmt is used polymorphically in stest3)
--
int:: Int -> String
int x = show x
str :: String -> String
str x = x
-- | The do-syntactic sugar would have been nice...
e1 ^ e2 = e1 >== (\x -> e2 >== (\y -> ret (x++y)))
infixl 1 $$
e1 $$ x = e1 >== (\f -> f x)
fmt to_str = shift(\k -> ret (k . to_str))
sprintf p = reset p
stest1 = run $ sprintf (ret "Hello world")
-- "Hello world"
stest2 = run $
sprintf (ret "Hello " ^ fmt str ^ ret "!") $$ "world"
-- "Hello world!"
stest3 = run $
sprintf (ret "The value of " ^ fmt str ^ ret " is " ^ fmt int)
$$ "x" $$ 3
-- "The value of x is 3"
-- The following is the same as stest3, only split into several parts.
-- The aim is to demonstrate that sprintf and the format specification
-- are first-class functions. This is not the case with Haskell's Printf
-- (which isn't even type safe) or OCaml's printf (where the
-- format specification has a weird typing and is not first class).
stest3' = run $ formatter $$ "x" $$ 3
where
-- demonstrate sprintf and format_specification can be passed as arguments
formatter = applyit sprintf format_specification
applyit f x = f x
format_specification = ret "The value of " ^ fmt str ^ ret " is " ^ fmt int
-- "The value of x is 3"