Control.ShiftResetGenuine

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

class Monadish m where

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

Methods

ret :: tau -> m a a tau

bind :: m b g sigma -> (sigma -> m a b tau) -> m a g tau

Instances

Monadish C

Fortunately, the rule app in AK07 (Fig 3) is expressible as the composition of two binds

Monad m => Monadish (MW m)

newtype MW m p q a

Inject regular monads to be monadish things too

Constructors

MW

Fields

unMW :: m a

Instances

Monad m => Monadish (MW m)

newtype C a b tau

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

Constructors

C

Fields

unC :: (tau -> a) -> b

Instances

Monadish C

Fortunately, the rule app in AK07 (Fig 3) is expressible as the composition of two binds

reset :: C sigma tau sigma -> C a a tau

The rules from AK07 as they are (see Fig 3)

shift :: ((tau -> C t t a) -> C s b s) -> C a b tau

shift.

run :: C tau tau tau -> tau

int :: Int -> String

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)

str :: String -> String