Types

Types classify programs based on the values that they can compute. Types serve a number of roles in a program:

  1. They allow the compiler to make decisions about the in-memory representation of a value.

  2. They help programmers to communicate their intent to others, serving as a lightweight specification for the inputs and outputs of a function that the compiler can ensure the program adheres to.

  3. They prevent various potential mistakes, such as adding a number to a string, and thus reduce the number of tests that are necessary for a program.

  4. They help the Lean compiler automate the production of auxiliary code that can save boilerplate.

Lean's type system is unusually expressive. Types can encode strong specifications like "this sorting function returns a permutation of its input" and flexible specifications like "this function has different return types, depending on the value of its argument". The type system can even be used as a full-blown logic for proving mathematical theorems. This cutting-edge expressive power doesn't obviate the need for simpler types, however, and understanding these simpler types is a prerequisite for using the more advanced features.

Every program in Lean must have a type. In particular, every expression must have a type before it can be evaluated. In the examples so far, Lean has been able to discover a type on its own, but it is sometimes necessary to provide one. This is done using the colon operator:

#eval (1 + 2 : Nat)

Here, Nat is the type of natural numbers, which are arbitrary-precision unsigned integers. In Lean, Nat is the default type for non-negative integer literals. This default type is not always the best choice. In C, unsigned integers underflow to the largest representable numbers when subtraction would otherwise yield a result less than zero. Nat, however, can represent arbitrarily-large unsigned numbers, so there is no largest number to underflow to. Thus, subtraction on Nat returns 0 when the answer would have otherwise been negative. For instance,

#eval 1 - 2

evaluates to 0 rather than -1. To use a type that can represent the negative integers, provide it directly:

#eval (1 - 2 : Int)

With this type, the result is -1, as expected.

To check the type of an expression without evaluating it, use #check instead of #eval. For instance:

#check (1 - 2 : Int)

reports 1 - 2 : Int without actually performing the subtraction.

When a program can't be given a type, an error is returned from both #check and #eval. For instance:

#check String.append "hello" [" ", "world"]

outputs

application type mismatch
  String.append "hello" [" ", "world"]
argument
  [" ", "world"]
has type
  List String : Type
but is expected to have type
  String : Type

because the second argument to String.append is expected to be a string, but a list of strings was provided instead.