A programm in Lazi is just a formula. So how can it write to a screen if there is no special input/output functions ? Lets say f is the program, it's a formula, to execute it we use an argument "U" and we compute f U. U is a formula représenting the universe from the point of view of f. But from our point of view, U can be partialy composed of our real universe. For example, if f is a program for printing the word "Hello" in stdout, then we can define f like this :
$Let f = $F U@$O[print] → print 'Hello
"print 'Hello" returns the universe resulting of the printing of Hello on stdout.
If you dislike abstractions you can bypass this part which is just a deep explanation of the paradigm behind :
In practice the representation needed for U is a very small part of the representation of our universe (phew!). But sometimes it can be more than just computer stuff, for exemple if f manage a plane then we can prove that f don't crash and don't crash the plane by having a representation of the plane in U that will be used to make mathematical proofs.
Lets see an example where U is unrelated to our universe and very simple, so f run in a complete virtual universe. The universe contain a data (called "screen") for either nothing either a word, and a function to change what is on the (virtual) screen. This example run the program and extract what is on the screen. The argument of f is a uniserve containing a "print" function.
$Let U = $O[
print = $F x → objSet this 'screen (just x)
We can run this program in the sandbox :
$Let f = $F U@$O[print] → print 'Hello; $Let U = $O[ screen = nothing; print = $F x → objSet this 'screen (just x) ]; (f U).o'screen
The result is "just 'Hello".
If we want to run f in our real universe, we use special interpreter/compiler which execute the print when the print function is evaluated and return the new U.
This way of managing inputs/ouputs has many advantages :
- U can be changed to adapt the program for testing, debuging, or for an OS or an other etc.
- Even if we deal with the real world, we can easily do mathematics on the program because all the external things is represented by U.
- U can be used like if it was a mutable global variable, the framework manage the translation into pure functions (for the mathematics) and types checking manages the control of the side effects.
- We can translate any program in any language as a pure functional program and finaly as a Lazi program.
Even if it's obvious in the world of Lazi, it's better to say it : we can construct abstractions to avoid the weight of manipulating U everywhere. In the example below f can use just "print"
Type checking could look like this.
// The type says that f is a function using the argument U to write in stdout and an integer. nothingT is the type of element in the empty set, hence we know that f is just modifying U.
type f : using(stdout) : $F integerT → nothingT
$Def f = $F x → print (g x)
This is an example of type, type system in Lazi is unlimited because it's free mathematic sentences.
Inputs are managed similarely to outputs.
This design has some issues to handle, these are details but it may interest you.
The solutions presented here may seems sometimes heavy but mathematic representation can be translated in a way that real program are fast and light.
What happens if a U.o'read is duplicated by the evaluation of a formula (Lazi use lazy interpretation) ?
To resolv this problem the interpreter/compiler has to share evaluations, hence when a formula "U.o'read" is evaluated, the other copy is replaced by the value. The actcual interpreter has already this behaviour.
How to avoid parallel access to the universe ?
How interrups are managed in this paradigm ?