Automatic Monadic Lifting

The presence of I/O, dependencies on time, logging, etc. makes functions impure, e.g., imagine we have a function foo that processes input of type A into output of type B in three steps prepare, perform, post-process

  foo (input A) B =>
    p := input.prepare
    q := p.perform
    r := q.postProcess
    r

Now imagine foo is called somewhere deep within a large application, e.g., it is called by bar:

  bar (input C) D =>
    .. some code ..
    x := foo(y)
    .. more code ..

Now, we would like to add logging to foo while keeping it a pure function, so we convert it into

  foo (input A, l Log) (B, Log) is
    p := input.prepare
    l := l.append "prepared"
    q := p.perform
    l := l.append "performed"
    r := q.postProcess
    l := l.append "postProcessed"
    (r, l)

How can we change the whole application to pass a proper logging object into the application without manually adding Log to bar, which in this examples represents the hundreds of features that sit between the main feature and foo?

Monadic Lifting

The idea is to mark such data as 'global' and automatically lift callers to pass this data through, i.e., we would declare foo as

  foo (input A) B global (l Log) Log =>
    p := input.prepare
    l := l.append "prepared"
    q := p.perform
    l := l.append "performed"
    r := q.postProcess
    l := l.append "postProcessed"
    (r, l)

Then, the compiler could automatically add an implicit global (l Log) Log to all features like bar.

What remains to be done is to add a means how to specify the logging mechanism in the application's main feature (or at an intermediate level depending on the logic of the application, e.g., for the main features of threads.

  main is
    mylog := MyLog "/var/log/main.log"
    (result, _) := bar input using mylog  # call bar on input specifying logger mylog, ignoring result logger

If we extend this to file I/O, MyLog in this example might itself require a global monadic parameter as in

  main is
    (mylog, _) := MyLog "/var/log/main.log" using fileIO
    (result, _) := bar input using mylog

What mechanisms could be handled like this? Maybe the following

• Logging
• debugging output
• Time
• Timeouts / Interrupts
• user input
• stdout output
• stderr output
• file I/O
• network I/O
• thread local data
• permissions
• exceptions (requires wrapping result and automatic continuations)
• multiple results, e.g. lifting sqrt(f f64) f64 to sqrt(f f64) list f64 such that it can return 0, 1, or 2 solutions (depending on f < 0, f = 0 or f > 0), without manually adding the case distinction to all uses of the result.
• yield and co-routines
• stack trace printing
• implementing the equivalent to Unix 'head', i.e., stopping after 10 lines of output
• implementing target-specific layers, e.g.,
  • a module providing 3D graphics routines needs to be based on top of an underlying library such as JavaFX or OpenGL. If there was a monad providing an abstract target interface, we could at build time decide which one to use for a specific target.
  • a security library requires cryptographic strength random numbers, the source that provides these could be very different on a desktop, a cloud server or a small embedded device. So instead of hard-coding one source of random numbers, one could put these in a monad and keep the implementation choice open until the system is built for a specific target.
• selecting floating-point rounding mode or precision

Open questions:

• What to do if main does not provide the global parameters?
• We could use a unit type monad as a default?
• How should the type of the global parameter be specified? Like a generic type parameter with a constraint, or a fixed type, possible a ref type with dynamic binding?
• should it be possible to not only add a global type to the result, but to wrap the result and fully replace it? Then, the remaining code of a caller must be treated like a continuation.
• How is this done in other languages? Haskell?
• What is the best syntax for this?
• Should it be possible to have several global parameters of the same type, e.g., several loggers for different purposes, several permissions, etc.? Or can these be modeled easily by wrapping them into types, e.g., stdout IO, stderr IO?

Monadic Parameters

We could treat monadic parameters like a more general form of type parameters. So a feature would declare three types of formal parameters: Formal type arguments, formal arguments and formal monadic arguments. The formal monadic arguments would then be used not to modify the feature itself, but to modify its callers by automatic monadic lifting up to the application's / thread's main feature.

An example could be a monad for stdout:

  # prints given String using Output monad o
  say [o Output] (msg String) unit =>
    o.action msg

  # hello will be monadically lifted automatically
  hello (name String) unit =>
    say "Hello " + name + "!"

  # and main has to provide actual monads when calling hello
  main is
    hello [stdOut  ] "Alice"    # will print "Hello Alice!"
    hello [noOutput] "Bob"      # will not print anything
    hello [stdOut  ] "Claire"   # will print "Hello Claire!"

How can stdOut and noOutput be implemented? These will need to be compatible to Output, e.g. as follows:

  stdOut (A type) : Output A is
    # action uses stdout to perform I/O:
    action (s String) stdOut A =>
      # stdout.println is an intrinsic that returns the first argument
      # (unchanged, but we don't tell anybody) and prints the second.
      stdout.println stdOut.this s

  noOutput (A type) : Output A is
    # action is a NOP for noOutput, we perform no I/O!
    action (s String) noOutput A =>
      noOutput.this

And Output must implement the magic of a monad:

  # Output inherits from an abstract monad. Output is a ref such that its
  # type is assignment compatible to heirs like stdOut and noOutput.
  Output (A type) ref : Monad is

    container (data A) is
      bind(B type, f fun (A) B) Output B => wrap f data

    return (x A) container x

    wrap (B type, x B) Output B => abstract

    action (s String) is abstract

  # as long as there is no syntactic sugar to implement wrap
  # generically as in
  #
  #  wrap (B type, x B) Output B => like (Output.this B).return x
  #
  # we will need to redefine wrap in all implementations of Output:
  #
  redef noOutput.wrap (B type, x B) Output B => (noOutput B).return x
  redef stdOut  .wrap (B type, x B) Output B => (stdOutput B).return x

Logically, what will happen to the example above after lifting, is this

  # say will be duplicated for each actual monadic parameter
  say1 (msg StdOut String) StdOut unit =>
    msg.action msg.container.bind(fun (x String) String => x)

  say2 (msg noOutput String ) noOutput unit =>
    msg.action msg.container.bind(fun (x String) String => x)

  # hello will be duplicated for each actual monadic parameter
  hello1 (wrappedName stdOut String) stdOut unit =>
    wrappedName.bind(fun (name String) String =>
      say1 (stdOut String) "Hello " + name + "!"

  hello2 (wrappedName noOut String) noOutput unit =>
    wrappedName.bind(fun (name String) String =>
      say2 (noOutput String) "Hello " + name + "!"

  # main will call hello1 or hello2 with actual instances of the monads
  main is
    hello1 (stdOut   String).container "Alice"
    hello2 (noOutput String).container "Bob"
    hello1 (stdOut   String).container "Claire"

What the compiler will create, however, will most likely look more like this:

  # say will retrieve output from some thread local data structure
  say (msg String) unit =>
    threadLocal.output.action msg

  # hello does not need to care at all for simple monads where bind
  # executes f on the contained data once.  In case bind could in some
  # cases not call f at all (option, result) or could call f repeatedly
  # (list), hello would have to be changed by the compiler accordingly.
  hello (name String) unit =>
    say "Hello " + name + "!"

  # main will set the thread local output monad
  main is
    threadLocal.output.push stdOut;   hello "Alice";  threadLocal.output.pop
    threadLocal.output.push noOutput; hello "Bob";    threadLocal.output.pop
    threadLocal.output.push stdOut;   hello "Claire"; threadLocal.output.pop

Monadic Parameters for System Configuration

Using monads for everything related to connecting to the outside world could provide a very nice way to list what a system does and to configure it when building for a particular target.

Monadic Parameters provided by back-end

Specific back-ends could provide their own default monads that map to the features provided by their specific targets, e.g., the Java APIs for a JVM backend or the system libraries for a native backend.

Monadic Lifting Examples

Man-or-Boy

I use Knuth's Man or Boy test as a small example with a quite awful side-effect.

Here is the original Fuzion code that updates a field k in the closure of feature b:

Using the handles-monad, this code can be made fully functional without requiring updating a field, but with lots of additional boilerplate. This is similar to using Haskell's ioRefs. Here is the corresponding Fuzion code:

Supporting one-way monads as part of an execution environment, the syntax could be simplified by providing a means to register a monad in the environment of the current thread. The resulting code could, e.g., look something like this:

The resulting semantics would be just like the explicit use of the monad.

Output Postprocessing

The following example uses the default io.out monad to print Hello World! three times. So far, this is nothing special.

Now, create a new instance of io.out that pre-processes the output by adding *** in front of every line that is printed. We can add this preprocessing without modification of the code that does the printing, it suffices to execute it in the context of a different instance of the io.out monad:

The kind of post-processing that is done does not matter. Alternatively, here is an example that translates the text to Danish before printing:

Next, we would like to add line numbers to the output. This is a little tricky since this requires that we store the current line number somewhere. Since Fuzion does not have static fields or singletons, the only means we have is another monad, in this case a state monad. We therefore use a state monad to store the number of lines printed so far and run the code in the context of an instance of this monad:

The previous example uses a state monad containing a value of type i32 without providing any clue what this value means. To convey a meaning, we can wrap the value into a new type as shown in the next example that defines a new type line around a value of type i32.

Wrapping a value in a one-way state monad permits to distinguish several values of the same basic type with different meanings. The following code extends the previous example by counting the total number of bytes written (excluding line numbers and linefeeds for simplicity of the example). Both, the line numbers and the byte counts use a value of type i32 that is wrapped into two different types, line and bytes:

Early return

Now, we use the previous example to limit the amount of computation that is performed within a oneway monad. The run feature now runs an endless loop printing Hello World! repeatedly without ever halting. However, we use the state monad that counts the number of lines printed to return early from the computation as soon as three lines have been printed.

Note that this does not only limit the output to three lines, but it stops the execution of the code after those lines were printed and does not return to feature run that executed an endless loop, but returns directly from the current oneway monad of type io.out.

Effects

effect is a specific onewayMonad that can be used to define effects similar as in koka. Here is a small example creating coroutines that communicate via a generator effect that defines an operation yield:

Using the same example with different sources that yield values to different sinks:

Related Work

Effect Systems: The use of automatic monadic lifting in Fuzion can be seen as an implementation of an effect systems that uses the types of monads as the names of effects.

Stephen Diehl wrote a nice blog post on effect systems, a language using an effect system is koka.

One impression I have is that Fuzion's automatic monads would typically be used at a much finer granularity than what effect systems currently do (i.e, not just say something is non-deterministic or modifies 'heap', but clearly state that a function uses, e.g. random i32 and provide the possibility to replace the generator for these random numbers by something else (like a predefined list of values for reproducible testing or a quantum-mechanics based source of true randomness).

A paper presenting an efficient implementation of effects: Ningnin Xie et al: Effect handlers, evidently, Proc. of the ACM on Programming Languages.