Stella Core Features

Stella Core is a minimalistic simply-typed purely functional programming language with two base types (Bool and Nat) and function types.

A Stella Core program consists of a collection of function declarations:

language core;

fn function_1(x : <some type>) -> <some type> { <function body> }
fn function_2(y : <some type>) -> <some type> { <function body> }
...
fn main(arg : <some base type>) -> <some base type> { <function body> }

All functions at the top-level must have different identifiers and at least one of the functions must be called main. The latter serves as an entry point of the Stella Core program.

Types

Stella Core supports only booleans and natural numbers as base types and single-argument function types.

Booleans

A value of type Bool is either true or false. The only built-in expression for booleans is the conditional expression:

  • if c then x else y returns x if c is true and y otherwise.

The conditional expression if c then x else y has type T whenever both x and y have type T and c has type Bool.

Functions

Each function declaration consists of its signature and body. The signature of a function introduces its name, arguments, their types, and the return type of the function. The body of each function consists of a single return statement with an expression.

For example, the following declaration introduces a function plus2 which takes an argument n of type Nat and returns an expression succ(succ(n)) of type Nat:

fn plus2(n : Nat) -> Nat {
  return succ(succ(n))
}

In Stella Core, all functions have exactly one argument. A type of a function is written as fn(T1) -> T2 where T1 is the type of the argument and T2 is the return type. Both T1 and T2 are allowed to be function types. Thus, Stella Core fully supports higher-order functions.

fn Bool::not(b : Bool) -> Bool {
  return
    if b then false else true
}

The function Bool::not above is an example of a simple function of type fn(Bool) -> Bool. Note that Bool::not is a single identifier (:: is not an operator, it is part of the identifier).

Let us consider now a higher-order function example:

fn twice(f : fn(Bool) -> Bool) -> (fn(Bool) -> Bool) {
  return fn(x : Bool) {
    return f(f(x))
  }
}

Function twice here has type fn(fn(Bool) -> Bool) -> (fn(Bool) -> Bool), meaning that it takes a function of type fn(Bool) -> Bool as an argument and returns a function of type fn(Bool) -> Bool.

We can call this function from main:

fn main(b : Bool) -> Bool {
  return twice(Bool::not)(b)
}

Twice will apply Bool::not function twice to b, yielding the same value it started from.

Anonymous Functions

In our previous example, we used a local function called g right before returning it as is. In situations like this, we do not actually care about the name of the function, so we could use anonymous functions instead.

An anonymous function has the same syntax as regular function declaration, except the name of the function is not there and return type is not specified. The entire thing is treated immediately as a value, so can be used in an expression:

fn twice(f : fn(Bool) -> Bool) -> (fn(Bool) -> Bool) {
  return fn (x : Bool) { return f(f(x)) }
}

Natural Numbers

A value of type Nat is either 0 or succ(n) where n is another value of type Nat. For example, succ(succ(succ(0))) is the representation of a natural number 3.

Note that even though succ acts like a function, it is not one. Instead, succ is a constructor of values of type Nat. It can be thought of as a runtime tag that does not modify the data it is applied to, but only "tags" it.

Natural literals are not a part of Stella Core, but can be enabled with natural literals extension.

Nat type supports only two built-in operations:

  • Nat::iszero(n) returns true if n is equal to 0, and false otherwise;
  • Nat::rec(n, z, s) represents primitive recursion over the natural numbers:
  • n is the input natural number.
  • z is the default (or initial) value.
  • s is a function that will perform one step in the recursion.
  • Nat::rec(n, z, s) is equivalent to s(0)(s(1)(...(s(n-1)(z))...)) where s is used n times.

You can understand Nat::rec(n, z, s) also as a restricted version of a for loop:

result = z;
for (int i = n-1; i >= 0; i--) {
  result = s(i, result);
}

The typing of Nat::rec(n, z, s) happens as follows:

  • n has to be of type Nat;
  • z can be of any type T;
  • s has to be of type fn(Nat) -> (fn(T) -> T);

All other operations on Nat, such as comparison, addition, and multiplication can be defined in terms of Nat::rec. The natural operations extension provides built-in versions of those.

For example, we can implement addition of natural numbers as follows:

fn Nat::add(n : Nat) -> (fn(Nat) -> Nat) {
  return fn(m : Nat) {
    return Nat::rec(n, m, fn(i : Nat) {
      return fn (r : Nat) {
        return succ(r)
      }
    })
  }
}

We can call this function from main:

fn main(n : Nat) -> Nat {
  return Nat::add(n)(succ(succ(0)))
}

Recursion

Stella Core does not allow general recursion. Recursive and mutually recursive functions are prohibited. Instead, users may only rely on primitive recursion in the form of Nat::rec. This in conjunction with a simple type system makes Stella Core a total language, meaning that all well-typed programs in Stella Core are terminating.

General recursion can be added with general recursion extension.