Optionally declare functions pure?

[shelby3]

@shelby3 wrote:

Also, the compiler can use a much simpler form of path analysis (independent of run-time state) to do that performance optimization without needing dependent typing (although without purity it becomes more difficult for the compiler to know what is safe to reorder).

Purity provides more opportunities for optimization.

[keean]

I would rather have monadic types for impurity. In this way we have a sound type system that can be expanded for full effects support. I would like to have inferred monadic side-effects. The inference means the average user does not need to bother or understand them, but you can use type classes to constrain the types to achieve things like this function must not do IO, or must not allocate memory etc.

If all the primitive operations have the correct mondaic types assigned to them, purity becomes constraining a type to have no side effects. I haven't really thought about the effect syntax, nor how a constraint on effects would look syntactically, but this achieves what you want with more fine-grained control about which side-effects to permit.

[SimonMeskens]

If operations are correctly typed and maybe with some syntactic spitshine, we can make monadic types look very simple, I'm all for just going with monadic types. We can probably make it so the user doesn't even realize he's using monadic types.

[keean]

Lets assume we have monadic types, and that all functions are in some monad (as we want to allow imperative style statements anywhere). Further lets assume we have a monadic effect system, with effect inference. As such effects will propagate from the function use site to the definition (the effects on a function being the union of all effects in functions used in the function definition).

As long as primitive functions get the correct types, it should all work without the user even knowing. They only need to know if they wish to constrain effects, probably with some kind of type class. In order to do this the type system will need to provide some a 'set' kind of type, but I think we need that for union types already.

Having to import functions from JavaScript and give them a type seems like some boilerplate, but I don't think there is any other way. For example a simple primitive 'print' type function would have a signature like:

print(x : String) : [write_stdout] ()

A primitive input function would type like this:

input() : [read_stdin] String

Now you can use them like this:

doit = (prompt) =>
    print(prompt)
    return input()

The type of doit can be inferred, however you can give optional type annotation like this:
doit = (prompt : String) =>
doit = (prompt) : String =>
doit = (prompt : String) : String =>
doit = (prompt : String) : [write_stdout, read_stdin] String =>
All the above would be valid, but the type below would not:
doit = (prompt : String) : [] String =>
The empty brackets would force the function to be pure, and of course the definition is not, so it should fail type-checking.

So the assumption is all functions are in the effect monad, and therefore we can omit the effect constructor '[]' from the type signatures of functions.

[SimonMeskens]

I like that. A lot.

[shelby3]

My understanding of a monad in this context it provides composition of functions that mutate some state (i.e. input and output the state type) with those that don't. The advantage over compiler-assisted access to globals, is we can have different state objects (e.g. different implementation of print) for different code paths. And I believe we can even compose monads in some cases, but they are less composable than Applicatives. I like the idea of fine-grained access to resources, as this also has security applications, e.g. Android apps need to declare which resources they access.

But separately we would still need a way to declare a function's inputs arguments and constructed references (collectively or individually) deeply immutable (which is not the same as JavaScript's const which merely prevents reassignment of the reference).

[keean]

Technically in an imperative language where any statement can perform IO to any external service, every function is in a monad :-) The threaded state is the 'world' and return is the unit function, and the statement separator (newline or ;) is bind.

[shelby3]

We need purity declarations, otherwise we model values separately from functions, which is a non-unified construction.

Note that the purity declaration for an immutable reference and a zero argument function can be unified to let.

[keean]

Then we get an arbitrary split, some functions are pure and some functions are impure. I can only call pure functions from pure functions but I can call either from impure functions. This is how Haskell works and it as a real problem for a lot of people to work with. You want to put a print statement in a pure function somewhere and all of a sudden you have to rewrite half the program.

If you want an easy to use language that Java programmers will be able to use, we cannot do this. This would make the language feel more like Haskell than any of the type system features I want.

I think we want all functions to be impure and in the IO monad. We can then use constraints to prevent side effects where we don't want them, but the functions will still be impure.

The separation between function reference and result value is very important.

[shelby3]

@keean wrote:

You want to put a print statement in a pure function somewhere and all of a sudden you have to rewrite half the program.

I thought you were planning to offer treading global state through pure functions with an implicit/inferred monadic system. So IO would be in the monad. Same as Haskell does it.

Seems to me we can't do your monadic idea unless we do it every where. But am I correct it will only add overhead to calls to functions which access the monadic state or will the performance of every function call suffer?

I think we want all functions to be impure and in the IO monad. We can then use constraints to prevent side effects where we don't want them, but the functions will still be impure.

If we are forced to have your monadic system every where, then why should all functions be impure and in the IO monad by default?

The separation between function reference and result value is very important.

I don't understand what you do you mean?

[shelby3]

If we will have pure annotations on functions, then we also need const annotations on input arguments for impure functions that only call pure functions on those const inputs.

[shelby3]

@keean seems to me silly that for example a length function will ever need to call print. That is what we have debuggers for.

[keean]

Seems to me we can't do your monadic idea unless we do it every where. But am I correct it will only add overhead to calls to functions which access the monadic state or will the performance of every function call suffer?

There is zero implementation overhead, it is simply a type system change. I have pointed out before you can give 'C' functions a monadic type, do the type checking and then compile it using the normal C compilation method.

[keean]

If we are forced to have your monadic system every where, then why should all functions be impure and in the IO monad by default?

Because we may want to change the function to include IO without having to change all the module type signatures.

I don't understand what you do you mean?

A program is a bunch of symbols that is executed to produce a result. It is important we can pass around the unexecuted function and then execute when we want. I think it is important that the notation is consistent no matter how many arguments a function has. Making an exception for zero argument functions is introducing special case inconsistent notation.

seems to me silly that for example a length function will ever need to call print. That is what we have debuggers for.

Debuggers should not make up for inadequacies of the language. Programs are rarely written in their final form and the ability to easily refactor is important.

[shelby3]

@keean wrote:

Because we may want to change the function to include IO without having to change all the module type signatures.

I don't understand. What do modules have to do with it? I probably need to see a code example.

A program is a bunch of symbols that is executed to produce a result. It is important we can pass around the unexecuted function and then execute when we want. I think it is important that the notation is consistent no matter how many arguments a function has. Making an exception for zero argument functions is introducing special case inconsistent notation.

Afaics, syntax of zero argument functions is orthogonal to a purity annotation decision and discussion. @skaller and I enumerated optimizations and benefits of purity. For example also the following also applies to non-zero argument pure functions:

@shelby3 wrote:

The following LOC would be a compiler error, because the result value of pure functions must be assigned:

size

---

Debuggers should not make up for inadequacies of the language.

What inadequacy? Purity annotation is an optional feature.

[shelby3]

Readers please note that certain side-effects are not side-effects in our type system. More discussion about the relationship to IO monad.

You had disagreed with me about certain side-effects being inapplicable, but I (and @skaller) argued I think convincingly that the only side-effects that matter are those that our type system guarantees.

If we pass around the IO monad as external state, then every print(x) will be an "impure" function w.r.t. to every function that also accesses the IO monad but if a new copy of the IO monad is returned instead of being mutated, then those functions are still pure functions because they don't modify external state nor depend on any state not provided by the inputs. This why Haskell is still pure even though it has side-effects to IO monad, because this IO monad state is a state which is passed along the function hierachy and so the ordering is explicit. That effects are semantically imperative (meaning that changing something in one function could affect expected semantics in some function far away, i.e. the locality of semantics is desirably forsaken), but the functions are operationally (operational semantics) pure and can be optimized as pure.

I wrote:

We can’t model everything with types, thus a typing system is always inconsistent (or otherwise stated can’t model all forms of errors nor allow all algorithms).

Thus even in a statically typed program, we must have dynamically typed features either explicitly or adhoc. So to characterize a program as unityped doesn’t mean it has less expressive power, only that it has less statically expressive power.

[shelby3]

@keean wrote:

I don't think we need purity anyway, just side-effect control.

What do we gain by marking a function pure?

@skaller and I already explained that. I also explained that even a non-zero argument pure function can't be invoked without assigned the result value, so the compiler can catch this bug:

The following LOC would be a compiler error, because the result value of pure functions must be assigned:

size

[keean]

@shelby3 okay well I think a zero argument function should be executed... it is not the same things as a value. Scala got this wrong :-)

[shelby3]

@keean there is no reason to execute a pure zero argument function. That is nonsense.

And there is no reason to execute any arity pure function if the result value is not assigned.

[keean]

@shelby3 It may fail due to lack of memory. A value is a value like '4' or '7'. A function has a value which is the set of symbols for example "4 + 7". Before you execute it is is "4 + 7" when you execute it, it returns "11". If it is a const function the compiler may optimise by executing it at compile-time. (By the way @skaller was saying the same thing).

To me it seems you want to save typing two characters () and that you are willing to mess the semantics up to do it.

[keean]

refresh again.

[keean]

We can analyse this further. The only time a pure function is really pure is when all the inputs are known at compile time (in which case you can treat it as a const). If any of the inputs to the function depend on IO then the pure function has to be lifted into the IO monad.

To put it another way, when we treat a function as pure and replace it with its value it means the input cannot change. If the inputs to a function change, its results will change to. You can see this in Haskell:

f x y = x + y    {- pure function -}

g : IO Int   {- impure function does IO -}
g = do
    x <- readInt
    y <- readInt
    z <- return (f x y)     {- lift f into the IO monad -}
    return z

If we don't do this the program will go wrong, because the compiler will not know that the result of 'f' can change with time, and it will replace it with a single value that won't change even if we run g again and the user inputs different values, once f is replaced by a value it will always be the same value.

[keean]

Of course if a function has no side effects, and no arguments, it must be a const value (IE the compiler can replace the function with its value at compile time). If this is the case you can declare it as a value instead, just do:

let x = 3 * 5 + 8

It seems there is no need to ever have a pure function with no arguments. The only useful zero argument functions have side-effects :-)

[shelby3]

@keean don't forget that (which I pointed out before) a function which takes a callback of a zero argument function, would also accept a pure such function. And this is another reason to treat const values and pure zero argument functions as equivalent and also pass them as callback for (pure and impure) zero argument functions.

[shelby3]

@keean wrote:

It may fail due to lack of memory.

...

The only time a pure function is really pure is when all the inputs are known at compile time

I already linked to were @skaller and I refuted that entire line of reasoning. I am not going to repeat it.

To put it another way, when we treat a function as pure and replace it with its value it means the input cannot change. If the inputs to a function change, its results will change to. You can see this in Haskell

You are conflating two orthogonal concepts. The value of the pure function never changes and no side-effects occur (that are modeled in the type system). The inputs select which element of the (lazily memoized) set of the function's value is presented.

An impure function isn't guaranteed to have the same result for any fixed input, i.e. the set of results that is the function's value is not constant.

To me it seems you want to save typing two characters () and that you are willing to mess the semantics up to do it.

No I want a system that is complete, consistent, and not corner cases. It appears to me sometimes you seem to want consistency by not being complete, which is a form of obscured inconsistency.

[skaller]

To make progress I suggest implementing basic stuff, when in doubt leave it out until there are actual uses cases to consider. So, do not put "pure" yet. Do not have => for functions and -> for functions with IO monad, yet.

These forums are not the best for technical discussions IMHO. For a start, you can't reply to someone as you can with email. We need an email list which tracks commits. I can write some test cases, but i would need commit access and a fairly clear specification of what is implemented and what it should do. As soon as possible, I think an FFI is required, and then a place to put a library of bindings to Javascript. Most of the work you can do with the language can then be done almost immediately by adding the required bindings and writing Javascript to bind to.

No matter what you think the advantages of Zen-fu are the primary one is the ability to leverage existing code, but access it in a better structured way (eg with type checking).

One thing I learned on the C++ committee is that the library drives the language. You add stuff you need to make the library work. So for example Felix has a restricted kind of constrained polymorphism where you can define a type set (a finite list of types), and constrain a type variable to that list. Why? Because that's whats needed to define addition of all 20 types of integers C++/Posix require in one line. (Just an example).

[shelby3]

@keean you didn't really address my question directly. I am agreeing with you that the IO monad is not composing functions that are impure w.r.t. to the world because the access to the world is sequenced by bind, but those functions must also otherwise be pure, i.e. they can't be allowed to save a mutable reference to the world because then they could violate the control of ordering dictated by bind. The access of mutating the world is really not pure, but it becomes pure because the mutations are ordered by the bind.

Thus I am saying you were wrong to imply that Haskell allows impure functions or that IO monad will work correctly with impure functions. The functions are actually impure w.r.t. to their mutation of the world, but because they are not otherwise impure (i.e. they can't save a mutable reference to the world) and because their access to the world is ordered via bind, then in effect they are pure w.r.t. to the world.

[keean]

Given a completely pure program like (a + b + c + d) the compiler is completely free to execute (a + b) and (c + d) in parallel, but must wait for both of these to finish before it can do the final add. However it needs to choose the correct order of additions to get the optimal parallel execution time.

However the context switch time (for example the standard unix context switch is 100 times a second) means that very small tasks are inefficient, so this kind of parallelism is actually slower, due to the overhead of context switching and the quantisation of CPU time.

On a Unix system for example optimal parallelism is when tasks take of the order of 10 milliseconds or longer.

[shelby3]

I don't see how your comment regarding the cost of context switches is at all relevant to my point.

The fact that a particular case of higher-level parallelism is not worth executing in parallel is irrelevant and has nothing to do with my point.

The point is that higher-level parallelism has access to invariants that low-level CPU level parallelism doesn't have.

(And yes the compiler along with any profiling runtime optimiser a la Hotspot could determine which instances of higher-level parallelism are not cost-effective to execute in parallel but that is besides my point)

[keean]

Thus I am saying you were wrong to imply that Haskell allows impure functions or that IO monad will work correct with impure functions.

The trick is in the monad itself, and is more to do with object naming than anything else, consider:

(world2 , i) = input(world1)
(world3, j) = input(world2)
(world4, k) = input(world3)

In the above the world is immutable, but we can "input" from it returning a new "world" hence we model IO sequencing in a pure functional program. However we have to keep track of the different versions of the world, and we can re-use earlier worlds (which would give us back-tracking in a parser). This is threading the state through a pure computation.

If we look at an OO program with state we might right:

i = world.input()
j = world.input()
k = world.input()

So the difference between the above functional version, and the OO version is that in the OO version the 'world' refers to the all versions together. Hence mutation can be seen as giving the same name to the object before and after it changes, whereas a pure function must give a new name to the new version of the object.

A monad lets you make the former (pure program) look like the latter (impure program) by hiding the state threading, but unlike in the OO sense the threading is still happening, so all the code is actually pure, although it behaves like impure code so:

do
i <- input
j <- input
k <- input

The monad is handling the threading of the world implicitly, and this is why you can have things like "MonadPlus" which is the equivalent of saving a reference to the world and reusing, hence giving backtracking.

So if the real trick to the monad is that it allows pure functional code to behave like impure imperative code, the final amazing thing is that you can view a monad as a pure type-system transformation, so if we take the 'C' program:

char* x = getLine();
printf("you typed %s", x);

We can type 'getLine' as a monadic function "IO String" without changing the 'C' code. We can type check the 'C' code as if it were a pure functional program.

[shelby3]

In the above the world is immutable

In other words, as I wrote, the functions input are otherwise pure.

Note the world is not actually immutable because you can't copy the world, so you can only mutate it. But we can pretend that our function input is treating world as immutable in every way (i.e. it can't store a mutable copy) except that it is allowed to call functions that mutate the world and then bind insures that those mutations are ordered (so that the functions input behave relatively speaking as if they are pure w.r.t. to the world).

Which is equivalent to what I already wrote.

Our brains work differently. I like to distill to the generative conceptual (abstract) essence.

You seem to prefer to think in terms of structures (i.e. algebras). Your essence is mathematical. My essence is conceptual. This why you tend to explain with notation and find it difficult explain well in words.

[shelby3]

Okay now that we've clarified monads, I feel more confident to conclude that your proposal for having tuples of effects will not compose with monads. The entire reason that monads don't compose well, is because they must maintain the ordering on the particular lifted type. If you mix and match lifted types, this ordering can't be maintained in the permutations of composition and mis-matches.

Monads enforce a total ordering on access. This is why they don't generally compose.

[keean]

Actually composition of monads is quite easy providing you have the right mechanisms. If you start with a type-indexed-set, then each monads state can be indexed by a type. We are effectively unioning monads together, where each monad can select its state from the type-set by a unique type.

If you do what Haskell does with monad transformers you end up in the "lifting-mess" that you describe, but with effect sets there is no lifting, beyond the simple one-level lifting of in the monad or not.

This is the doing the equivalent for monads, that union types do for simple types.

[shelby3]

I don't understand. I have stated that lifting unions of types is incompatible with bind under composition of different unions. Bind can only work with the same lifted type. Thus your unions will have to match. Thus composition becomes impossible when they don't match.

It seems you want unions of types as indication of which effects are allowed. Okay fine. But it doesn't compose well with bind. In other words, the logic on supersets doesn't compose with bind, i.e. you can have a match that is permissioned but won't compose.

[keean]

You lift both sides of the bind, so the monad constructor is the union of all monad constructors used in the function. Note the union occurs in the constructor, not the parameter, so the union of a monad m a and a monad n a is (m /\ n) a. So the type of bind remains w a -> (a -> w b) -> w b where w is the union of all monad constructors used in the chain of binds.

[shelby3]

I wrote:

EDIT#3: Haskell (and Purescript) forces pure functions every where. (There's also the lazy evaluation every where in Haskell but not Purescript). All imperative code has to be shoehorned into the IO monad or other monad such as the State monad. Monads don't generally compose (although Applicatives do). Monads are more powerful because the bind commits to the type of container versus apply for Applicatives. When people in the Haskell world speak of "effects" they're referring to capturing the inpurity of imperative code in the state of the Monad. Monads may help us reason about impure effects within the mathematical conceptualization of category theory. Which in turns aids some functional/modular reuse and composition (e.g. Applicatives can lift any function on value types to a function on collections of that value type). However, some algorithms which are straightforward with imperative code, may require significant modeling with Monad transformers to achieve in the monadic model. As I understand it, this attempt to categorize (as in category theory) all variants of imperative structure, is a pita. I'm not sure if it is worth it. Many programmers are comfortable with the flexibility of unstructured imperative coding. For the mathematically minded, who want to model every aspect of their program with category theory, it may afford some significant productivity benefits. But I'm not convinced yet that is the correct direction for a mainstream programming language. Note this summary may be incorrect, as I'm not a Haskell expert. I have minimal understanding of Haskell, category theory, and monads. We had discussed monads in a separate thread.

[shelby3]

My rambling musings[mudslinging] from private discussion with @keean:

In the abstract, note how goroutines lift the effects of concurrency out of the control structure of functions and into another space where the effects appear only in terms of for example data races. Immutability and referential transparency are analogous in the sense that they lift the effects of state out of the internals of the objects/functions and into compositional ordering of objects/functions.

Immutability of objects (i.e. that any mutations must not impact other references to the same object) enables my complete solution to the Expression Problem for heterogeneous containers employing unions for the value type, although it has a log n slowdown. Immutability doesn’t necessary require copying. An alternative is to keep track of mutations separately for each reference to the object.

Clojure employs efficient immutable data structures such as tries.

Lazy evaluation helps with the efficient computation of pure functional compositions, which enables equational reasoning mentioned below, but has tradeoffs w.r.t. strict evaluation.

So that computations which are discarded by the composition are never computed.

Lifting effects out of functions make it possible to reason about effects in a category theory model where functions are morphisms, i.e. functions in a mathematical sense, not procedures.

Internally a function need not be pure w.r.t. it’s internal state and externally it can be pure w.r.t. to external state.

So when we can isolate objects to exclusive references, then we can do impure algorithms and still be pure on the composition with external state. So this leads us to a generalized unified model.

I think Oleg’s recent research is probably a formal way of stating what I just stated?

So when we restrict concurrency to single-threaded w.r.t. to shared state, then enables us to reason about the data races on the shared state (the external state effects) w.r.t. functions which are concurrent and those which are not. Concurrent functions can yield, which can preempt the single-threaded algorithm.

Whereas, with multi-threaded preemption, every instruction can be preempted, so there is no way to reason about data races except by a total order of exclusivity of mutability. Which is what Rust does.

See also the Mutable Objects #32

[shelby3]

Algebraic Effects

I’m making a reasonably detailed exposition targeted towards even those who aren’t well versed in Haskell or category theory, both because my desire is to produce a mainstream programming language (so I might as well start now trying to layout these concepts in a manner that non-researchers can grok) and for myself to refer back to if in the future I’ve forgotten some details.

Picking up again my naive investigation and steep autodidact learning curve from 2011 (c.f. also here and here), recently I’ve been (along with some assistance from @keean in private messages) analyzing algebraic effects as possibly a better model for controlling imperatively ordered⁵ effects. Such effects include I/O, exception handling, callbacks, and access to state without referential transparency. Applicative algebraic effects commute; and thus modularly compose unlike for monads^[*] which require transformers that discourage modular composition.

I was exposed to algebraic effects in my search/research for how to achieve goroutines in Multicore OCaml, and then @keean mentioned to me Levy’s CBPV (call-by-push-value as unification of call-by-name/CBN and call-by-value/CBV). What motivated me is realizing that the value restriction can only be avoided with applicative (aka pure) programming (i.e. the restriction exists to prevent purity aka referentially transparent assumptions about parametricity that don’t hold in an impure context, _{^{c.f. also §Separation of values & computations on pg. 3 of An Introduction to Algebraic Effects and Handlers1}}), and that the value restriction is indicative of lack of equational reasoning (i.e. as evident by the restriction preventing application of functions to functions as a parametrised value, which is Scala’s syntactical restriction). And also the realization that modularity requires applicative ML-like functors.

IOW, continuing to program in a C-like or JavaScript-like imperative style isn’t going to produce modular, referentially transparent effects which can increase flexibility of code reuse and decrease bugs.

So perhaps we need a new paradigm. And hopefully one not as abstruse as Haskell and without the often unnecessary lazy evaluation (aka call-by-need) which complicates reasoning about implicit space and time effects.

Backtracking example employing algebraic effects

The example for backtracking with algebraic effects in §2.3.2 Backtracking on pg. 8 of An Introduction to Algebraic Effects and Handlers^1 2:

rec fn chooseInt(m,n) →
  fail() if m>n else
    do b ← decide() in
      (return m) if b else chooseInt(m + 1,n)

def pythagorean = fn (m,n) →
  do a ← chooseInt(m,n−1) in
    do b ← chooseInt(a+1,n) in
      (return (a,b,√a²+b²)) if isSquare(a²+b²) else fail()

def backtrace = handler {decide(_;k) →
                           with
                             handler {fail(_;_) → k false}
                           handle
                              k true}

A key point in understanding the above backtracking example is an inversion-of-control such that the return in chooseInt is “calling” (i.e. applying) the instances where it’s invoked with do. Actually to be more precise, the handler for decide is applying the continuation k with k true to evaluate the in block of do b ← decide() in with a true or false value for b. Before sequencing the continuation of the decide handler, the return (i.e. (return m) if b) in the said in block sequences the in block of the do which consume chooseInt— a coinductive inversion. Because per the ordering of monadic bind operation, the return value of chooseInt is the continuation monad returned by decide not return m (the latter being the return value of the function input to the bind operation). And as graphically elucidated in Semantics of §1 Language on pg. 3, each handler operation such as decide creates a DAG tree of possible evaluations which is the coinduction of the apparency of inductive procedural nesting. The decide handler only has two branches true and false. The false branch only is evaluated if the decide handler encompasses an evaluated fail “exception” operation.

This coinduction is more explicit in the §2.3.1 Maximal result on pg. 7, because the handler for decide in this case explicitly sequences the k true and k false continuation applications with do to capture the results of each leaf of the DAG to compute a hierarchical maximum value.

def pickMax = handler {decide(_;k) →
                         do xt ← k true in
                           do xf ← k false in
                             return max(xt, xf)}

Note pickMax can’t used with pythagorean because the former expects an integer type and the latter a tuple (integer, integer, integer) (for (a,b,√a²+b²)).

For the backtracking example, the depth-first algorithm is by applying k true first in the handler for decide because it applies the if isSquare(a²+b²) first and else chooseInt(m + 1,n) is only applied later if there's a fail exception. Transposing the false and true in the handler for decide creates a breadth-first algorithm because else chooseInt(m + 1,n) is applied first and if isSquare(a²+b²) is only applied later if there's a fail exception.

Complete understanding of operational and denotational semantics requires learning that the do notation binds (i.e. implicitly wraps the subsequent block(s) in the (nested) functions of a monadic bind^[*](c.f. also^[*]) as evident by the return which is the unary operator of a monad, thus enforcing referential transparency via recursion of the binary bind operation of a monad, thus syntactically disallowing cyclic loops and referencing (thus enforcing the aforementioned acyclic DAG).

The subsequent Fined-grain monadic continuations section is a primer on the relevant domain knowledge that applies to understanding the prior paragraph.

Translated to pure functional and imperative

Below are the example code translations for the equivalent operation semantics interpretation employing pure functional programming and imperative equivalents. The None correspond conceptually to the fail() in the algebraic effects example. It’s amazing that with algebraic effects by merely changing the handler for decide, we exchange between depth-first or breadth-first algorithms, which I will explain more below.

// functional recursive
fn f(m,n) = fa(m,n-1)

// `decide()` tries `true` first, i.e. depth-first
fn fa(a,n) = fab(a,a+1,n+1)
             | Some(r) -> r
             | None    -> fa(a+1,n+1) if a < n
fn fab(a,b,n) = Some(a,b,√a²+b²) if isSquare(a²+b²) else fab(a,b+1,n) if b < n else None

// `decide()` tries `false` first, i.e. breadth-first
fn fa(a,n) = fa(a+1,n) if a < n else None
             | Some(r) -> r
             | None    -> fab(a,a+1,n+1)
fn fab(a,b,n) = fab(a,b+1,n) if b < n else None
                | Some(r) -> r
                | None    -> Some(a,b,√a²+b²) if isSquare(a²+b²) else None

// imperative loops
fn f(m,n)
// depth-first
var r = None
for(a = m; a <= n - 1 && r == None; a++) {
  for(b = a + 1; b <= n && r == None; b++) Some(a,b,√a²+b²) if isSquare(a²+b²) else None
}

// breadth-first
var r = None
for(a = n - 1; a >= m && r == None; a--) {
  for(b = n; b >= a + 1 && r == None; b--) Some(a,b,√a²+b²) if isSquare(a²+b²) else None
}

Modular generic flexibility

As exemplified for the return x → return (x, “”) and return (x, join s acc) in the handler for collect in §2.1.3 Collecting output on pg. 5, the return type of the handled operations (e.g. abc) which invoke the contained handler (e.g. print) can be modified by the handler, i.e. inversion-of-dependencies. This is what is meant by “the return clause would return a singleton list containing the returned value […]” in §2.3.1 Maximal result on pg. 7 for implementing pickAll; which in turn is referred to by §2.3.2 Backtracking on pg. 8 for implementing a pickAll for the backtracking example.

Fined-grain monadic continuations

Per §1 Language on pg. 2 of An Introduction to Algebraic Effects and Handlers, P. Levy’s fine-grain call-by-value is the programming language concept employed in the algebraic effects examples of this post.

1. First, a non-category theory overview and interpretation of the most salient points from 20 years of the research:

   1. In 1989, Filinski explained³ that call-by-name (CBN) has category theory products _{^{(aka conjunction productions)}} but no category theory sums _{^{(aka disjunctive coproductions)}}; and vice versa for call-by-value (CBV).

   2. Meaning all computations ^{_{(aka productions/operations/functions)}} in CBN for example ((x, y) => y if x !== null else x)(obj, obj.property)^2 4 are not—and values in CBV are not—populated by ^{_{(an artifact of evaluation known as)}} the non-termination/divergence (aka bottom) type ⊥. And vice versa CBV has computations (e.g. those functions whose return type includes ⊥ because they can throw an exception) which are—and CBN has values⁵ which are—populated by ⊥ divergence. Essentially the dichotomous dilemma duality is because of bifurcation of typing if comparing CBN to CBV. CBV has inductive value types for everything including first-class functions (because the meaning of first-class if they can be stored in values), yet CBN has coinductive computation types for everything including values⁵.

   3. Which btw, is the reason why (so as to avoid segfaults that) CBV requires one of the following: a bifurcation of types, value restriction, or disallowing parametric polymorphism for values. §2. Some examples on pg. 2 of Levy’s Modelling environments in call-by-value programming languages implies the same requirement because it exemplifies that CBV doesn’t have consistent cojunctive products, e.g. the inconsistent evaluation order (relative to each other) of each a tuple of function parameters.

   4. Levy’s call-by-push-value (CBPV) models and subsumes both CBN and CBV by employing separate (i.e. a bifurcation of) types for values and computations; and employing explicit thunks aka continuations (which are values) to model the delayed application of the computation’s ^{_{(aka production/operation/function’s)}} parameters inherent in CBN.

   5. In §1. Introduction of Modelling environments in call-by-value programming languages, Levy’s aforementioned insight (in #1-iv above) to bifurcate the types of values and computations was applied to devise a variant of Moggi’s model where everything has a function type and coarse-grained strong Monads simulate imperatively ordered values⁵ in a type safe manner (i.e. which provided the aforementioned required bifurcation only implicitly and monolithically as metalanguage for value types). As explained in §3.1. λ_c Calculus and monadic metalanguage on pp. 5 – 6, Moggi augmented the simply typed λ_c-calculus with strong monads (as a metalanguage) to most elegantly meet the aforementioned requirement in #1-iii above.

      Levy’s §3.2. Fine-grain call-by-value (as reiterated in §8. Conclusions on pg. 19) attains the bifurcation between values and computations (aka ‘producers’ of values) ^{_{(aka productions/operations/functions)}} with explicit distinct operational semantics models for each, thus enabling explicit control of the evaluation order of continuations (examples follow below) enabling a more fine-grained flexibility without the aforementioned (c.f. the 2nd paragraph of this post) downside of (Moggi’s strong) monads.

      Thus as compared to Moggi, while sequencing of operations remains via the bind operation of a monad, yet the monad is the continuation (e.g. k here) which producers (aka operations here) may explicitly apply (examples follow below).

Thus, the do and return in the algebraic effects examples of An Introduction to Algebraic Effects and Handlers, are respectively the syntax sugar for the binary bind operation combined with §Generic effects on pg. 2 and the unary return operation both for a continuation monad.

The return constructs a continuation monad with the input parameter y (in return y) to be later provided as the input to the callback morphism function (a → M b) provided (to bind) upon application of the bind operation— which corresponds as explained in §Generic effects to the do y ← syntax sugar.

The bind operation can be seen in the example from §2.1.2 Reversed output on pg. 5:

def abc = print “A”; print “B”; print “C”

Per Sequencing in §1 Language on pg. 2, the semicolon is a syntax sugar for the do notation.

def abc = _ ← do print “A” in
            _ ← do print “B” in
              _ ← do print “C”

Above per Language extensions in §1 Language on pg. 3 the _ ignores the parameter which we do in this case because print outputs unit aka () (and unit always has same value, so it’s pointless to give it another name as a parameter, because we can use its consistent name ()).

The do notation is a syntax sugar for the bind operation.

def abc = (print “A”) bind (() → 
            (print “B”) bind (() →
              print “C”))

Written in a more JavaScript-like syntax pseudocode:

function abc = bind(print("A"), () =>
                 bind(print("B"), () =>
                        print("C")))

The laws which every monad must obey insure that regardless whether our programming language is CBV or CBN, the print() operations will be evaluated before the morphism which is the other (i.e. the 2nd or rightmost) parameter to bind— which was the point of Moggi’s augmention aforementioned in #1-v above.

P.S. For more information about shallow handlers from §2.1.1 Constant input on pg. 5 (and more in depth information on other facets), c.f. §2.6 Handling by Application on pg. 4 of Do Be Do Be Do.

¹ _{Paper was also mentioned in §3.6 A tutorial on algebraic effects and handlers on pg. 6 of From Theory to Practice of Algebraic Effects and Handlers by Andrej Bauer et al.}

² _{Incorporating my proposed b if a else c syntax for ternary instead of if a then b else c or a ? b : c.}

³ _{Filinski, Declarative Continuations and Categorical Duality, §1.3.1 Basic definitions, §2.2.1 Products and coproducts, §2.2.2 Terminal and initial objects, §2.5.2 CBV with lazy products, §2.5.3 CBN with eager coproducts, §2.5.4 A comparison of CBV and CBN, and §3.6.1 CBV and CBN in the SCL.}

⁴ _{The example is an anonymous function function f(x, y) => y if x !== null else x application (called) with the parameters f(obj, obj.property). CBN doesn’t evaluate the function parameters before invoking the anonymous function, thus obj.property isn’t evaluated if obj === null. Whereas, CBV would evaluate the both function parameters before applying the anonymous function; thus causing a segfault when obj.property would be evaluated even when obj === null.}

⁵ _{To understand how CBN can have computation in value types, note that an object and its properties can be modeled with continuations. And imperativity as an orthogonal concept to referential transparency (aka pure functional) can be expressed by the (partial and/or compositional) application order of computations/functions combined with altered copies of said objects which how a Monad models state.}

[shelby3]

Functional reactive programming to avoid the imperative modality of the “spaghetti of listeners” doom, e.g. a practical GUI programming example use case, can be implemented with algebraic effects. I explained algebraic effects in my prior post above.

EDIT: and a follow-up to relate it all back to algebraic effects and explain further the algebraic effects.

EDIT#2: a more holistic explanation of algrebraic effects and it’s relation to the free monad.

[shelby3]

Regarding the discussion of IO monad here, here, and here, I made a summarizing comment.

---

I have referred to making copies of immutable data structures more efficiently, and the official term is persistent data structure.

[shelby3]

Referential transparency doesn’t mean there are no side effects. Referential transparency prevents the side-effect of referenced (through a pointer) shared state, but not state shared through some higher-ordered semantic such as monadic.

@keean wants to declare which effects a function mutates such as:

https://www.microsoft.com/en-us/research/publication/convenient-explicit-effects-using-type-inference-with-subeffects/

What is the advantage of doing so?

[keean]

@shelby3 the advantage is that you can then put constraints on effects like pure (no effects allowed), no heap allocation, no stack allocation, no arithmetic exceptions, which can then be enforced by the compiler.

[shelby3]

Yeah I got that part already, but I’m asking what practical advantage do such coarse grained constraints provide? I’m failing to visualize an example usage which is worthy.

To avoid a kitchen sink design, features must be motivated by use cases.

I noted you are (I think correctly) defining ‘pure’ as “no effects” instead of as just referentially transparent.

[sighoya]

How do you solve bottom-up propagation of effects?

Do you allow to overwrite effects?

[keean]

@sighoya you can infer effects, so that keeps some of the boilerplate down. We can be row polymorphic on effects, IE.specify at least these effects allowed, and we can be negative about effects, everything except this allowed.

I also think that effects that are contained should not escape. So an code that is impure can have a pure interface provided the impurity cannot escape.

[sighoya]

I also think that effects that are contained should not escape. So an code that is impure can have a pure interface provided the impurity cannot escape.

Do you mean that effects of subfunctions inside a function with effects are not propagated upwards?

[keean]

@sighoya

Do you mean that effects of subfunctions inside a function with effects are not propagated upwards?

If they do not escape then yes. Consider a function that uses some internal state for example summing the numbers in a list. We might write:

fun sum(a : [Int]) : Int
   s := {0}
   for i in range(1, length(a))
      s += a[i]
   return |s|

Note, im experimenting with some syntax here '{0}' creates an object containing the value 3, |s| extracts the value of the object s. This function has an imperative implementation, but the interface is pure, anyone using sum does not need to know about the impurity, and can treat it as a pure function.

[sighoya]

@keean

I think the whole function is pure. Local mutations in functions which do not escape don't make a function impure.

What I mean are callbacks which cause effects:

void callback()
    update(1,2) //has effects

[keean]

@sighoya

I think the whole function is pure.

I agree, and Haskell can use the State monad, and runstate is then a pure function. But monads don't compose which makes any attempt to use this very convoluted.

What I mean are callbacks which cause effects

The function that accepts the callback would specify which effects are acceptable. For example in an OS kernel setting an interrupt handler may prohibit memory allocation effects, so that we don't get an OOM in an interrupt handler, which is normally a hard unrecoverable crash (reboot).

[shelby3]

@sighoya wrote:

How do you solve bottom-up propagation of effects?

Do you allow to overwrite effects?

Just don’t do that anymore.