Control.Linear

A linear type-based I/O system a la Clean - including a "safe C" (like Cyclone).

This is an alternative to composing monads - one can decompose them into their corresponding comonads, with linear operations for manipulating them. (See Kieburtz, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.5169&rep=rep1&type=pdf)

Documentation

data St

Values representing the real world.

data A t u v

Linear computations are arrows over linear data, but monads over nonlinear data.

Instances

Default a => Category * (A a)

Default a => Arrow (A a)

Default a => ArrowChoice (A a)

data Blank

Instances

Storable Blank

data Pair t u

Instances

(Storable a, Storable b) => Storable (Pair a b)

type Fn t u = A () (Pair t St) (Pair u St)

(>>==) :: A t t1 t3 -> (t -> A t2 t3 v) -> A t2 t1 v infixl 1

Monadic bind (for nonlinear data).

rtn :: t -> A t v v

Monadic return

Algebraic operations

run :: A a St St -> IO a

This setup is from http://cs.ioc.ee/~tarmo/tsem11/jeltsch1602-slides.pdf

It implements some of http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf

bimap :: A t3 t t2 -> A t4 t1 u -> A (t3, t4) (Pair t t1) (Pair t2 u)

assoc1 :: A () (Pair (Pair t t1) u) (Pair t (Pair t1 u))

assoc2 :: A () (Pair t (Pair u1 u)) (Pair (Pair t u1) u)

drop1 :: A () (Pair Blank v) v

drop2 :: A () (Pair v Blank) v

undrop1 :: A () u (Pair Blank u)

undrop2 :: A () t (Pair t Blank)

swap :: A () (Pair u t) (Pair t u)

apply :: A t (Pair (A t t1 v) t1) v

curry :: A t (Pair t1 u) v -> A () t1 (A t u v)

distr :: A () (Pair t (Either a b)) (Either (Pair t a) (Pair t b))

assoc3 :: ((t, t1), t2) -> (t, (t1, t2))

assoc4 :: (t1, (t2, t)) -> ((t1, t2), t)

void' :: A b t v -> A () t v

bimap' :: A () t u -> A () v w -> A () (Pair t v) (Pair u w)

Basic I/O system

data Exclusive

Instances

Storable Exclusive

data Semiclosed

Instances

Storable Semiclosed

data Open p

Instances

Storable (Open p)

Weakening (Open p)

data Placeholder

Constructors

Placeholder

open :: FilePath -> IOMode -> A () St (Pair Exclusive St)

getStdin :: A () Blank (Open p)

getStdout :: A () Blank (Open p)

getStderr :: A () Blank (Open p)

close :: A () (Pair Exclusive St) St

close1 :: A () (Pair Semiclosed St) St

fileSize :: Openhandle h => A Integer (Pair h St) (Pair h St)

setFileSize :: Openhandle t => Integer -> A () (Pair t St) (Pair t St)

eof :: Openhandle h => A Bool (Pair h St) (Pair h St)

seek :: Openhandle t => SeekMode -> Integer -> A () (Pair t St) (Pair t St)

tell :: Openhandle h => A Integer (Pair h St) (Pair h St)

char :: Openhandle h => A Char (Pair h St) (Pair h St)

line :: Openhandle h => A String (Pair h St) (Pair h St)

lookahead :: Openhandle h => A Char (Pair h St) (Pair h St)

contents :: A String (Pair Exclusive St) (Pair Semiclosed St)

putC :: Openhandle t => Char -> A () (Pair t St) (Pair t St)

putS :: Openhandle t => String -> A () (Pair t St) (Pair t St)

random :: Random t => (t, t) -> A t Blank Blank

Safe pointer facilities

data Pointer p s t

Instances

Storable (Pointer p s t)

Weakening (Pointer p Nonlinear t)

Weakening (Pointer p Focused t)

data Linear

Pointers can be linear, nonlinear, or focused. There are the following tradeoffs:

• Linear pointers support strong update, but can only be split under focusing.
• Nonlinear pointers can be split, but do not support strong update.

Placeholders classify pointers that either point to junk or to data that is not allowed to be used (to maintain linearity).

Constructors

Linear

data Nonlinear

Constructors

Nonlinear

Instances

Weakening (Pointer p Nonlinear t)

data Focused

Constructors

Focused

Instances

Weakening (Pointer p Focused t)

data Fix f

With the Fix constructor, I can build data structures of linear data.

Constructors

In (f (Fix f))

fixInj1 :: Pointer p s (Fix f) -> Pointer p s (f (Fix f))

fixInj2 :: Pointer p s (f (Fix f)) -> Pointer p s (Fix f)

class Weakening t where

Methods

weakening :: A () (Pair t St) St

Instances

Weakening (Open p)

Weakening (Pointer p Nonlinear t)

Weakening (Pointer p Focused t)

contraction :: A () (Pointer Nonlinear s t) (Pair (Pointer Nonlinear s t) (Pointer Nonlinear s t))

new :: Storable t => A () St (Pair (Pointer p Placeholder t) St)

Allocate a new linear block (containing junk), Use poke' to initialize it.

free :: A () (Pair (Pointer p2 Placeholder t) St) St

Use peek' to take ownership of the contents of a block before freeing it.

split :: forall t u p s. (Storable t, Storable u, Splittable s) => A () (Pointer p s (Pair t u)) (Pair (Pointer p s t) (Pointer p s u))

Split a pointer to a pair, into a pair of pointers.

ptrSwap :: Storable t => Fn (Pair (Pointer p s t) t) (Pair (Pointer p s t) t)

Focusing

focus :: (forall p. A a (Pair (Pointer p Focused t) u) v) -> A a (Pair (Pointer p s t) u) (Pair (Pointer p s t) v)

Focusing on a pointer.

Temporarily turns a linear pointer into a focused pointer. I get the linear pointer back after all copies have been surrendered (with weakening).

focusHdl :: (forall p. A a (Pair (Open p) t) u) -> A a (Pair Exclusive t) (Pair Exclusive u)

Focusing on a handle.

Strong update

peek' :: Storable t => Fn (Pointer p Linear t) (Pair (Pointer p Placeholder t) t)

Take the data out of a block, making it a placeholder.

poke' :: Storable t => Fn (Pair (Pointer p Placeholder t) t) (Pointer p Linear t)

The reverse operation.

changeType :: forall t u p. (Storable t, Storable u) => A () (Pointer p Placeholder t) (Pointer p Placeholder u)

A placeholder block can change its type.

Operations on nonlinear data / Weak update

newNonlinear :: Storable t => t -> A () Blank (Pointer p Nonlinear t)

Allocate a nonlinear pointer.

peek1 :: Storable t => A t (Pair (Pointer Nonlinear s t) St) (Pair (Pointer Nonlinear s t) St)

poke1 :: Storable t => t -> Fn (Pointer p s t) (Pointer p s t)

Multithreading

fork :: A () St (Pair St St)

Duplicate the world state. This is interpreted as creating a thread.

join' :: A () (Pair St St) St

Sync together two world states.

Example programs

helloWorld :: A () St St

printStuff :: A () St St

concurrent :: A () St St