Typed holes

You can use a question mark (?) anywhere an expression would be expected, and the type checker will tell you what the type of the missing expression needs to be. For example, if you type-check the following code:

let mass = 1 kg
let f: Force = mass * ?

Run this example

The type checker will produce an error message indicating that there is a typed hole, and it will tell you that an expression of type Acceleration is expected at that position (Newton's second law):

error: Found typed hole
  ┌─ <input:2>:3:23
  │
3 │ let f: Force = mass * ?
  │                       ^ Acceleration
  │
  = Found a hole of type 'Acceleration' in the statement:
  =   let f: Force = mass × ?

Dimensional analysis with typed holes

As we saw above, this can be useful if you write mathematical expressions and need to figure out what part you are missing.

As another example, say you want to compute the potential energy of a charge q at a distance r from another charge Q. You might remember that Coulomb's law involves the product of the two charges divided by the distance, but you might have forgotten the proportionality constant. You can write:

let q = electron_charge
let Q = 2 electron_charge
let r = 1 a0  # Bohr radius

q Q / (? r) -> eV

Run this example

If you run the type checker on this code, it will tell you what type is expected at the position of the question mark. If possible, it will also suggest available bindings that match the expected type. In this case, we can see that an electric permittivity is expected, and the type checker suggests the globally available constant ε0 (and its aliases) as a possible match:

error: Found typed hole
  ┌─ <input:8>:5:8
  │
5 │ q Q / (? r) -> eV
  │        ^ ElectricPermittivity
  │
  = Found a hole of type 'ElectricPermittivity' in the statement:
  =   q × Q / (? × r) ➞ electronvolt
  = Relevant matches for this hole include:
  =   eps0, ε0, electric_constant

Arbitrary types

Using typed holes is not limited to physical quantities. You can use them to infer arbitrary types in any expression:

fn seq(n) = if n == 1 then [1] else cons_end(n, ?)

Run this example

error: Found typed hole
  ┌─ <input:2>:1:49
  │
1 │ fn seq(n) = if n == 1 then [1] else cons_end(n, ?)
  │                                                 ^ List<Scalar>
  │
  = Found a hole of type 'List<Scalar>' in the statement:
  =   fn seq(n: Scalar) -> List<Scalar> = if (n == 1) then [1] else cons_end(n, ?)

You can even use them to infer function types:

fn transform(xs: List<Scalar>) -> List<String> = map(?, xs)

Run this example

error: Found typed hole
  ┌─ <input:2>:1:54
  │
1 │ fn transform(xs: List<Scalar>) -> List<String> = map(?, xs)
  │                                                      ^ Fn[(Scalar) -> String]
  │
  = Found a hole of type 'Fn[(Scalar) -> String]' in the statement:
  =   fn transform(xs: List<Scalar>) -> List<String> = map(?, xs)