Data.Unrestricted.Linear.Internal.Ur

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.