Lazi

Lazi Tutorial

A brief presentation

This tutorial is a sequence of short lessons to introduce you to the programming in Lazi. Because Lazi is special by puting a mathematic foundation in the center, we don't have the space to explain the big picture here. Briefly Lazi is new concept of language, it is :

  • purely functional (like Haskell)
  • purely mathematic (a mathematic foundation is defined at first and the heart of the language)
  • auto-constructing (even variables, types and input/output are constructed!)

A sandbox is provided to let you experiment lazi, see https://lazi.bobu.eu/online/

At the start : 4 words and 8 rules

Every lazi programs can be translated in a formula using 4 words ("if", "1b", "0b", "distribute"). To compute this formula you need 8 rules. For the curious I give the rules below :

  • "if", "1b", "0b", "distribute" are words
  • words are formulas
  • for some formulas x,y,z :
    • "x (y)" is a formula
    • "if (1b) (x) (y)" is computed in "x"
    • "if (0b) (x) (y)" is computed in "y"
    • "distribute (x) (y) (z)" is computed in "x (z)(y (z))"
    • if x is computed in y then "x (z)" is computed in "y (z)"
    • if x is computed in y then "if (x)" is computed in "if (y)"

One of the beauty of Lazi is that even a very big program, like a software to control a plane, can be translated in a unique formula using these 4 words (yes I know, even with the inputs/outputs). To understand how it's possible you need to read some theory.

It's not "1" of "true" but "1b" because it's a bit. "True" and "False" are mathematical constructions which come later.

Lets do our first experiment : using the sandbox, lets compute the formula "if 0b 0b 1b". "if" is a function with 3 arguments, if the first is 1b then it return the second, else it returns the third.
In Lazi formulas are a word or an application of 2 formulas, the one on left is called the function and the one on right is called the argument. if 0b 0b 1b reads (((if 0b) 0b) 1b), so "if" is seen as a function, as "if 0b", as "(if 0b) 0b)". With Lazi you can see the very basic nature of functions and arguments, which is just being on left or right part. Later higher level notions of function and argument will be constructed, which will correspond better of what you are used to. But it will be just a start, because Lazi construct itself endlessly.

You can see in the result page that it computed "¬b 0b", this is because it's the same thing and the translater prefer to print more readable formulas.

From the emptyness to big things

Perhaps you don't beleive that these few words and rules, without the concept of function or variable can be usefull.

So lets compute this formula : ∀l x/$L[ 0b, 0b, 1b, 0b]; x
which means "for all x in the list ( 0b, 0b, 1b, 0b) , x is 1b". It computes to 0b.

This formula contains a variable "x" and a loop on a list. This formula can be translated in the basic lazi formula, you can see the translation here.

You can copy past this big formula and compute it in the Lazi's sandbox.

Lets start by the start

The first definition of the lazi's foundations is the identity function :
$Def identF = if 0b 0b

This is the identity function because if 0b 0b x computes in x, so identF x computes in x.

We have a '$' to mark a syntax construction, this means that "$Def" can not be translated alone to a formula. In Lazi we need to let space for future new syntaxes, for example we use '$L[ ... ]' for (and not just '[ ... ]').

Sadly the sandbox can't use global definitions, but you can replace it by a local definition to test it:

$Let identF = if 0b 0b;
identF $L[ 0b, 0b, 1b, 0b]

The sandbox know identF, but the local definition supersed the global one.

In lazi you need just "$Def" to define every global things (types, function, data etc). You will encounter this simplicity everywere in Lazi.

So, what is this "lazi's foundations" ? It's the heart of Lazi : a mathematic foundation which allow us to create safe extensions and empower the language without any kind of limit.

A data structure

Lazi constructs itself, data structure, types, mathematic foundation, compiler etc. Here we construct our first data structure, pairs :

$Def pair = $F x,y,c → if c x y

So we define the name "pair", it's equal to the function with 3 arguments x,y,c which return if c x y. x and y are the data stored in the pair. So for exemple "pair a b" is the pair "(a,b)", to get the first element you apply the argument 1b to pair a b (pair a b 1b is equal to if 1b a b which is equal to a).

Let try this :
$Let pair = $F x,y,c → if c x y; pair $L[ 0b, 1b ] 0b 1b

Some syntax : () ; ,

In Lazi "," and ";" have the same role, you can use one or the other as you want. For exemple, lets try the last formula but invert "," and ";" :
$Let pair = $F x;y;c → if c x y, pair $L[ 0b; 1b ] 0b 1b
As in natural language, this is usefull to express strongness of the splits.

We can use commas (or a ";" of course) inside parenthesis, this is a shortcut, like this :
(x ; y) means (x)(y), (x,y;z) means (x)(y)(z) etc.
it's a syntactic suger, replacing "," (or ";") by ")(".

You can use for example :
if ( isThing m ; f \ getThing m; x )
this way it's lighter than
if ( isThing m ) (f \ getThing m) x

This is why Lazi has no special syntax for "if" as Haskell (with its "if x then y else z").

For a big "if" you can write it like this :
if ( p i ) (

$F d → this .o'translateEvents (getType tn .o'translateThis j d) p
,
$F d → $T[
'eDeduction,
mapDeductions i $F deductionT,k → deductionT .o'translateEvents k p,
i .o'object .o'translateEvents d p
]
)

A fun fact is that with this notation you can have a Lazi formula which seems a non lambda calculus formula, like "add(x,y)". But the last formula is also equal to (add,x,y) in Lazi.

An other usefull syntax is "\" which is like the "$" of Haskell (but here it's purely syntactic). "x \ y" translate to x (y) whatever x and y is, provided x don't contain a "\". This syntax is usefull to avoid to put parenthesis around the last argument. For exemple we can write "f \ getThing m" instead of "f ( getThing m )". This is very usefull when the last argument is long.
We can combine them : "x \ y \ z" means x ( y (z) ).

Our first type : nothingT

$Def nothingT = $O[
  domain = constF 0b
]

This type is the simplest mathematic structure : the empty set without additionnal function (no need, even equality, because there is no element.

Our first type : dynPairT

Lazi is like mathematics: things have no label to say "this is my type". In set theory mathematic we can see 5 as an element of ℝ,ℕ,ℚ and even as a set. This is why a type in lazi is like a structure in mathematics: it's a set with some function associated (the equal function is mandatory). A type in Lazy can have parameters, this is the case of dynPairT below which have 2 parameters (t1 and t2f).

dynPairT is the type of a pair x1 x2 where the type of x1 is t1 and the type of x2 is "t2f x1". So the type of the second argument depends on the value of first argument.

This definition of dynPairT is :

$Def dynPairT = 
  $O($O[t1,t2f])[
	domain = $F i@$T[x1,x2] → isPair i ∧b  x1 ∈t t1 ∧b x2 ∈t t2f x1
  ,
	equal = $F $T[x1,x2],$T[y1,y2] → (t1 .o'equal) x1 y1 ∧b (t2f x1 .o'equal) x2 y2
  ,
	object = $F $T[x1,x2] → $T[t1 .o'object x1 , t2f x1 .o'object x2 ]
  ,
	map = $F $T[x1,x2],f → $T[ f t1 x1 , f (t2f x1) x2 ]
  ,
	fold = $F $T[x1,x2],f,r → f (t2f x1) (f t1 r x1) x2
  ]

Lets explain some parts of this code :

  • $0 is used to construct an object. An object in Lazi is like a sofisticated associative array.
  • The "($O[t1,t2f])" means that t1 and t2f are entries of the object but defined elsewhere. Hence we can define
dynPairT with t1 and t2f as parameters.
  • domain is the first entry, it's the definition of a function ( $F) to define what data belongs to the type. So for some t1,t2f, if domain x = 1b then x belongs to the type. The argument of the function is special, it's pattern mathching, as in Haskell.
  • equal is the equality between members of the type. "t1 .o'equal" is the function "equal" of the type t1.
  • object is not related to the "object" data structure in Lazi. It means "the goal", that is what is represented by the data. This is often usefull because we often use something to represent something else. For example the object of a proof is the sentence deduced by the proof. Don't worry about that.
  • map and fold are function specific to this type.
Testons ce type :

$Let  dynPairT = 
  $O($O[t1,t2f])[
	domain = $F i@$T[x1,x2] → isPair i ∧b  x1 ∈t t1 ∧b x2 ∈t t2f x1
  ,
	equal = $F $T[x1,x2],$T[y1,y2] → (t1 .o'equal) x1 y1 ∧b (t2f x1 .o'equal) x2 y2
  ,
	object = $F $T[x1,x2] → $T[t1 .o'object x1 , t2f x1 .o'object x2 ]
  ,
	map = $F $T[x1,x2],f → $T[ f t1 x1 , f (t2f x1) x2 ]
  ,
	fold = $F $T[x1,x2],f,r → f (t2f x1) (f t1 r x1) x2
  ];
$Let t = dynPairT wordT \ $F  c → if(wordT o'equal c 'w ; wordT ; anythingT)

Where are the types declarations ?

Lazi constructs itself and construct the definitions and compilation of languages. We start without types declaraction. We will construct it later, using, guess what ?, mathematics. This is why types declarations will be extensible and will support high level of constraints without limits. This is very powerfull to remove bugs.

The steps of the construction of Lazi are :

  • define tools (done)
  • define the mathematic foundation (done)
  • define the Lazi computer langage as a mathematic object (so we can manipulate it, for exemple to check types, compile it etc. (some tools done, lot of work to do).
  • more steps, Lazi contains a full representation of itself, by full I mean logic included (the mathematic foundation).