Example usage:

git clone https://github.com/maiavictor/formality
cd examples

# Interpreter evaluation
formality everything.formality.hs -e not_true 

# SIC evaluation
formality everything.formality.hs -s -f not_true 

# Type-checking
formality everything.formality.hs -t add
formality everything.formality.hs -t add-comm

Formality is a very simple language. Its programs are composed of just two building blocks: inductive datatypes, which represent data formats, and functions, which represent computations over those types of data. And that's all you need.

One of the simplest types, the boolean, can be declared as:

data Bool : Type
| true    : Bool
| false   : Bool

And the negation function as:

let not(b : Bool) =>
    case b  -> Bool
    | true  => Bool.false
    | false => Bool.true

Pattern-matching is used everytime we want to inspect the value of a datatype.

One of the simplest recursive types, the natural number, can be declared as:

data Nat : Type
| succ   : (n : Nat) -> Nat
| zero   : Nat

And a function that doubles it can be written as:

let double(a : Nat) =>
    case a       -> Nat
    | succ(pred) => Nat.succ(Nat.succ(fold(pred)))
    | zero       => Nat.zero

Since Formality is total, recursion is performed by using the fold keyword, which is available inside cases of a pattern-match. It allows us to recursivelly apply the same logic to structurally smaller values.

Types can be easily parameterized:

data Pair<A : Type, B : Type> : Type
| new : (x : A, y : B) -> Pair

Declaring polymorphic functions is as simple as taking types as arguments:

let fst(A : Type, B : Type, pair : Pair<A, B>) =>
    case pair   -> A
    | new(x, y) => x

That allows you to reuse the same implementation of a function for multiple concrete types, a powerful, ancient trick that certain "modern system languages" surprisingly couldn't get right.

Formality allows types to be parameterized not only by other static types, but by runtime values: we call those "indices". The classic Vector type, with a length that is symbolically known at compile time, can be declared as:

data Vect<A : Type> : (n : Nat) -> Type
| cons : (n : Nat, x : A, xs : Vect(n)) -> Vect(Nat.succ(n))
| nil  : Vect(Nat.zero)

When pattern-matching on those, we can specify a return type that depends on indices:

let tail(A : Type, n : Nat, vect : Vect<A>(Nat.succ(n))) =>
    case vect        -> (n) => Vect<A>(pred(n))
    | cons(n, x, xs) => xs
    | nil            => Vect<A>.nil

This allows us to write powerful type-safe functions, such as an indexing function over vectors that can't overflow. We can also use the self keyword to refer to the matched structure itself, allowing us to express mathematical induction (see examples).

Those features allow Formality to express theorems as types. For example, mathematical equality can be defined as:

data Eq<A : Type> : (x : A, y : A) -> Type
| refl : (x : A) -> Eq(x, x)

And the proof that a == b implies b == a is just:

let sym(A : Type, a : A, b : A, e : Eq<A>(a, b)) =>
    case e    -> (a, b) => Eq<A>(b, a)
    | refl(x) => Eq<A>.refl(x)

With that much expressivity, Formality types can be seen as a "language of specifications". We can, for example, write "the type of sorted lists", "the type of prime numbers >10", or even "the type of smart contracts that can't be drained".

The following Formality program:

id(1000000000(List<Bool>, map(Bool, Bool, not), list))