| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Unrestricted.Linear
Description
This module provides essential tools for doing non-linear things in linear code.
Critical Definition: Restricted
In a linear function f :: a %1-> b, the argument a must
be used in a linear way. Its use is restricted while
an argument in a non-linear function is unrestricted.
Hence, a linear function with an argument of Ur a (Ur is short for
unrestricted) can use the a in an unrestricted way. That is, we have
the following equivalence:
(Ur a %1-> b) ≌ (a -> b)
Consumable, Dupable, Moveable classes
Use these classes to perform some non-linear action on linearly bound values.
If a type is Consumable, you can consume it in a linear function that
doesn't need that value to produce it's result:
first :: Consumable b => (a,b) %1-> a
first (a,b) = withConsume (consume b) a
where
withConsume :: () %1-> a %1-> a
withConsume () x = xIf a type is Dupable, you can duplicate it as much as you like.
-- checkIndex ix size_of_array
checkIndex :: Int %1-> Int %1-> Bool
checkIndex ix size = withDuplicate (dup2 ix) size
where
withDuplicate :: (Int, Int) %1-> Int %1-> Bool
withDuplicate (ix,ix') size = (0 <= ix) && (ix < size)
(<) :: Int %1-> Int %1-> Bool
(<) = ...
(<=) :: Int %1-> Int %1-> Bool
(<=) = ...
(&&) :: Bool %1-> Bool %1-> Bool
(&&) = ...If a type is Moveable, you can move it inside Ur
and use it in any non-linear way you would like.
diverge :: Int %1-> Bool
diverge ix = fromMove (move ix)
where
fromMove :: Ur Int %1-> Bool
fromMove (Ur 0) = True
fromMove (Ur 1) = True
fromMove (Ur x) = FalseSynopsis
- data Ur a where
- unur :: Ur a %1 -> a
- lift :: (a -> b) -> Ur a %1 -> Ur b
- lift2 :: (a -> b -> c) -> Ur a %1 -> Ur b %1 -> Ur c
- class Consumable a where
- consume :: a %1 -> ()
- class Consumable a => Dupable a where
- class Dupable a => Movable a where
- lseq :: Consumable a => a %1 -> b %1 -> b
- dup :: Dupable a => a %1 -> (a, a)
- dup3 :: Dupable a => a %1 -> (a, a, a)
- module Data.Unrestricted.Internal.Instances
Unrestricted
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)
Instances
| Functor Ur Source # | |
| Applicative Ur Source # | |
| Foldable Ur Source # | |
Defined in Data.Unrestricted.Internal.Instances Methods fold :: Monoid m => Ur m -> m # foldMap :: Monoid m => (a -> m) -> Ur a -> m # foldMap' :: Monoid m => (a -> m) -> Ur a -> m # foldr :: (a -> b -> b) -> b -> Ur a -> b # foldr' :: (a -> b -> b) -> b -> Ur a -> b # foldl :: (b -> a -> b) -> b -> Ur a -> b # foldl' :: (b -> a -> b) -> b -> Ur a -> b # foldr1 :: (a -> a -> a) -> Ur a -> a # foldl1 :: (a -> a -> a) -> Ur a -> a # elem :: Eq a => a -> Ur a -> Bool # maximum :: Ord a => Ur a -> a # | |
| Traversable Ur Source # | |
| Functor Ur Source # | |
| Applicative Ur Source # | |
| Storable a => Storable (Ur a) Source # | |
| Consumable (Ur a) Source # | |
Defined in Data.Unrestricted.Internal.Instances | |
| Dupable (Ur a) Source # | |
| Movable (Ur a) Source # | |
| Eq a => Eq (Ur a) Source # | |
| Ord a => Ord (Ur a) Source # | |
| KnownRepresentable a => KnownRepresentable (Ur a) Source # | |
Defined in Foreign.Marshal.Pure | |
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 = ...lift2 :: (a -> b -> c) -> Ur a %1 -> Ur b %1 -> Ur c Source #
Lifts a function to work on two linear Ur a.
Performing non-linear actions on linearly bound values
class Consumable a where Source #
Instances
class Consumable a => Dupable a where Source #
The laws of Dupable are dual to those of Monoid:
first consume (dup2 a) ≃ a ≃ second consume (dup2 a)(neutrality)first dup2 (dup2 a) ≃ (second dup2 (dup2 a))(associativity)
Where the (≃) sign represents equality up to type isomorphism.
When implementing Dupable instances for composite types, using dupV
should be more convenient since V has a zipping Applicative instance.
Instances
| Dupable Bool Source # | |
| Dupable Char Source # | |
| Dupable Double Source # | |
| Dupable Int Source # | |
| Dupable Ordering Source # | |
| Dupable () Source # | |
| Dupable Any Source # | |
| Dupable All Source # | |
| Dupable Pool Source # | |
| Dupable a => Dupable [a] Source # | |
| Dupable a => Dupable (Maybe a) Source # | |
| Dupable a => Dupable (Sum a) Source # | |
| Dupable a => Dupable (Product a) Source # | |
| Dupable a => Dupable (NonEmpty a) Source # | |
| Dupable (Ur a) Source # | |
| Dupable (Array a) Source # | |
| Dupable (Vector a) Source # | |
| Dupable (Set a) Source # | |
| (Dupable a, Dupable b) => Dupable (Either a b) Source # | |
| (Dupable a, Dupable b) => Dupable (a, b) Source # | |
| Dupable (HashMap k v) Source # | |
| (Dupable a, Dupable b, Dupable c) => Dupable (a, b, c) Source # | |
class Dupable a => Movable a where Source #
Use Movable aBool or [] are Movable.
Though, bear in mind that this typically induces a deep copy of the value.
Formally, Movable aUr 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 xcase move x of {Ur x -> (x, x)} = dup2 x
Instances
| Movable Bool Source # | |
| Movable Char Source # | |
| Movable Double Source # | |
| Movable Int Source # | |
| Movable Ordering Source # | |
| Movable () Source # | |
Defined in Data.Unrestricted.Internal.Instances | |
| Movable Any Source # | |
| Movable All Source # | |
| Movable a => Movable [a] Source # | |
Defined in Data.Unrestricted.Internal.Instances | |
| Movable a => Movable (Maybe a) Source # | |
| Movable a => Movable (Sum a) Source # | |
| Movable a => Movable (Product a) Source # | |
| Movable a => Movable (NonEmpty a) Source # | |
| Movable (Ur a) Source # | |
| (Movable a, Movable b) => Movable (Either a b) Source # | |
| (Movable a, Movable b) => Movable (a, b) Source # | |
Defined in Data.Unrestricted.Internal.Instances | |
| (Movable a, Movable b, Movable c) => Movable (a, b, c) Source # | |
Defined in Data.Unrestricted.Internal.Instances | |
lseq :: Consumable a => a %1 -> b %1 -> b Source #
Consume the first argument and return the second argument.
This is like seq but the first argument is restricted to be Consumable.