Control.Linear

A linear type-based I/O system a la Clean.

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 t2 t t3 -> (t2 -> A t1 t3 v) -> A t1 t 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 a1)) (Either (Pair t a) (Pair t a1))

void' :: A t1 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 :: A StdGen Blank Blank

Safe pointer facilities

data Pointer p s t

Instances

Storable (Pointer p s t)

Weakening (Pointer p Foreign t)

Weakening (Pointer p Focused t)

data Freeable

Pointers can be freeable, foreign, or focused. There are the following tradeoffs:

• Freeable pointers support strong update, but can only be split under focusing.
• Foreign 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

Freeable

data Foreign

Constructors

Foreign

Instances

Weakening (Pointer p Foreign 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 () t Blank

Instances

Weakening (Open p)

Weakening (Pointer p Foreign t)

Weakening (Pointer p Focused t)

contraction :: Copyable s => A () (Pointer p s t) (Pair (Pointer p s t) (Pointer p s t))

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

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

free :: A () (Pointer p2 Placeholder t) Blank

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

split :: forall t u p s. (Storable t, Storable u, Copyable 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) (Pair v St)) -> A a (Pair (Pointer p2 s t) u) (Pair (Pair (Pointer p2 s t) v) St)

Focusing on a pointer.

Temporarily turns a freeable pointer into a focused pointer. I get the freeable 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 Freeable 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 Freeable 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

newForeign :: Storable t => t -> A () Blank (Pointer p Foreign t)

Allocate a Foreign pointer.

peek1 :: (Storable t, Copyable s) => A t (Pair (Pointer p s t) St) (Pair (Pointer p s t) St)

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