type-annotations.org

Type annotations

In Elisp users are not required to provide type annotations to their code. While at many places the types can be inferred there are places, especially in user-defined functions, where we can not infer the correct type.

Therefore Elsa provides users with the option to annotate forms in their code to add additional type information.

def* declarations (defun, defvar, …)

For function definitions, the annotations are placed in front of the body of the function inside a special comment form:

;; (add-one :: (function (int) int))
(defun add-one (x)
  (1+ x))

The type annotation form starts with the function name followed by two colons :: and the type. The same annotation is used for functions (currently defun) and variables defvar, defcustom, defconst.

The name in the annotation must match the name of the following form. This is checked to prevent accidental copy-paste errors when the comment form is forgotten or misplaced.

Local scope variable

To annotate a local scope variable, place the annotation form after the point where the variable was defined and before the place where the variable is used. This will probably change in later versions so that it is also possible to annotate variables at the place of definition.

(lambda (index arg)
  ;; (var arg :: (struct elsa-form))
  (progn
    ;; arg here is now of type elsa-form
    (oref arg start)))

Elsa type system

Here are general guidelines on how the types are constructed.

Built-in types

For built-in types with test predicates, drop the p or -p suffix to get the type:

• stringp → string
• integerp → integer (int is also accepted)
• markerp → marker
• hash-table-p → hash-table

Some additional special types:

• t stands for t and is always true
• nil stands for nil and is always false
• bool is a combination of explicitly t or nil

Nullable types

By default types do not accept nil values. This helps preventing errors where you would pass nil to a function expecting a value. To mark a type nullable you can combine it with nil type using the or combinator: (or string nil) is a type which takes any string but also nil.

Implicitly castable type

Type of anything is called mixed.

Mixed is a special type in a way that it serves as an opt-out from type analysis.

Mixed accepts any other type except unbound. This is type-theoretically sound because mixed is the union of all types.

However, mixed is also accepted by any other type. This is unsafe and works as an implicit type-casting.

Typically, if some function returns mixed, such as reading a property from a symbol with get, we can wrap this call in a function and provide a more narrow type signature for the return type provided we know that the property is always of a certain type.

;; (set-property :: (function (symbol int) int))
(defun set-property (name value)
  (set name value))

;; (get-property :: (function (symbol) int))
(defun get-property (name)
  ;; Even though `get' returns mixed, we know that if we only set it
  ;; with `set-property' it will always be int and so we can provide
  ;; more specific return type.
  (get name value))

It is recommended to always provide type signatures for top-level functions instead of implicit mixed.

Most general type [not implemented yet]

A type for everything is called unknown. It accepts anything and is always nullable (that means it accepts nil). This is the default type for when we lack type information.

Because an unknown type can be anything it itself is only accepted by unknown (and mixed), so that the following would not type-check:

;; (a-goes-in :: (function (unknown) number))
(defun a-goes-in (a)
  ;; a *might* be an number, but we don't know for sure
  (1+ a))

This is useful for APIs and cases where we want to signal “this can be any value, so you must perform some type of checking before you use it”. This forces users to safely introspect returned values.

;; (a-goes-in :: (function (unknown) number))
(defun a-goes-in (a)
  (if (numberp a) ;; type guard makes sure a is a number
      (1+ a)
    (error "A is not a number")))

The difference between unknown and mixed is that mixed is acepted by any type by implicitly casting it to the required type. It is an opt-out from type-safety.

Composite (higher order) types

Composite or higher-order types are types which take other types as arguments.

Composite types usually correspond to data constructors such as cons, list, vector…

• (cons a b) where a is the type of car and b is the type of cdr. If the car and cdr can be anything write (cons mixed mixed) or simply cons for short.
• (list a) where a is the type of items in the list. If the list can hold anything, write (list mixed) or simply list for short.
• (vector a) where a is the type of items in the vector. If the vector can hold anything, write (vector mixed) or simply vector for short.
• (hash-table k v) where k is the key type and v is the value type. If the hash table can hold anything, write (hash-table mixed mixed) or simply hash-table for short.

Tuple

Tuple is a list of fixed length. Unlike (list a), a tuple can have a different type for each position. This is sometimes useful for “poor man’s data types”, such as (list "firstname" "secondname" 45), for first and second name and age.

The tuple type is created by simply enclosing the types in parentheses, so the tuple from the example has type (string string int).

Constant types

A constant type always holds a specific value. Functions often take flags which can be symbols such as 'append or 'prepend or constant strings.

To specify a constant type wrap the value in a (const) constructor, so that:

• (const a) is the symbol a (when used in a lisp program you would pass it around as 'a),
• (const 1) is the integer 1,
• (const "foo") is the string "foo".

Because constant types are pretty common, we provide a short-hand syntax, where any “atom” simply stands for itself, so that:

• In any type context, "foo" is the same as (const "foo").
• In any type context, 1 is the same as (const 1).
• In any type context, 'sym is the same as (const sym). Notice that the quote is missing inside const, similar to how it is not repeated inside quote, such as (quote sym).

Function types

Function types are types of functions. They have input argument types and a return type.

The function add-one from the introduction has a function type (function (int) int) which means it takes in one integer and returns an integer.

A lambda form (lambda (x) (number-to-string x)) has function type (function (number) string), it takes in a number and returns a string.

A function can have a function type as one of its input types. An example of such a function is mapcar which takes a function and a list and applies the function to every item of the list.

;; (app :: (function ((function (number) number)) (list number)))
(defun app (fn)
  "Apply FN to the list (1 2 3 4)"
  (mapcar fn (list 1 2 3 4)))

(app (lambda (x) (* x x)))

The app function requires that we pass in a function which processes a number into a number and returns a list of numbers.

Sometimes, functions can have multiple signatures based. For example, a function can return a number if a number is passed in, or it can return a string if a string is passed in. The different variants are called overloads.

(my-fn 1) ;; => evaluates to 2
(my-fn "1") ;; => evaluates to "2"

To capture the overloads, we construct an intersection type:

(my-fn :: (and (function (int) int) (function (string) string)))

When we pass an int into this function, Elsa can use match the input arguments against the different overloads and determine the return type.

Note that the type is constructed with and and not or. Here, the function really is both types at the same time, not one or the other.

Generic types [not implemented yet]

Generic types are types where some of the type arguments are variable. Both basic and composite types can be turned into generic types.

Motivation

An example of a generic function is identity. This function takes anything in and anything out. We could therefore give it a type annotation (elsa (mixed) mixed).

However, we can do better! We know that whatever was passed in will be returned and so the type actually must be the same. The (elsa (mixed) mixed) signature allows us to pass in an int and it can return back a string no problem and so it would not catch a huge number of possible errors.

What we want to express here is “X comes in, X comes out”.

Syntax

The syntax for generic types is “generic type name” + * suffix. Any string can be used for the generic type name, but customarily single-letter names are used.

For the above mentioned identity function we therefore write the type as (elsa (a*) a*) where a* stands for a generic type a.

A function such as car can be typed as follows:

(elsa ((cons a* b*)) a*)

It takes a cons with a in the car and b in the cdr and return the car which is of type a , whatever that happens to be.

Optional types

If a function can take optional arguments we need to convert them into a nullable type (or type nil).

;; (drop-items :: (function ((list a*) (or int nil)) (list a*)))
(defun drop-items (list &optional n)
  "Drop first item of LIST or N items if N is provided."
  (setq n (or n 1))
  (dotimes (_ n list)
    (setq list (cdr list))))

Variadic types

If a function can take arbitrary number of arguments we preceed the last variadic argument with &rest marker just as we do in the argument list.

;; (join :: (function (string &rest string) string))
(defun join (separator &rest strings)
  "Join STRINGS with SEPARATOR."
  (mapconcat 'identity strings separator))

Type combinators

Sum types

Sum types can be specified as a list form starting with or, so (or string int) is a type accepting strings or integers.

A sum type is useful if the function internally checks the passed value and decides what processing to do:

;; (to-number :: (function ((or int string)) int))
(defun to-number (x)
  (cond
   ((numberp x) x)
   ((stringp x) (string-to-number x))))

Intersection types

Intersection types can be specified as list form starting with and, so (and string float) is a type which is at the same time string and float (such a type has empty domain, nothing can be string and float at the same time). Intersection types are used to track impossible assignments.

;; Such a condition can never evaluate to true
(if (and (stringp x) (integerp x))
    "X is both string and int which is impossible, this branch never executes"
  "This branch always executes")

Difference types

Difference types can be specified as list form starting with diff so (diff mixed string) is a type which can be anything except a string.

Difference types are useful in narrowing the possible values of variables after conditional checks.

(if (stringp x)
    "X is definitely string here"
  "X is anything but string here")