Safe Haskell | None |
---|---|
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 = x
If 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) = False
Synopsis
- 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 :: Type -> Type) 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
.
newtype UrT (m :: Type -> Type) a Source #
UrT
transforms linear control monads to non-linear monads.
UrT (
is a non-linear monad with linear state.State
s) 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
Consumable All Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Any Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Void Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Int16 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Int32 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Int64 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Int8 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Word16 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Word32 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Word64 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Word8 Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable Ordering Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Pool Source # | |
Defined in Foreign.Marshal.Pure.Internal | |
Consumable () Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Bool Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Char Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Double Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Float Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Int Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable Word Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (First a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Last a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (First a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Last a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Max a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Min a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (WrappedMonoid a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable Methods consume :: WrappedMonoid a %1 -> () Source # | |
Consumable a => Consumable (Dual a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Product a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Sum a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (NonEmpty a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Generic a, GConsumable (Rep a)) => Consumable (Generically a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable Methods consume :: Generically a %1 -> () Source # | |
Consumable (Array a) Source # | |
Defined in Data.Array.Mutable.Linear.Internal | |
Consumable (Replicator a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable Methods consume :: Replicator a %1 -> () Source # | |
Consumable (Set a) Source # | |
Defined in Data.Set.Mutable.Linear.Internal | |
Movable a => Consumable (AsMovable a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable (Ur a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable (Vector a) Source # | |
Defined in Data.Vector.Mutable.Linear.Internal | |
Consumable a => Consumable (Vector a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Maybe a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable (Solo a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable a => Consumable [a] Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Consumable e, Consumable a) => Consumable (Either e a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Consumable a, Consumable b) => Consumable (Arg a b) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable (HashMap k v) Source # | |
Defined in Data.HashMap.Mutable.Linear.Internal | |
(KnownNat n, Consumable a) => Consumable (V n a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
Consumable (V 0 a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Instances | |
(Consumable a, Consumable b) => Consumable (a, b) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable (f a) => Consumable (Ap f a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
Consumable (f a) => Consumable (Alt f a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Consumable a, Consumable b, Consumable c) => Consumable (a, b, c) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Consumable a, Consumable b, Consumable c, Consumable d) => Consumable (a, b, c, d) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable | |
(Consumable a, Consumable b, Consumable c, Consumable d, Consumable e) => Consumable (a, b, c, d, e) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Consumable |
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)
(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 betweendup2
anddupR
) - 4.
consume = Replicator.elim () . dupR
(coherence betweenconsume
anddupR
) - 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 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 Generically
Dupable
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 a
s from a
, in a linear fashion.Dupable
a
Instances
Dupable All Source # | |
Dupable Any Source # | |
Dupable Int16 Source # | |
Dupable Int32 Source # | |
Dupable Int64 Source # | |
Dupable Int8 Source # | |
Dupable Word16 Source # | |
Dupable Word32 Source # | |
Dupable Word64 Source # | |
Dupable Word8 Source # | |
Dupable Ordering Source # | |
Dupable Pool Source # | |
Dupable () Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable | |
Dupable Bool Source # | |
Dupable Char Source # | |
Dupable Double Source # | |
Dupable Float Source # | |
Dupable Int Source # | |
Dupable Word Source # | |
Dupable a => Dupable (Product a) Source # | |
Dupable a => Dupable (Sum a) Source # | |
Dupable a => Dupable (NonEmpty a) Source # | |
(Generic a, GDupable (Rep a)) => Dupable (Generically a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable Methods dupR :: Generically a %1 -> Replicator (Generically a) Source # dup2 :: Generically a %1 -> (Generically a, Generically a) Source # | |
Dupable (Array a) Source # | |
Dupable (Replicator a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable Methods dupR :: Replicator a %1 -> Replicator (Replicator a) Source # dup2 :: Replicator a %1 -> (Replicator a, Replicator a) Source # | |
Dupable (Set a) Source # | |
Movable a => Dupable (AsMovable a) Source # | |
Dupable (Ur a) Source # | |
Dupable (Vector a) Source # | |
Dupable a => Dupable (Maybe a) Source # | |
Dupable a => Dupable (Solo a) Source # | |
Dupable a => Dupable [a] Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable | |
(Dupable a, Dupable b) => Dupable (Either a b) Source # | |
Dupable (HashMap k v) Source # | |
(KnownNat n, Dupable a) => Dupable (V n a) Source # | |
(Dupable a, Dupable b) => Dupable (a, b) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable | |
(Dupable a, Dupable b, Dupable c) => Dupable (a, b, c) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable | |
(Dupable a, Dupable b, Dupable c, Dupable d) => Dupable (a, b, c, d) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable | |
(Dupable a, Dupable b, Dupable c, Dupable d, Dupable e) => Dupable (a, b, c, d, e) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Dupable |
class Dupable a => Movable a where Source #
Use
to represent a type which can be used many times even
when given linearly. Simple data types such as Movable
aBool
or []
are Movable
.
Though, bear in mind that this typically induces a deep copy of the value.
Formally,
is the class of
coalgebras of the
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 x
case move x of {Ur x -> (x, x)} = dup2 x
Instances
Movable All Source # | |
Movable Any Source # | |
Movable Int16 Source # | |
Movable Int32 Source # | |
Movable Int64 Source # | |
Movable Int8 Source # | |
Movable Word16 Source # | |
Movable Word32 Source # | |
Movable Word64 Source # | |
Movable Word8 Source # | |
Movable Ordering Source # | |
Movable () Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable | |
Movable Bool Source # | |
Movable Char Source # | |
Movable Double Source # | |
Movable Float Source # | |
Movable Int Source # | |
Movable Word Source # | |
Movable a => Movable (Product a) Source # | |
Movable a => Movable (Sum a) Source # | |
Movable a => Movable (NonEmpty a) Source # | |
(Generic a, GMovable (Rep a)) => Movable (Generically a) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable Methods move :: Generically a %1 -> Ur (Generically a) Source # | |
Movable a => Movable (AsMovable a) Source # | |
Movable (Ur a) Source # | |
Movable a => Movable (Maybe a) Source # | |
Movable a => Movable (Solo a) Source # | |
Movable a => Movable [a] Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable | |
(Movable a, Movable b) => Movable (Either a b) Source # | |
(Movable a, Movable b) => Movable (a, b) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable | |
(Movable a, Movable b, Movable c) => Movable (a, b, c) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable | |
(Movable a, Movable b, Movable c, Movable d) => Movable (a, b, c, d) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable | |
(Movable a, Movable b, Movable c, Movable d, Movable e) => Movable (a, b, c, d, e) Source # | |
Defined in Data.Unrestricted.Linear.Internal.Movable |
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 a
s from a
, in a linear fashion.Dupable
a
dup5 :: Dupable a => a %1 -> (a, a, a, a, a) Source #
Creates 5 a
s from a
, in a linear fashion.Dupable
a
dup6 :: Dupable a => a %1 -> (a, a, a, a, a, a) Source #
Creates 6 a
s from a
, in a linear fashion.Dupable
a
dup7 :: Dupable a => a %1 -> (a, a, a, a, a, a, a) Source #
Creates 7 a
s from a
, in a linear fashion.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 # |