Data.Linear.Token

Reexports

Definitions

data World : Type

  An empty type for tagging linear computations that can be wrapped in `IO`

Totality: total
Visibility: public export
Hints:

HasIO (Pure World)

HasIO (Pure World)

Lift1 World IO

0 T1 : Type -> Type

  A linear token used in computations with mutable linear state.
  
  The idea is that mutable state (mutable references, arrays, pointers,
  and so on) can only be accessed in the presence of the linear token
  that was used to create the mutable resource.
  
  The advantage of using linear types over the `ST` monad: They come
  without the (significant) performance overhead of monadic code in
  Idris. Like the `ST` monad, this provides safe resource handling, because
  the function for running linear computations over a `T1` (function
  `run1`) must work with function argument `f` of type
  `forall s . (1 t : T1 s) -> R1 s a`, that is, mutable references cannot
  leak out of the linear computation and remain usable.

Totality: total
Visibility: export

data R1 : Type -> Type -> Type

  The result of a stateful linear computation.
  
  It pairs the result value with a new linear token.

Totality: total
Visibility: public export
Constructor: 

(#) : a -> (1 _ : T1 s) -> R1 s a

mapR1 : (a -> b) -> (1 _ : R1 s a) -> R1 s b

  `R1` is a functor, but since `map` does not have the correct
  quantities, this is what we use instead.

Totality: total
Visibility: export

0 F1 : Type -> Type -> Type

  A linear computation operating on resources `rs` that produces a
  result of type `a` with a new token operating on resources `ss`.

Totality: total
Visibility: public export

0 F1' : Type -> Type

  Convenience alias for `F1 s ()`.

Totality: total
Visibility: public export

unit1 : F1' s

  The dummy action that performs no effect at all.

Totality: total
Visibility: export

mapF1 : (a -> b) -> F1 s a -> F1 s b

  `F1` is a functor, but since it is a function type, we cannot
  implement an interface for it (but see `Control.Monad.Pure`).

Totality: total
Visibility: export

run1 : F1 s a -> a

  Runs a linear computation by providing it with its own linear token.
  
  Since this is universally quantified over `s`, it is impossible that
  callers can freely choose the tag for the state thread and thus reuse
  their mutable references.
  
  It is also not possible that the linear token paired with the
  corresponding mutable state leaks into the outer world, because
  the result value must have quantity omega (see the definition of `R1`).

Totality: total
Visibility: export

primRun : F1 World a -> PrimIO a

  Runs a linear computation tagged with `[World]` as a primitive
  `IO` action.

Totality: total
Visibility: export

runIO : HasIO io => F1 World a -> io a

  Convenience wrapper around `primRun`.

Totality: total
Visibility: export

toF1 : PrimIO a -> F1 World a

  Safely uses a primitive `IO` action in `F1 [World]`.

Totality: total
Visibility: export

ioToF1 : IO a -> F1 World a

  Safely uses an `IO` action in `F1 [World]`.

Totality: total
Visibility: export

when1 : Bool -> Lazy (F1' s) -> F1' s

  Run the given stateful computation if the boolean value is `True`.

Totality: total
Visibility: export

whenAlt1 : Alternative f => Bool -> Lazy (F1 s (f a)) -> F1 s (f a)

  Run the given stateful computation if the boolean value is `True`.

Totality: total
Visibility: export

forN : Nat -> F1' s -> F1' s

  Run a stateful computation `n` times

Totality: total
Visibility: export

ffi : PrimIO a -> F1 s a

  Use this to convert a primitive FFI call to a linear function
  of type `F1 rs a`.
  
  This is typically used for running effectful computations that
  do not produce an interesting result.
  See `Data.Linear.Ref1.prim__writeRef` and
  the corresponding `Data.Linear.Ref1.write1` for a usage example.

Totality: total
Visibility: export

interface Lift1 : Type -> (Type -> Type) -> Type

  An interface for wrapping linear computations in a monadic context.
  
  This allows us to deal with pure as well as effectful computations.
  Effectful computations should use `World` as the tag for `s`, while
  pure computations should use universal quantification.

Parameters: s, f
Constraints: Monad f
Methods:

lift1 : F1 s a -> f a

Implementations:

Lift1 s (Pure s)

Lift1 s (Pure s)

Lift1 World IO

lift1 : Lift1 s f => F1 s a -> f a

Totality: total
Visibility: public export

0 IO1 : Type -> Type

Totality: total
Visibility: public export

0 LIO : (Type -> Type) -> Type

  Convenience alias for `Lift1 World`

Totality: total
Visibility: public export

data DebugFlag : Type

Totality: total
Visibility: public export
Constructors:

NoDebugging : DebugFlag

Debugging : DebugFlag

debug1 : String -> F1' s

  This is a utility for debugging complex linear algorithms
  similar to but more convenient than the one find in module
  `Debug.Trace`.
  
  Strictly speaking, using this breaks referential transparency.

Totality: total
Visibility: export

debugIf1 : DebugFlag => Lazy String -> F1' s

  Like `debug1` but can be conveniently turned on and off via an
  auto-implicit flag.

Totality: total
Visibility: export