Lazi

Inputs,Outputs

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 :

I suggest you seek to prove or deny this sentence :
The universe is computed in a lazy way (the computation occurs only when needed) just for my existence and nothing else.

In fact you can't prove that it's true of false. We use this impossibility property for f by placing f in the center of the computation. When we want to see f U as a formula, we suppose that the universe is computed in a lazy way just to compute f. In this view U is computed each time f has interaction with it (read or write).

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[

screen = nothing;
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) ?

For example : "($F x → g x x) U.o'read"
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 ?

For example in "f (U.o'readFile 7 , U.o'readFile 4)", the first evaluation return a universe which should be used for the other evaluation, because the reading change the Universe. To resolve this we have to serialize the access. f (g U) (h U) must be translated into $Let U2 = g U; f U2 (h U2).

How interrups are managed in this paradigm ?

Interrupts can trigger a modification of U, for exemple the interrupt 10 can be used to call "f U 10" which compute the new U. The computation of the new U can occure just before the running function has finish to modifie U. If we want to translate a program using interrups into a function, we need to insert some checks of the interruption state after each computation of a new U. If an interrups triggers an exit we need to translate the need to exit by an "exit flag" in U.