8.7. Special Types🔗

Understanding the representation of data in memory is very important. Usually, the representation can be understood from the definition of a datatype. Each constructor corresponds to an object in memory that has a header that includes a tag and a reference count. The constructor's arguments are each represented by a pointer to some other object. In other words, List really is a linked list and extracting a field from a structure really does just chase a pointer.

There are, however, some important exceptions to this rule. A number of types are treated specially by the compiler. For example, the type UInt32 is defined as Fin (2 ^ 32), but it is replaced at run-time with an actual native implementation based on machine words. Similarly, even though the definition of Nat suggests an implementation similar to List Unit, the actual run-time representation uses immediate machine words for sufficiently-small numbers and an efficient arbitrary-precision arithmetic library for larger numbers. The Lean compiler translates from definitions that use pattern matching into the appropriate operations for this representation, and calls to operations like addition and subtraction are mapped to fast operations from the underlying arithmetic library. After all, addition should not take time linear in the size of the addends.

The fact that some types have special representations also means that care is needed when working with them. Most of these types consist of a structure that is treated specially by the compiler. With these structures, using the constructor or the field accessors directly can trigger expensive conversions between efficient representations and representations designed for use in proofs.

For example, arrays are defined as structures that wrap linked lists. In compiled code, they are represented as efficient dynamic arrays, and applying the constructor Array.mk to a list converts the list to such an efficient array, which takes linear time. The field accessor toList converts the array back to a linked list, which also takes linear time. This definition of Array exists entirely to make it easier to prove things about arrays, and these conversions should be avoided in code that is intended to be run. Similarly, String is defined as a structure that contains an array of bytes together with a proof that the bytes are valid UTF-8, but the run-time representation additionally includes a field that caches the number of characters in the string. Applying the constructor to a byte array can only be done when the byte array is valid, so there's no need to check that the bytes are in fact a UTF-8 sequence, but the character count is computed in linear time. The accessor toByteArray allocates a new byte array object and copies the underlying bytes, taking linear time and space. Many of the basic operations on strings are replaced by the compiler with efficient versions that mutate the run-time version of the string when possible instead of allocating a new one.

Both types themselves and proofs of propositions are completely erased from compiled code. In other words, they take up no space, and any computations that might have been performed as part of a proof are similarly erased. This means that proofs can take advantage of the convenient interface to arrays as inductively-defined lists, including using induction to prove things about them, without imposing slow conversion steps while the program is running. For these built-in types, a convenient logical representation of the data does not imply that the program must be slow.

If a structure type has only a single non-type non-proof field, then the constructor itself disappears at run time, being replaced with its single argument. In other words, a subtype is represented identically to its underlying type, rather than with an extra layer of indirection. Similarly, Fin is just Nat in memory, and single-field structures can be created to keep track of different uses of Nats or Strings without paying a performance penalty. If a constructor has no non-type non-proof arguments, then the constructor also disappears and is replaced with a constant value where the pointer would otherwise be used. This means that true, false, and none are constant values, rather than pointers to heap-allocated objects.

The following types have special representations: