Core Features

Let

Allows 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: let has no computational effect, it simply performs a parse-time substitution.

Numbers

The type of a native number is Number.

main : Number
  1900

They can also be written in hexadecimal:

main : Number
  0x76C

And in binary:

main : Number
  0b11101101100

They include many built-in operations:

name syntax javascript equivalent
addition x .+. y x + y
subtraction x .-. y x - y
multiplication x .*. y x * y
division x ./. y x / y
modulus x .%. y x % y
exponentiation x .**. y x ** y
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

There is no operator precedence: parenthesis are always placed on the right. That means 3 * 10 + 1 is parsed as 3 * (10 + 1). If you want the multiplication to occur first, you must be explicit:

main : Number
  (3 .*. 10) .+. 1

If / Else

if allows branching with a Number 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!")

Pairs

Native pairs store two elements of possibly different types.

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 : [:Number, Number]
  [1, 2]

Extracting the first element:

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

Extracting both elements:

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

Nesting to the left:

import [email protected]

main : [:[:Number, Number], String]
  [[1, 2], "Hello World!"]

Nesting to the right:

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

Erased (first element):

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

Erased (second element):

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

Notably, the second element of a pair can depend on the value of the first.

main : [x : Number, (if x: Number else: Bool)]
  [0, true] // if you change 0 to 1, the second element must be a Number.

Functions

Formality functions are anonymous expressions, like Haskell’s lambdas. There are no multi-argument lambdas.

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 : Number -> Number -> Number
  {x, y} x .+. y

main : Number
  adder(40, 2)

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

adder : {x : Number, y : Number} -> Number
  x .+. y

main : Number
  adder(40, 2)

An inline function (lambda expression):

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

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

main : Number
  (({x, y} x .+. y) :: Number -> Number -> Number)(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 : Number
  id(~Number, 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.

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
$t Unboxes t

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.

Equality

Formality used to include untyped equality primitives, the same one seen in Cedille. It doesn’t anymore because most of its use cases can be replicated with a user-defined equality type. This will be explained in an advanced tutorial. To learn about the old equality, click here, as it can still be pedagogical.

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

Note that Self Types are not the same as recursive types. Recursive types allow the type to access itself. For example:

N_Nums : {n : Number} -> Type
  if n .<. 2:
    Number
  else:
    [:Number, N_Nums(n .-. 1)]

The type above allows you to create a list of N words:

main : N_Nums(4)
  [0, 1, 2, 3]

Self Types allow a type to access its own value. This has many uses. Suppose that you wanted to create a pair of identical words:

sameNums : Type
  ${self} [:Number, :Number, fst(self) == fst(snd(self))]

same_words_0 : sameNums 
  new(~sameNums) [0, 0, res]

same_words_1 : sameNums 
  new(~sameNums) [1, 1, res]

same_words_2 : sameNums 
  new(~sameNums) [2, 2, refl(~2)]

Notice how the sameNums type has access to values of its terms. So, when we instantiate same_words_0, the self variable on the type is replaced by [0, 0, refl(~0)], which becomes [:Num, :Num, 0 == 0], allowing us to write the last element a refl(~0). Of course, in this case, this effect could be achieved with dependent pairs:

sameNumsB : Type
  [x : Number, y : Number, Equal(Number, %x, %y)]

same_words_b_0 : sameNumsB
  [0, 0, refl(~Number, ~%0)]

same_words_b_1 : sameNumsB
  [1, 1, refl(~Number, ~%1)]

same_words_b_2 : sameNumsB
  [2, 2, refl(~Number, ~%2)

But what is interesting is that Self Types are more expressive than dependent pairs. We could, for example, make an “insanely dependent” pair where the first element depends on the second, and vice-versa:

insane : Type
  ${self}
  [: [a : Number, (a .*. 2) == fst(snd(self))],
     [b : Number, b == fst(fst(self)) .+. 1]]
  
insane : insane
  new(~insane)
  [[1, refl(~2)],
   [2, refl(~2)]]

This define the type of pairs [a,b] such that a .*. 2 = b and b = a .+. 2. Notice the mutual reference. The only possible way to make it is with a = 1 and b = 2, which is the solution to the equation above.

Self Types are used by Formality to create inductive datatypes. This is explained in more details on the tutorial section.

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 : Number
  (({x, y} x .+. y) :: Number -> Number -> Number)(40, 2)

They’re also important for dependent pairs:

annotation0
   [1, 2]

annotation1
   [1, 2] :: [x : Number, (if x: Number else: Bool)]

The pairs above have different types, despite having the same value. Explicit annotations are inline, different from top-level annotations:

annotation2 : [x : Number, (if x: Number else: Bool)]

Non-terminating terms

While Formality’s stratification checks make it a terminating language with a well-defined complexity class, this is relaxed in certain parts of your programs: inside types and unrestricted terms. Those bring first-class non-termination to the language, and can be expressed as:

syntax description
-A A is an unrestricted term of type A
%t Converts t to an unrestricted term
+t Converts t back to a restricted term

In general, prefixing a type with - means that it can either be a well-typed term of that type or non-terminating computation. The %t syntax marks a term as unrestricted, and the +t syntax removes the mark, but it can only be used inside other unrestricted terms, or types. Inside both types and unrestricted terms, you can unbox terms at will, use variables more than once, and even use top-level definitions recursively. So, for example, while the List(Number) type represents a finite list of words, the -List(Number) type can be infinite:

  // A list with infinite copies of the number 1
  ones : -List(Number)
    % cons(~Number, 1, +ones)

And you also use unrestricted terms to write recursive algorithms:

  double : {x : Number} -> -Number
    if x .==. 0:
      % 0
    else:
      % 2 .+. +double(x .-. 1)

The trade-off is that:

  1. Unrestricted terms can’t be compiled to efficient interaction nets.
  2. Unrestricted terms can’t be interpreted as valid mathematical proofs.

The reason for (1) is that, without stratification checks, Formality terms stop being compatible with our efficient, “oracle-free” interaction net runtime. The reason for (2) is that, with unrestricted recursion, it is easy to prove absurd statements. For example, one could prove -Empty by just making a loop:

  main : -Empty
    %+main

But this can’t be taken as a mathematical proof. Note that normal Formality terms (not marked with a -) can be seen as mathematical proofs, even if their types refer to non-terminating terms (ex: double(x) == add(x, x) for recursively defined double and add). That’s because our core language is the Elementary Affine Lambda Calculus, which is not only very restricted computationally, but terminates independent of types.

Unrestricted terms are extremely useful when you have a function argument that will only be used inside a type; for example, the Nat index of a Vector. They also play an important role in the implementation of inductive datatypes with self-types.

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. If you give it a name, it will cause Formality to print the type expected on the hole location, its context (scope variables), and possibly a value, if Formality can fill it for you. For example, the program below:

import Base@0

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

Will output:

[ERROR]
Found hole: 'a'.
- With goal... Bool
- Couldn't solve it.
- With context:
- x : Bool

This tells you that, on the location of the hole, you should have a Bool. In some cases, Formality will be able to find a well-typed term that could be used to fill this hole. For example, on the code above:

main : List(Number)
  cons(~?a, 2, nil(~Number))

Formality outputs:

Found hole: 'a'.
- With goal... Type
- Solved as... Number

Since Formality can infer that the value of ?a should be Number. You can proceed to fill it, or just remove the name, leaving only a ?: this will cause the program to type-check, since Formality knows how to complete it. As a shorthand, you can use _ instead of ~?:

main : List(Number)
  cons(_2, nil(_))

Even when Formality can’t fill a hole, it will locally assume it to be true, allowing you to move on to other parts of your program before returning, making them very useful for development. 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. Of course, unfilled holes cause the top-level term to fail to type-check.

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))
  ?a

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

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

Found hole: 'a'.
- With goal... Nat
- Couldn't solve it.
- With context:
- f : {:Bool} -> Nat

Unsolved holes.

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)

Compile-time logs are extremelly useful for development. We highly recommend you to use them as much as possible!

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)

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 “dependency hell”, and is useful for many applications.

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