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

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

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

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

main : Number
```

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))]

```

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)]

[0, 0, refl(~Number, ~%0)]

[1, 1, refl(~Number, ~%1)]

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

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

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

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