Funcons-beta : Giving.cbs | PRETTY | PDF

Giving

[
  Entity given-value
  Funcon initialise-giving
  Funcon give
  Funcon given
  Funcon no-given
  Funcon left-to-right-map
  Funcon interleave-map
  Funcon left-to-right-repeat
  Funcon interleave-repeat
  Funcon left-to-right-filter
  Funcon interleave-filter
  Funcon fold-left
  Funcon fold-right
]

Meta-variables
  T, T′ <: values
  T? <: values?

Entity
  given-value(_:values?) |- _ ---> _

The given-value entity allows a computation to refer to a single previously-computed V:values. The given value ( ) represents the absence of a current given value.

Funcon
  initialise-giving(X:( )=>T′) : ( )=>T′
   ~> no-given(X)

initialise-giving(X) ensures that the entities used by the funcons for giving are properly initialised.

Funcon
  give(_:T, _:T=>T′) : =>T′

give(X, Y) executes X, possibly referring to the current given value, to compute a value V. It then executes Y with V as the given value, to compute the result.

Rule
  given-value(V) |- Y ---> Y′
  ------------------------------------------------
  given-value(_?) |- give(V:T, Y) ---> give(V, Y′)
Rule
  give(_:T, W:T′) ~> W

Funcon
  given : T=>T

given refers to the current given value.

Rule
  given-value(V:values) |- given ---> V
Rule
  given-value( ) |- given ---> fail

Funcon
  no-given(_:( )=>T′) : ( )=>T′

no-given(X) computes X without references to the current given value.

Rule
         given-value( ) |- X ---> X′
  ------------------------------------------------
  given-value(_?) |- no-given(X) ---> no-given(X′)
Rule
  no-given(U:T′) ~> U

Mapping

Maps on collection values can be expressed directly, e.g., list(left-to-right-map(F, list-elements(L))).

Funcon
  left-to-right-map(_:T=>T′, _:(T)*) : =>(T′)*

left-to-right-map(F, V*) computes F for each value in V* from left to right, returning the sequence of resulting values.

Rule
  left-to-right-map(F, V:T, V*:(T)*)
    ~> left-to-right(give(V, F), left-to-right-map(F, V*))
Rule
  left-to-right-map(_, ( )) ~> ( )

Funcon
  interleave-map(_:T=>T′, _:(T)*) : =>(T′)*

interleave-map(F, V*) computes F for each value in V* interleaved, returning the sequence of resulting values.

Rule
  interleave-map(F, V:T, V*:(T)*)
    ~> interleave(give(V, F), interleave-map(F, V*))
Rule
  interleave-map(_, ( )) ~> ( )

Funcon
  left-to-right-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*

left-to-right-repeat(F, M, N) computes F for each value from M to N sequentially, returning the sequence of resulting values.

Rule
  is-less-or-equal(M, N) == true
  -------------------------------------------------------------------------
  left-to-right-repeat(F, M:integers, N:integers)
    ~> left-to-right(give(M, F), left-to-right-repeat(F, int-add(M, 1), N))
Rule
  is-less-or-equal(M, N) == false
  ----------------------------------------------
  left-to-right-repeat(_, M:integers, N:integers) ~> ( )

Funcon
  interleave-repeat(_:integers=>T′, _:integers, _:integers) : =>(T′)*

interleave-repeat(F, M, N) computes F for each value from M to N interleaved, returning the sequence of resulting values.

Rule
  is-less-or-equal(M, N) == true
  -------------------------------------------------------------------
  interleave-repeat(F, M:integers, N:integers)
    ~> interleave(give(M, F), interleave-repeat(F, int-add(M, 1), N))
Rule
  is-less-or-equal(M, N) == false
  -------------------------------------------
  interleave-repeat(_, M:integers, N:integers) ~> ( )

Filtering

Filters on collections of values can be expressed directly, e.g., list(left-to-right-filter(P, list-elements(L))) to filter a list L.

Funcon
  left-to-right-filter(_:T=>booleans, _:(T)*) : =>(T)*

left-to-right-filter(P, V*) computes P for each value in V* from left to right, returning the sequence of argument values for which the result is true.

Rule
  left-to-right-filter(P, V:T, V*:(T)*)
   ~> left-to-right(when-true(give(V, P), V), left-to-right-filter(P, V*))
Rule
  left-to-right-filter(_) ~> ( )

Funcon
  interleave-filter(_:T=>booleans, _:(T)*) : =>(T)*

interleave-filter(P, V*) computes P for each value in V* interleaved, returning the sequence of argument values for which the result is true.

Rule
  interleave-filter(P, V:T, V*:(T)*)
   ~> interleave(when-true(give(V, P), V), interleave-filter(P, V*))
Rule
  interleave-filter(_) ~> ( )

Folding

Funcon
  fold-left(_:tuples(T,T′)=>T, _:T, _:(T′)*) : =>T

fold-left(F, A, V*) reduces a sequence V* to a single value by folding it from the left, using A as the initial accumulator value, and iteratively updating the accumulator by giving F the pair of the accumulator value and the first of the remaining arguments.

Rule
  fold-left(_, A:T, ( )) ~> A
Rule
  fold-left(F, A:T, V:T′, V*:(T′)*) ~> fold-left(F, give(tuple(A, V), F), V*)

Funcon
  fold-right(_:tuples(T,T′)=>T′, _:T′, _:(T)*) : =>T′

fold-right(F, A, V*) reduces a sequence V* to a single value by folding it from the right, using A as the initial accumulator value, and iteratively updating the accumulator by giving F the pair of the the last of the remaining arguments and the accumulator value.

Rule
  fold-right(_, A:T′, ( )) ~> A
Rule
  fold-right(F, A:T′, V*:(T)*, V:T) ~> give(tuple(V, fold-right(F, A, V*)), F)

← ↑ →