The Leaf Programming Language

A statically typed and interpreted programming language written in Kotlin

View on GitHub

What is Leaf?

The Leaf programming language is a statically and strongly typed, lexically scoped and interpreted programming language using type inference that allows the developer to implement traits and custom types. It is object oriented, but does not support inheritance because typically, it is a common source of maintainability issues.

This programming language was solely written by me for educational purposes only. It should showcase some concepts I learned in my Masters computer science courses at TU Vienna. Although I am sure it could technically be used as production ready language, I would not recommend it yet.

Leaf by Example

This section shows you how to code using the leaf programming language.

Hello World

First off, let's start with the most common code example in the history of programming; the "hello world" program. Leaf exports certain functions by default from it's core. One of these is the println function that takes zero to any number of parameters.

println("Hello World")

Variables

Variables can be used like in any other programming language. Leaf, especially, distinguishes between const and var. Constants cannot be modified after setting a value for the first time, variables, on the other hand, can. Since Leaf is a statically typed programming language, each declaration of a new variables requires either an initialization or a type specification.

const a                   // invalid
const b: string           // invalid
const c = 10              // valid
var d: string = "Hello"   // valid
var e: number = true      // invalid

(be careful to always match the declared type with the type of the r-value, otherwise, the static semantic analyzer is going to produce an error)

If Expression

Leaf knows different kinds of control structures. One of these is the if conditional expression. The interpreter will execute different branches based on a given predicate. The value of the last expression in the if or else branch will be returned an can be used in any other kind of expression or statement.

const a = if false {
  "This is impossible"
} else {
  "This is the else branch"
}

Loop Statement

Another very useful control structure is the loop. It is used to run a single code block multiple times. Compared to other programming languages, Leaf only knows this one kind of loop. A loop head consists of three blocks. The init block that is run before the first loop iteration, the condition and the step block that are both executed after each iteration.

loop var i = 0 : i < 10 : i = i + 1 {
  println("This is iteration " + i)
}

But loop can also be executed with only a condition block or without any block at all in the head. In the latter case, the loop will run endlessly and has to be broken with break for example.

loop isHungry() { eat() }
loop { break }

Functions

Functions are basically a piece of code that is reusable and can be parameterized. Leaf not only supports functions, but functions are a first level-citizen of the programming language. This means that they are treated in the same way like variables are. A function definition might look like the following:

fun sayHi(to: string) {
  println("Hi " + to)
}

First level functions allow the developer to create very powerful constructs using the functional programming paradigm. They implement the Lambda calculus and can be used like parameters to other functions creating higher-order functions.

fun compute(num: number, comp: fun) {
  const result = comp(num, num)
  println("Result: " + result)
}

// Invoke like:
compute(10, fun (a: number, b: number) = a * b)

Besides the well known function parameters and the function body, functions in Leaf do have some unique capabilities that are unusual compared to other programming languages. In the Leaf programming language, you can specify pre- and post-conditions (also known as variant and covariant) for input and output parameters as well. The pre-condition checks if the input parameter do match some formal definition while the post-condition checks if the evaluation of the function body yield a valid result. You can access the return value (the result) of the function by using the reserved _ variable.

fun factorial(n: number) : n > 0 : _ > 0 -> number {
  if n == 1 {
    return 1
  }
  return n * factorial(n - 1)
}

factorial(10) // valid
factorial(-2) // will produce a runtime error

The program will produce an error if either the pre- or post-condition is not met. Pre-conditions are especially useful to guide the developer using your function into the correct direction. Post-conditions are very useful as kind-of "regression test". They ensure that the condition is met even if you change something in the function body.

Custom Types

Besides the built-in data types (like number, string or bool), Leaf allows you to define your own custom data types. These are basically records that can be extended using functions.

type Human {
  name: string
  sex = "female"
  mom: Human, dad: Human
}

fun <Human>.sayHi(to: Human) {
  println(object.name + " says hi to " + to.name)
}

const mom = new Human { "Anna Anderson" }
const me = new Human { "Peter Peterson", sex = "male", mom }

me.sayHi(mom)

Functions that are an extension of some type have to be written in <...>. You can specify as many types for a single function extension as you like (separated with comma). Properties of a type can then be accessed via the reserved object keyword. This is similar to this in other programming languages, however, the object variables is inferred dynamically and based on the types structure at runtime in Leaf. This allows for declaring multiple extensions for one function.

More Examples

For more examples, please visit the GitHub page of the programming languages. You will find some interesting use cases and even some games written in Leaf to get started.

Language Specification

The formal language definition in Backus-Naur form looks like the following. Feel free to implement it yourself.

Statements

program    ::= statements
block      ::= '{' (NL)* statements (NL)* '}'

statements ::= statement ((';' | (NL)*) statement)*
statement  ::= ('const' | 'var') (NL)* declaration
             | 'async' statement
             | 'return' ((NL)* expr)?
             | 'break'
             | 'continue'
             | type-declaration
             | assignment
             | loop-stmt
             | expr

Functions

fun-declaration ::= 'fun' (NL)* (fun-extension (NL)*)? (name (NL)*)?
                     (fun-params (NL)*)?
                     (fun-requires (NL)*)?
                     (fun-ensures (NL)*)?
                     (fun-returns (NL)*)?
                     (fun-body)

fun-extension ::= '<' type (NL)* (',' (NL)* type (NL)*)* '>' (NL)* '.'
fun-params    ::= '(' (NL)* declarations (NL)* ')'
fun-requires  ::= ':' (NL)* expr
fun-ensures   ::= ':' (NL)* expr
fun-return    ::= '->' (NL)* type
fun-body      ::= block
                | ('=' (NL)* statement)

Turing Completeness

As you might have already guessed, the Leaf programming language is indeed Turing complete. This means, that it is basically powerful enough to solve any problem that can also be solved by any other programming language (to be precise: by any other Turing machine).

Turing completeness can be shown by implementing a mapping between the WHILE and the Leaf programming language. The WHILE programming language is proven to be Turing complete and is defined as follows:

C ::= L := E
| 'if' B 'then' C 'else' C
| 'while' B 'do' C
| C;C
| skip

B ::= 'true' | 'false' | E '=' E | B '&' B | '-' B
E ::= L | n | (E + E)

The (bidirectional) mapping from WHILE to Leaf can be implemented as isomorphism function and looks like the following (WHILE on the left hand side and Leaf on the right hand side):

C <=> declaration | assignment
    | if-expr
    | loop-stmt
    | statements
    | empty

B <=> 'true' | 'false' | expr
E <=> expr
L <=> name

Therefore, every program written in WHILE can also be expressed in Leaf without loss of semantic meaning. The proof is complete and Turing completeness has been shown.