Types

This page documents the Husk type system.

Atomic types

The following Husk types are called atomic:

• Numbers; type TNum.
• Characters; type TChar.

A number can be either an arbitrary-precision rational number, a floating point number, positive or negative infinity, or the special value Any (which is the result of 0/0 and other indeterminate forms, and is deemed equal to any finite number). These classes of numbers are distinguished at runtime, but not at the type level. As a convention, integers are used as truth values in built-in functions.

Compound types

In addition to atomic types, Husk has the following compound types:

• Lists of values of some type; type TList a, shortened to [a].
• Pairs of values of some, possibly different, types; type TPair a b, shortened to (a, b).
• Functions from values of type a to values of type b; type TFunc a b, shortened to a -> b.

A Husk list is homogeneous, which means it can only contain values of one type. A list of numbers is a list of numbers, and you cannot append a character to it. This applies to empty lists too: if the type of an empty list has been inferred as [TNum], it is a list of numbers.

A function of two or more arguments has type a -> (b -> c), and is curried (partially applied) automatically: it is really a one-argument function that takes a value of type a, and produces a function of type b -> c. A function of type a -> b can be applied to a value of type a to produce a value of type b. Type variables are lowercase letters, which can be substituted with any type. For example, the list reversal function rev has type [a] -> [a], meaning that it takes a list of values of some type a, and produces a list of the same type.

Type classes

Husk has the following typeclasses:

• The class of concrete types, Concrete. Atomic types are concrete, and lists and pairs of concrete types are concrete.
• The class of vectorizable types, Vect. The constraint Vect a b x y means that x is a nested list of as and y is a nested list of bs of the same nesting depth.
• The class of bi-vectorizable types, Vect2. The constraint Vect a b c x y z means that x is a nested list of as, y is a nested list of bs and z is a nested list of cs, and the nesting depth of z equals the maximum of that of x and y. It also requires that a and b are not list types.

Some built-in functions have typeclass-constrained types. For example, the equality-testing function eq has type (Concrete x) => x -> x -> TNum. This means that for any type x in the class Concrete, the function eq can have type x -> x -> TNum. For example, you can call eq on two lists of numbers, since [TNum] is a concrete type, but not on two lists of functions, or a character and a number.

Vectorization is performed with the built-in function vec, which has type Vect a b x y => (a -> b) -> (x -> y). You should think of vec as a composition of an indeterminate number of maps: it takes a function from a to b and maps it zero or more layers deep in a nested list. The nesting depth is not necessarily determined by the function. For example, take the length function len, which has type [a] -> TNum. Then vec len has type Vect [a] TNum x y => x -> y. Given a nested list of type [[[TNum]]], the result can be of type TNum, [TNum] or [[TNum]], depending on which nesting level the length function is mapped over. The type inference engine will choose an interpretation that fits together with the rest of the program, if possible.

Binary vectorization is done with the function vec2, which has type Vect2 a b c x y z => (a -> b -> c) -> x -> y -> z and is a bit more complex than vec. It takes a binary function f of type a -> b -> c and returns a new binary function that distributes f over nested lists of as and bs. As an example, consider vect add, where add is the numeric addition function of type TNum -> TNum -> TNum. Given two matrices of type [[TNum]], vec2 add adds them element-wise. Given a matrix and a vector of type [TNum], it adds the vector to every row of the matrix element-wise. Given a matrix and a numbet of type TNum, it adds the number to each element of the matrix. In general, if one argument is nested less deeply than the other, it is distributed over it; if they have the same nesting depth, they are zipped together. For now, vec2 can only be used on functions that don't take lists as arguments, as it simplifies type inference greatly.

Nondeterministic types

Many built-in commands in Husk have several implementations, each with a different type. We call this nondeterministic typing. For example, the command : has the implementation cons of type a -> [a] -> [a], which prepends a value to the beginning of a list, and snoc of type [a] -> a -> [a], which appends a value to the end of a list. During compile time, both of these are tried for each occurrence of : in the source file. The first value that results in a well-typed program (taking into account the types of inputs to the whole program) is chosen as the "true value" of a particular occurrence.