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 ```

Examples

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.

Simple types

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

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

And the negation function as:

haskell 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.

Recursive types

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

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

And a function that doubles it can be written as:

haskell 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.

Polymorphic types

Types can be easily parameterized:

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

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

haskell 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.

Dependent types

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:

haskell 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:

haskell 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).

Theorem Proving

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

haskell 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:

haskell 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".

Optimal Evaluation

The following Formality program:

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