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

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

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

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

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

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

main : Word
```

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

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

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