Alexander Kuklev (akuklev) wrote,
Alexander Kuklev


(Ниженаписанное — спекулятивный черновик для внутреннего применения, приведённые утверждения пока даже не проверены, не говоря о формальных доказательствах.)

Purely functional total computations are excellently understood both syntactically and semantically, they are very easy to work with mathematically. The business of describing effectful computations urges to extend this result from total pure functions to procedures written in powerful general purpose imperative programming languages. Procedures are assumed to be typed and composable (thus, form a category, say Proc; actually, a monoidal category we are to interpret procedures with more than one argument) and to faithfully include total pure functions (thus, there should be a monoidal functor proc : Func -> Proc). This structure is enough to interpret plain (i.e. without loops and other control structures) ALGOL-style procedure definitions, i.e. sequences of instructions and let-definitions. Control structures have to be described separately as additional generators of the Proc category.

The other way round, procedures (unless they go beyond Turing-compatibility) can be emulated by pure functions. Just to give you an example, lots of procedures p : X -> Y can be seen as functions f : X × Env -> Either[Y, Failure], i.e. functions taking X and some additional information from the environment, and either produce a result of the type Y or Fail for some reason.

In all cases the authors met so far, categories Proc[E] of procedures where effects are restricted to some homogeneous sort E admit particularly nice emulation by pure functions, namely such that the map emulate : Proc[E] -> Func is a functor and only changes the result (resp. argument) type being right (resp. left) adjoint of the functor proc[E]. In this case the effects are called monadic (resp. comonadic), because respective pair of adjoint functors gives rise to a monad (resp. comonad). Some sorts of effect allow emulations of both types, these effects are called bimonadic and are particularly well-behaved.

Plain lambda term (i.e. one containing no lambda terms inside) is a type-aligned directed acyclic graph with nodes labeled by functions, the dataflow graph.
Monadic effects are the ones admitting separation of data flow and execution flow, definitions of procedures with monadic effects look very much like plain lambda terms, with additional strict linear execution order loosely aligned to the dataflow graph. That's precisely the point of ALGOL-style definitions arise, they strive to set both dataflow and execution flow without much boilerplate. There are lots of information about monadic effects. In particular, all monadic effects present in general purpose programming languages are particularly nice ones: they arise as free monads for left Kan extensions of type-indexed inductive type families and compose very well. These are precisely the effects which can be understood in terms of delimited continuations (exceptions, loops, cooperative multithreading, state, non-determinism).

Explanations about comonadic effects are rarely to find. Consider a function f : X -> Y. Such functions are given by lambda expressions (x : X => expression-of-the-type-Y). Prototypical example of a comonad is adding an additional argument F(X) = X × C, functions of the type F(X) -> Y are given by lambda (x : X, c : C => expression-of-the-type-Y). In what follows we'll use postfix notation X ⋊F for F(X) whenever the dependent type F(_) is equipped by a free comonad structure. This notation should suggest that every free comonad may be viewed like this albeit with substantial restrictions on how the additional argument c may be treated: In general, substitution and contraction (using the argument variable more than once or any other means of “cloning” it) are not admissible. Ignoring the additional variable is allowed:
There is morphism discardF[X] : X ⋊F -> X which allows to lift any term f : X -> Y to term f ∘ discardF : X ⋊F -> Y.

Free comonadic effects look like an additional affine argument (can be discarded). For procedures with comonadic effects we'll use the lambda-term-like notation where these affine arguments start by #. In addition to data flow, these terms track linear order of operations on affine arguments. Affine arguments might change their type upon actions of such operations. Dually to free-er monads, we can consider cofree comonads on Kan-extensions of type-parametrized codata-types, these should compose well. Let me give you some examples:

@Service Logger:
  Logger.log(m : Message) : Unit

@Service Oracle[T : *]
  Oracle[:T].compare(a b : T) : (a = b) or not (a = b)

@Service Tty:
  Tty.say(m : Message) : Unit
  Tty.ask(r : Request) : r.Response

@def hello-world(name : String, #console : Tty):
    Hello, [name]!

@Service Tty[number-of-questions-permitted : Nat]:
  Tty.say(m : Message) : Unit
  Tty[succ(:n)].ask(r : Request) : r.Response @Goto(Tty[n])

@Serice GetOnce[T : *]:
  GetOnce[:T].get : T @Goto(Unit)

(Non-deterministic output: Tty[:n].ask-for-additional-question: (b : Boolean) @Goto(Tty[if b then n + 1 else n]))

The most intriguing question I do not yet have a satisfactory answer to, is the question about general form of handlers for comonadic effects. Interestingly, most general handlers for monadic effects are procedures getting an affine argument called "continuation", i.e. they are themselves comonadically effectful. This suggests that comonadic handlers should be monadically effectful and the dual of continuation is, intuitively, backtrack. Might they be allowed cast a retry(newArg) request? For lots of bimonadic effects (like state or exceptions) it can be a very natural idea to use both monadic or comonadic handlers depending on the problem. We might want to catch exceptions, we might want to rerun the piece of code which led to an exception. The only thing is that we must be sure that the piece of code we're reruning is free of monadic effects (we do not know how to "undo" monadic actions) or respectively that all thunks we pass as continuations are free of comonadic effects, since invoking a retry inside of the continuation would also involve undoing a monadic action, which is in general impossible.

  • Towards Univalent Construction Calculus

    Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning. By “modern”…

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.