Idris2Doc : Stellar.API.Morphism

Stellar.API.Morphism

(source)
Reexports
import public Stellar.Ops
import public Data.Sigma
Definitions
record (=&>) : API -> API -> Type
  Totality: total
  Visibility: public export
  Constructor: 
(!!) : ((x : a .message) -> Σ (b .message) (\y => b .response y -> a .response x)) -> a =&> b

  Projection: 
.continuation : a =&> b -> (x : a .message) -> Σ (b .message) (\y => b .response y -> a .response x)

  Hints:
  
APIAlternative (=&>) (*) Maybe
  
APIBifunctor (=&>) (*)
  
APIFunctor (=&>) Maybe
  
APIFunctor (=&>) Maybe
  
APIMonad (=&>) Maybe
  
APIMonad (=&>) Maybe
  
APIPointed (=&>) Maybe
  
APIPointed (=&>) Maybe
  
Cartesian (=&>) (*)
  
Category (=&>)
  
Preorder API (=&>)
  
Reflexive API (=&>)
  
Transitive API (=&>)

  Fixity Declaration: infixr operator, level 1
.continuation : a =&> b -> (x : a .message) -> Σ (b .message) (\y => b .response y -> a .response x)
  Totality: total
  Visibility: public export
continuation : a =&> b -> (x : a .message) -> Σ (b .message) (\y => b .response y -> a .response x)
  Totality: total
  Visibility: public export
.fwd : a =&> b -> a .message -> b .message
  Totality: total
  Visibility: export
identity : a =&> a
  Identity of container morphisms

  Totality: total
  Visibility: public export
(|&>) : a =&> b -> b =&> c -> a =&> c
  Composition of container morphisms

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 1
bimapEx : a =&> b -> (t -> s) -> Ex a t -> Ex b s
  Totality: total
  Visibility: export
parallel : c1 =&> c2 -> c3 =&> c4 -> (c1 // c3) =&> (c2 // c4)
  Tensor is a bifunctor.

  Totality: total
  Visibility: public export
concurrent : c1 =&> c2 -> c3 =&> c4 -> (c1 * c3) =&> (c2 * c4)
  Dirichlet is a bifunctor.

  Totality: total
  Visibility: public export
biSequence : a =&> b -> a' =&> b' -> (a &> a') =&> (b &> b')
  Sequence is a bifunctor
  /!\ This calls the continuation of `m2` twice /!\

  Totality: total
  Visibility: public export
choice : c1 =&> c2 -> c3 =&> c4 -> (c1 + c3) =&> (c2 + c4)
  + is a bifunctor.

  Totality: total
  Visibility: export
swap : (a // b) =&> (b // a)
  Swap tensors

  Totality: total
  Visibility: public export
swap' : (x * y) =&> (y * x)
  Swap dirichelet

  Totality: total
  Visibility: public export
dia : (a + a) =&> a
  Diagonal on coproduct

  Totality: total
  Visibility: public export
dia3 : ((a + a) + a) =&> a
  Diagonal on coproduct

  Totality: total
  Visibility: public export
inl : a =&> (a + b)
  Totality: total
  Visibility: public export
inr : b =&> (a + b)
  Totality: total
  Visibility: public export
elimChoice : a =&> c -> b =&> c -> (a + b) =&> c
  Totality: total
  Visibility: export
pairLUnit : (End // a) =&> a
  End is the neutral for //

  Totality: total
  Visibility: public export
pairRUnit : (a // End) =&> a
  End is the neutral for //

  Totality: total
  Visibility: public export
left : a + Void -> a
  Extract the left value

  Totality: total
  Visibility: public export
right : Void + b -> b
  Extract the right value

  Totality: total
  Visibility: public export
sumLUnit : (Never + a) =&> a
  End is the neutral for //

  Totality: total
  Visibility: public export
sumRUnit : (a + Never) =&> a
  End is the neutral for //

  Totality: total
  Visibility: public export
compLUnit : (End &> c) =&> c
  End is the neutral for &>

  Totality: total
  Visibility: public export
compRUnit : (c &> End) =&> c
  End is the neutral for &>

  Totality: total
  Visibility: public export
comp2Unit : a =&> End -> b =&> End -> (a &> b) =&> End
  Totality: total
  Visibility: public export
State : API -> Type
  State x is the same a 1 =&> x

  Totality: total
  Visibility: public export
state : a .message -> State a
  Build a state from a value.

  Totality: total
  Visibility: public export
Costate : API -> Type
  Costate x is the same a x =&> 1

  Totality: total
  Visibility: public export
costate : ((x : a .message) -> a .response x) -> Costate a
  Build a costate from a continuation.

  Totality: total
  Visibility: public export
extract : Costate a -> (x : a .message) -> a .response x
  Extract the continuation from a costate

  Totality: total
  Visibility: public export
runCostate : Costate a -> (x : a .message) -> a .response x
  Extract the continuation from a costate

  Totality: total
  Visibility: public export
.getVal : State a -> a .message
  Obtain the value from a state.

  Totality: total
  Visibility: public export
0 Context : API -> API -> Type
  A context is both a State and a Costate.

  Totality: total
  Visibility: public export
map_Lift : Functor f => a =&> b -> Lift f a =&> Lift f b
  Totality: total
  Visibility: public export
counit : Monad m => Lift m a =&> a
  Given a monad m we get a counit.

  Totality: total
  Visibility: public export
comult : Monad m => Lift m a =&> Lift m (Lift m a)
  Given a monad m we get a comulitiplication.

  Totality: total
  Visibility: public export
coKleisli : Monad m => Lift m a =&> b -> Lift m b =&> c -> Lift m a =&> c
  Totality: total
  Visibility: export
pure : Comonad m => a =&> (m $- a)
  Given a comonad we get a pure, or unit

  Totality: total
  Visibility: public export
join : Comonad m => (m $- (m $- a)) =&> (m $- a)
  Given a comonad we get a join

  Totality: total
  Visibility: public export
distrib_plus : Lift f (a + b) =&> (Lift f a + Lift f b)
  Coproduct distributes over Lifts.

  Totality: total
  Visibility: public export
distrib_plus_3 : Lift f ((a + b) + c) =&> ((Lift f a + Lift f b) + Lift f c)
  Coproduct distributes over Lifts.

  Totality: total
  Visibility: public export
lift_IO : HasIO io => (io $- a) =&> (IO $- a)
  Totality: total
  Visibility: export
run : (x : State a) -> Costate a -> a .response (x .getVal)
  We need both a state and costate to run a program.

  Totality: total
  Visibility: public export
seq2M : Monad m => Costate (Lift m a) -> Costate (Lift m b) -> Costate (Lift m (a &> b))
  We can sequence two monadic costates

  Totality: total
  Visibility: public export
runSequenceM3 : Monad m => (input : State ((a &> b) &> c)) -> Costate (Lift m a) -> Costate (Lift m b) -> Costate (Lift m c) -> m (((a &> b) &> c) .response (input .getVal))
  Sequence and run three monadic operations.

  Totality: total
  Visibility: public export
forward : (a -> b) -> (a :- c) =&> (b :- c)
  Totality: total
  Visibility: export
backward : (a -> b) -> (c :- b) =&> (c :- a)
  Totality: total
  Visibility: export
trace : Show a => Show (b x) => (a !> b) =&> (a !> b)
  Totality: total
  Visibility: export
traceFwd : Show a => (a !> b) =&> (a !> b)
  Totality: total
  Visibility: export
traceBwd : Show (b x) => (a !> b) =&> (a !> b)
  Totality: total
  Visibility: export