-- 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.
-- See SRTest.hs for the example of answer-type polymorphism of
-- the captured delimited continuation, and of do-notation.
module 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
-- We may also use do-notation, see SRTest.hs
-- 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))
-- To ensure that the captured continuation is answer-type polymorphic,
-- we should define shift as follows, perfectly matching AK07.
-- shift :: ((tau-> forall t. C t t a) -> C s b s) -> C a b tau
-- shift f = C(\k -> unC (f (\tau -> ret (k tau))) id)
-- It means that the type of shift is of Rank 2. We have to use a GHC
-- extension.
-- There is a different way to indicate that the captured
-- continuation is pure: its type should not be monadic.
-- Therefore, we change the definition of shift to read as follows:
shift :: ((tau -> a) -> C s b s) -> C a b tau
shift f = C(\k -> unC (f k) id)
-- The change, albeit slightly deviating from AK07, seems more
-- parsimonious and more perspicuous.
-- One may even define
-- throw k v = ret (k v)
-- as an operation to pass a value to the pure continuation.
-- It is appealing that k may be regarded as a `continuation object', with a
-- special operator throw to apply it.
-- It is quite common in various calculi to treat the variable
-- bound by shift in a special way.
run :: C tau tau tau -> tau
run (C f) = f id
-- The append example from AK07, section 2.1
appnd [] = shift (\k -> ret (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...
-- And is is possible, see SRTest.hs
e1 ^ e2 = e1 >== (\x -> e2 >== (\y -> ret (x++y)))
infixl 1 $$
e1 $$ x = e1 >== (\f -> f x)
fmt to_str = shift(\k -> ret (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"