-- 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"