Data.Unrestricted.Linear

Ur a represents unrestricted values of type a in a linear context. The key idea is that because the contructor holds a with a regular arrow, a function that uses Ur a linearly can use a however it likes.

someLinear :: Ur a %1-> (a,a)
someLinear (Ur a) = (a,a)

Get an a out of an Ur a. If you call this function on a linearly bound Ur a, then the a you get out has to be used linearly, for example:

restricted :: Ur a %1-> b
restricted x = f (unur x)
  where
    -- f __must__ be linear
    f :: a %1-> b
    f x = ...

Lifts a function on a linear Ur a.

Lifts a function to work on two linear Ur a.

UrT transforms linear control monads to non-linear monads.

• UrT (State s) a is a non-linear monad with linear state.

Linearly unwrap the UrT newtype wrapper.

Lift a computation to the UrT monad, provided that the type a can be used unrestricted.

Extract the inner computation linearly, the inverse of liftUrT.

evalUrT (liftUrT m) = m

The laws of Dupable are dual to those of Monoid:

• 1. first consume (dup2 a) ≃ a ≃ second consume (dup2 a) (dup2 neutrality)

• 2. first dup2 (dup2 a) ≃ (second dup2 (dup2 a)) (dup2 associativity)

where the (≃) sign represents equality up to type isomorphism.

• 3. dup2 = Replicator.elim (,) . dupR (coherence between dup2 and dupR)

• 4. consume = Replicator.elim () . dupR (coherence between consume and dupR)

• 5. Replicator.extract . dupR = id (dupR identity)

• 6. dupR . dupR = (Replicator.map dupR) . dupR (dupR interchange)

(Laws 1-2 and 5-6 are equivalent)

Implementation of Dupable for Data.Unrestricted.Movable types should be done with deriving via Data.Unrestricted.AsMovable.

Implementation of Dupable for other types can be done with deriving via Generically. Note that at present this mechanism can have performance problems for recursive parameterized types. Specifically, the methods will not specialize to underlying Dupable instances. See this GHC issue.

Use Movable a to represent a type which can be used many times even when given linearly. Simple data types such as Bool or [] are Movable. Though, bear in mind that this typically induces a deep copy of the value.

Formally, Movable a is the class of coalgebras of the Ur comonad. That is

• unur (move x) = x

• move @(Ur a) (move @a x) = fmap (move @a) $ move @a x

Additionally, a Movable instance must be compatible with its Dupable parent instance. That is:

• case move x of {Ur _ -> ()} = consume x

• case move x of {Ur x -> (x, x)} = dup2 x

Consume the first argument and return the second argument. This is like seq but the first argument is restricted to be Consumable.

Creates two as from a Dupable a. Same function as dup2.

Creates 3 as from a Dupable a, in a linear fashion.

Creates 4 as from a Dupable a, in a linear fashion.

Creates 5 as from a Dupable a, in a linear fashion.

Creates 6 as from a Dupable a, in a linear fashion.

Creates 7 as from a Dupable a, in a linear fashion.