Function types

Function types represent functions that take inputs and yield outputs. The type of functions that take inputs of type A and yield outputs of type B is written A -> B (or A → B).

Every function in Disco takes exactly one input and produces exactly one output. “Multi-argument” functions can be represented using a pair type as the input type. For example, the type of a function taking two natural numbers as input and producing a rational number as output could be written N × N → Q.

Note that if A and B are types, then A -> B is itself a type, which can be used in all the same ways as any other type. In other words, functions in Disco are “first-class”, which means they can be used in the same ways as any other values: for example, functions can be given as input to other functions, or returned as output, we can have lists of functions, etc.

Function values cannot be compared, however, because in general this would require testing the functions on every single possible input, of which there might be infinitely many.