4. Core Features

4.1. Let

Formality includes let expressions, which allow you to give local names to terms.

import Base@0

main : Output
  let hello = "Hello, world!"
  print(hello)

let expressions can be infinitely nested.

import Base@0

main : Output
  let output =
    let hello = "Hello, world!"
    print(hello)
  output

Note that let has no computational effect. It simply performs a parse-time substitution.

4.2. Words

Formality includes native, unsigned, 32-bit numbers, and many numeric operations:

name syntax haskell equivalent
addition x + y (x + y) >>> 0
subtraction x - y (x - y) >>> 0
multiplication x * y (x * y) >>> 0
division x / y (x / y) >>> 0
modulus x % y (x % y) >>> 0
exponentiation x ^ y (x ** y) >>> 0
bitwise-and x .& y x & y
bitwise-or x .| y x | y
bitwise-xor x .^ y x ^ y
bitwise-not .!(y) ~y
bitwise-right-shift x .>> y x >>> y
bitwise-left-shift x .<< y x << y
greater-than x .> y x > y ? 1 : 0
less-than x .< y x < y ? 1 : 0
equals x .= y x === y ? 1 : 0
float-addition x +f y x + y
float-subtraction x -f y x - y
float-multiplication x *f y x * y
float-division x /f y x / y
float-modulus x %f y x % y
float-exponentiation x ^f y x ** y
uint-to-float .f(y) -
float-to-uint .u(y) -

The type of a native number is Word. A number literal can be written in decimal:

main : Word
  1900

Or in hexadecimal:

main : Word
  0x76C

Or in binary:

main : Word
  0b11101101100

Operators work as expected, except there is no precedence: parenthesis are always placed on the right. An expression like 3 * 10 + 1, for example, is always parsed as 3 * (10 + 1). If you want the multiplication to occur first, you must be explicit:

main : Word
  (3 * 10) + 1

4.3. If / Else

if allows branching with a Word condition.

syntax description
if n: a else: b If n .= 0, evaluates to b, else, evaluates to a

Usage is straightforward:

import Base@0

main : Output
  let age = 30

  if age .< 18:
    print("boring teenager")
  else:
    print("respect your elders!")

4.4. Pairs

Formality includes native pairs.

syntax description
[x : A, B(x)] The type of a pair
[a, b] Creates a pair with elements a and b
fst(p) Extracts the first element of a pair
snd(p) Extracts the second element of a pair
get [a, b] = p ... Extracts both elements of a pair

Note that the type of a pair is [x : A, B(x)], because the type of the second element can depend on the value of the first. When it doesn’t, you can write just [:A, B] instead. Using pairs is straightforward. Examples:

Creating:

main : [:Word, Word]
  [1, 2]

Extracting the first element:

main : Word
  let pair = [1, 2]
  fst(pair)

Extracting both elements:

main : Word
  let pair  = [1, 2]
  get [a,b] = pair
  a + b

Nesting:

import Base@0

main : [:[:Word, Word], String]
  [[1, 2], "Hello Word!"]

Chaining:

main : Word
  let triple  = [1, 2, 3] // same as [1, [2, 3]]
  get [x,y,z] = triple
  x + y + z

Erased (first element):

main : [~x : Word, Word]
  [~1, 2] // the number "1" is erased from runtime

Erased (second element):

main : [x : Word ~ Word]
  [1 ~ 2] // the number "2" is erased from runtime

4.5. Functions

Formality includes primitives for creating and applying functions:

syntax description
{x : A, y : B, z : C, ...} -> D Function type with args x : A, y : B, z : C, returning D
{x, y, z, ...} body A function that receives the arguments x, y, z and returns body
f(x, y, z, ...) Applies the function f to the arguments x, y, z (curried)

Formality functions are anonymous expressions, like Haskell’s lambdas. There are no multi-argument lambdas; {x, y, z, ...} body is the same as {x} {y} {z} ... body, which works like JS’s x => y => z => ... body and Haskell’s \ x y z ... -> body. Function calls use f(x, y, z) syntax, which is the same as f(x)(y)(z).... The type of a function is written as A -> B -> C -> D, like on Haskell, but it can also be written with names, as {x : A, y : B, z : C ...} -> D, which is equivalent to Agda’s (x : A) -> (y : B) -> (z : C) -> ... D. Examples:

A top-level function:

adder : Word -> Word -> Word
  {x, y} x + y

main : Word
  adder(40, 2)

When you write the variable names, lambdas are added implicity. For example:

adder : {x : Word, y : Word} -> Word
  x + y

main : Word
  adder(40, 2)

An inline function (lambda expression):

main : Word
  ({x : Word, y : Word} x + y)(40, 2)

You can annotate the full type rather than the type of each variable:

main : Word
  (({x, y} x + y) :: Word -> Word -> Word)(40, 2)

You can avoid types. This won’t type-check, but can still be ran:

main
  ({x, y} x + y)(40, 2)

Lambdas and applications can be erased with a ~, which causes them to vanish from the compiled output. This is useful, for example, to write polymorphic functions without extra runtime costs. For example, on the code below, id is compiled to {x} x, and main is compiled to id(42). The first argument disappears from the runtime.

id : {~T : Type, x : T} -> T
  x

main : Word
  id(~Word, 42)

Formality functions are affine, which means you can’t use a variable more than once. For example, the program below isn’t allowed, because b is used twice:

copy : {b : Bool} -> [:Bool, Bool]
  [b, b]

While this sounds limiting, there are many ways to deal with it, as will be explained later, and it is extremelly important for both logical consistency and runtime performance.

4.6. Boxes and Copying

Formality includes primives for performing explicit, deep copies of terms, as long as they’re “boxed”.

syntax description
#t Puts term t inside a box
!T The type of a boxed term
dup x = t; u Unboxes t and copies it as x inside u

Since this increases the power of the language considerably, in order not to cause logical inconsistencies, and to still allow for an efficient runtime, boxes are limited by the “stratification condition”. It enforces that the number of #s surrounding a term must never change during reduction. As such, boxes aren’t very useful for copying data, but are essential to implement control structures like loops and recursion. This all will be explained in more details later on.

4.7. Equality

Formality includes untyped equality primitives, the same one seen in Cedille.

syntax description
a == b A type asserting that a is equal to b
refl(~x) A proof that x == x
sym(~e) Given e : a == b, proves b == a
cong(~f, ~e) For any f, given e : a == b, proves f(a) == f(b)
t :: rewrite x in P(x) with e Given e : a == b and t : P(a), proves P(b)

Here, a == b is a type specifying that a is equal to b. It is not a proof, it is merely “a question”. To prove it, you must construct a term x of type a == b. The only way to do it directly is with refl(~t), which proves that a term is equal to itself. That is, for any t, proves t == t. So, for example:

main : 1 == 1
  refl(~1)

That means refl(~1) is a proof that 1 == 1. As you can see, we can have values inside types: that’s perfectly normal in Formality.

Equalities are useful to, among other things, restrict the domain of a function. For example:

mul_small : {x : Word, y : Word, ~e : (x + y) == 10} -> Word
  x * y

main : Word
  mul_small(3, 7, ~refl(~10))

This “small multiplication” function can only be called if its first two arguments add to 10. This is enforced by the presence of the third argument, e, which is erased (due to the ~). In other words, differently than a classic “assert”, this restriction is checked statically and has no runtime costs. As an exercise, try changing the arguments of mul_small on the program above and see what happens.

Equality can be used and manipuled with 3 primitives. The sym primitive just flips the sides of an equality. The cong primitive just appends a function to both sides. The rewrite primitive allows us to substitute equal terms in arbitrary types. It consists of a term to be casted (t), a variable (x), a template (P(x)) and an equality proof (e), and performs the following operation:

// Step 1: assert that `e`'s type is an equality.
// Step 2: replace the template's variable by the left-side of the equality.
// Step 3: assert that the type of `a` matches the type above.
// Step 4: replace the template's variable by the right-side of the equality.
// Step 5: cast `t` to the type above.

For example, suppose that we had a function that received a x : Word and a y : Word that added to 9, and we wanted to call small_mul with them. We could try this:

main : {x : Word, y : Word, ~e : (x + y) == 9} -> Word
  mul_small(x + y, 1, ~e)

But we’d have the following error:

Type mismatch.
- Found type... x + y == 9
- Instead of... (x + y) + 1 == 10

That’s because e is a proof that x + y == 9, not that (x + y) + 1 == 10. But since 9 is smaller than 10, we should be able to call mul_small on x + y. With rewrite, we can do that as follows:

main : {x : Word, y : Word, ~xy_is_9 : (x + y) == 9} -> Word
  // The term to be casted.
  let t = refl(~10)

  // The rewrite equality.
  let e = sym(~xy_is_9)

  // Step 1: asserted `e`'s type is an equality (`9 == x + y`).
  // Step 2: replacing `k` on the template by `9`, we get `(9 + 1) == 10`.
  // Step 3: asserted that `t : 10 == 10` matches the type above (by reduction).
  // Step 4: replacing `k` on the template by `x + y`, we get `((x + y) + 1) == 10`.
  // Step 5: `t` is casted to the type above.
  let t = t :: rewrite k in (k + 1) == 10 with e

  // Since `T : ((x + y) + 1) == 10`, we can call `mul_small` with `(x + y)` and `1`.
  mul_small(x + y, 1, ~t)

In short, it allowed us to replace 9 by x + y on t : (9 + 1) == 10 by exploiting the e : 9 == x + y argument. Note that, here, t is an equality too, but that’s not mandatory; it could have been any type that had a 9 inside it.

4.8. Self Types

Formality also has Self Types, which allow it us to implement inductive datatypes with λ-encodings:

syntax description
$self T(self) T is a type that can access its own value
new(~T) t Constructs an instance of a T with value t
(%t) Consumes a self-type t, giving its type access to its value

This primitive is explained in more details on the paper linked above. While Self Types are extremelly useful and powerful, they should be considered an advanced feature that most users won’t need to use directly. Formality includes a large set of syntax-sugars that allow users to define and use datatypes with a familiar notation, similar to other traditional functional languages.

4.9. Annotations

You can also explictly annotate the type of a term:

syntax description
term :: Type Annotates term with type Type

This is useful when the bidirectional type-checker can’t infer the type of an expression.

main : Word
  (({x, y} x + y) :: Word -> Word -> Word)(40, 2)

4.10. Holes

Formality also features holes, which are very useful for development and debugging. A hole can be used to fill a part of your program that you don’t want to implement yet. It can be written anywhere as ?name, with the name being optional. This will cause Formality to print the type expected on the hole location, as well as its context (scope variables). For example, the program below:

import Base@0

main : {x : Bool} -> Bool
  and(true, ?)

Will output:

[ERROR]
Hole found.
- With goal... Bool
- Inside of... and(true, ?help)
- With context:
- x : Bool

This tells you that, on the location of the hole, you should have a Bool.

The point of holes is that Formality will assume them to be true, allowing you to move on to other parts of your program before returning. Note that this is only automatic if Formality can infer the expected type of the hole’s location. Otherwise, you must give it an explicit annotation, as in ?hole :: MyType.

4.11. Logs

Another handy feature is log(x). When running a program, it will print the normal form of x, similarly to haskell’s console.log and haskell’s print, but for anything (not only strings). When type-checking a program, it tells you the normal-form and the type of x. This is useful when you want to know what type an expression would have inside certain context. For example:

import Base@0

main : {f : Bool -> Nat} -> Nat
  log(f(true))
  ?

Type-checking the program above will cause Formality to output:

[LOG]
Term: f(true)
Type: Nat

[ERROR]
Hole found.
- With goal... Nat
- Inside of... {f} => ?
- With context:
- f : {:Bool} -> Nat

This tells you that, inside the body of main, the type of f(true) is Nat. Since it coincides with the type of the hole, you can complete the program above with it:

import Base@0

main : {f : Bool -> Nat} -> Nat
  f(true)

4.12. Local imports

The import statement can be used to include local files. For example, save an Answers.fm file in the same directory as hello.fm, with the following contents:

import Base@0

everything : String
  "42"

Then save a test.fm file as:

import Base@0
import Answers

main : Output
  print(everything)

And run it with fm test/main. You should see 42.

If multiple imports have conflicting names, you can disambiguate with File/name, or with a qualified import, using as:

import Base@0
import Answers as A

main : Output
  print(A/everything)

4.13. Global imports

Formality also has a file-based package manager. You can use it to share files with other people. A file can be saved globally with fm -s file. This will give it a unique name with a version, such as file@7. Once given a unique name, the file contents will never change, so file@7 will always refer to that exact file. As soon as it is saved globally, you can import it from any other computer. For example, remove Answers.fm and change hello.fm to:

import Base@0
import Answers@0

main : Output
  print(everything)

This will load Answers@0.fm inside the fm_modules directory and load it. Any import ending with @N refers to a unique, immutable, permanent global file. That prevents the infamous “depencency hell”, and is useful for many applications.

Right now, global imports are uploaded to our servers, but, in a future, they’ll upload files to a decentralized storage such as IPFS/Swarm, and give it a unique name using Ethereum’s naming system.