| 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:
fst :: Consumable b => (a,b) %1-> a
fst (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
- newtype UrT m a = UrT (m (Ur a))
- runUrT :: UrT m a %1 -> m (Ur a)
- liftUrT :: (Movable a, Functor m) => m a %1 -> UrT m a
- evalUrT :: Functor m => UrT m a %1 -> m a
- class Consumable a where
- consume :: a %1 -> ()
- class Consumable a => Dupable a where
- dupR :: a %1 -> Replicator a
- dup2 :: a %1 -> (a, a)
- 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)
- dup4 :: Dupable a => a %1 -> (a, a, a, a)
- dup5 :: Dupable a => a %1 -> (a, a, a, a, a)
- dup6 :: Dupable a => a %1 -> (a, a, a, a, a, a)
- dup7 :: Dupable a => a %1 -> (a, a, a, a, a, a, a)
- newtype AsMovable a = AsMovable a
- newtype MovableMonoid a = MovableMonoid a
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
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.
UrT transforms linear control monads to non-linear monads.
UrT (is a non-linear monad with linear state.States) a
liftUrT :: (Movable a, Functor m) => m a %1 -> UrT m a Source #
Lift a computation to the UrT monad, provided that the type a can be used unrestricted.
evalUrT :: Functor m => UrT m a %1 -> m a Source #
Extract the inner computation linearly, the inverse of liftUrT.
evalUrT (liftUrT m) = m
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:
- 1.
first consume (dup2 a) ≃ a ≃ second consume (dup2 a)(dup2neutrality) - 2.
first dup2 (dup2 a) ≃ (second dup2 (dup2 a))(dup2associativity)
where the (≃) sign represents equality up to type isomorphism.
- 3.
dup2 = Replicator.elim (,) . dupR(coherence betweendup2anddupR) - 4.
consume = Replicator.elim () . dupR(coherence betweenconsumeanddupR) - 5.
Replicator.extract . dupR = id(dupRidentity) - 6.
dupR . dupR = (Replicator.map dupR) . dupR(dupRinterchange)
(Laws 1-2 and 5-6 are equivalent)
Implementation of Dupable for Movable types should
be done with deriving via .AsMovable
Implementation of Dupable for other types can be done with
deriving via . Note that at present this mechanism
can have performance problems for recursive parameterized types.
Specifically, the methods will not specialize to underlying GenericallyDupable
instances. See this GHC issue.
Methods
dupR :: a %1 -> Replicator a Source #
Creates a Replicator for the given a.
You usually want to define this method using Replicator's
Applicative instance. For instance, here is an
implementation of Dupable [a]
instance Dupable a => Dupable [a] where dupR [] = pure [] dupR (a : as) = (:) <$> dupR a <*> dupR as
dup2 :: a %1 -> (a, a) Source #
Creates two as from a Dupable a
Instances
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
lseq :: Consumable a => a %1 -> b %1 -> b infixr 0 Source #
Consume the first argument and return the second argument.
This is like seq but the first argument is restricted to be Consumable.
dup4 :: Dupable a => a %1 -> (a, a, a, a) Source #
Creates 4 as from a Dupable a
dup5 :: Dupable a => a %1 -> (a, a, a, a, a) Source #
Creates 5 as from a Dupable a
dup6 :: Dupable a => a %1 -> (a, a, a, a, a, a) Source #
Creates 6 as from a Dupable a
dup7 :: Dupable a => a %1 -> (a, a, a, a, a, a, a) Source #
Creates 7 as from a Dupable a
Newtype that must be used with DerivingVia to get efficient Dupable
and Consumable implementations for Movable types.
Constructors
| AsMovable a |
newtype MovableMonoid a Source #
Constructors
| MovableMonoid a |
Instances
| Monoid a => Monoid (MovableMonoid a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances Methods mempty :: MovableMonoid a # mappend :: MovableMonoid a -> MovableMonoid a -> MovableMonoid a # mconcat :: [MovableMonoid a] -> MovableMonoid a # | |
| Semigroup a => Semigroup (MovableMonoid a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances Methods (<>) :: MovableMonoid a -> MovableMonoid a -> MovableMonoid a # sconcat :: NonEmpty (MovableMonoid a) -> MovableMonoid a # stimes :: Integral b => b -> MovableMonoid a -> MovableMonoid a # | |
| (Movable a, Monoid a) => Monoid (MovableMonoid a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances Methods mempty :: MovableMonoid a Source # | |
| (Movable a, Semigroup a) => Semigroup (MovableMonoid a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances Methods (<>) :: MovableMonoid a %1 -> MovableMonoid a %1 -> MovableMonoid a Source # | |