Type System

The underlying techniques are not easy to understand, but there are some links:

• bidirectional type checking: https://jaked.org/blog/2021-09-15-Reconstructing-TypeScript-part-1
• type system borrowed here: https://github.com/hkust-taco/mlscript

Some tricks are taken for help reducing the complexity of code:

First, the array literals are identified as tuple type, that each cell of the array has type individually.

Second, the and the type are reused frequently.

• the type is notated as , and the type is a special tuple type .

• the type is imported from mlscript, notated as .

• the type consists of:

  • a positional argument list, in type.
  • a named argument list, in type.
  • an optional rest argument, in type.
  • an optional body, in any type.

  notated as

• the is a without rest and body.

With aboving constructors, we soonly get typst's type checker.

• it checks array or dictionary literals by converting them with a corresponding and .
• it performs the getting element operation by calls a corresponding .
• the closure is converted into a typed lambda, in type.
• the pattern destructing are converted to array and dictionary constrains.