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.
Documentation
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
Inject regular monads to be monadish things too
some syntactic sugar
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 sigmaa -> taub of the calculus as an arrow type
sigma -> C a b tau.
Incidentally, this notational convention
expresses the rule fun
in AK07
The append example from AK07, section 2.1
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)