liboleg-2010.1.5: An evolving collection of Oleg Kiselyov's Haskell modules

Control.ShiftResetGenuine

Description

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.

Synopsis

# Documentation

```  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 tauSource

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

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 Source

Constructors

 MW FieldsunMW :: m a

Instances

newtype C a b tau Source

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 FieldsunC :: (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 tauSource

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

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

shift.

run :: C tau tau tau -> tauSource

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)