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, postProcess
foo (input A) B is p := input.prepare q := p.perform r := q.postProcess r
foo is called somewhere deep within a large
application, e.g., it is called by
bar (input C) D is .. 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
which in this examples represents the hundereds of features that sit between the
main feature and
The idea is to mark such data as 'global' and automatically lift callers to
pass this data through, i.e., we would declare
foo (input A) B global (l Log) 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)
Then, the compiler could automatically add an implicit
global (l Log)
Log to all features like
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
- debugging output
- Timeouts / Interrupts
- user input
- stdout output
- stderr output
- file i/o
- network i/o
- thread local data
- exceptions (requires wrapping result and automatic continuations)
- multiple results, e.g. lifting
sqrt(f f64) f64to
sqrt(f f64) list<f64>such that it can return 0, 1, or 2 solutions, whithout manually adding the case distinction to all uses the result.
- yield and coroutines
- stack trace printing
- implementing the equivalent to unix 'head', i.e., stopping after 10 lines of output
- 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 modelled easily by wrapping them into types, e.g., stdout<IO>, stderr<IO>?
We could treat monadic parameters like a more general form of type parameters. So a feature would declare three types of formal parameters: Formal arguments, formal type 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 is o.action msg # hello will be monadically lifted automatically hello (name String) unit is 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> : Output<A> is # action uses stdout to perform I/O: action (s String) stdOut<A> is # 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> : Output<A> is # action is a NOP for noOutput, we perform no I/O! action (s String) noOutput<A> is noOutput.this
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> ref : Monad is container (data A) is bind<B> (f fun (A) B) Output<B> is wrap f data return (x A) container x wrap <B> (x B) Output<B> is abstract action (s String) is abstract # as long as there is no syntactic sugar to implement wrap # generically as in # # wrap <B> (x B) Output<B> is like Output.this<B>.return x # # we will need to redefine wrap in all implementations of Output: # redef noOutput.wrap <B> (x B) Output<B> is noOutput <B>.return x redef stdOut .wrap <B> (x B) Output<B> is stdOutput<B>.return x
Logically, what will happen to the example above after lifting, is this
# say will be duplicted for each actual monadic parameter say1 (msg StdOut<String>) StdOut<unit> is msg.action msg.container.bind(fun (x String) String => x) say2 (msg noOutput<String>) noOutput<unit> is msg.action msg.container.bind(fun (x String) String => x) # hello will be duplicted for each actual monadic parameter hello1 (wrappedName stdOut<String>) stdOut<unit> is wrappedName.bind(fun (name String) String is say1 stdOut<String> "Hello " + name + "!" hello2 (wrappedName noOut<String>) noOutput<unit> is wrappedName.bind(fun (name String) String is 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 is 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 is 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