Types

This section describes informally the structure of types in Unison. See also the section titledUser-defined typesfor detailed information on how to define new data types.

Formally, Unison’s type system is an implementation of the system described by Joshua Dunfield and Neelakantan R. Krishnaswami in their 2013 paperComplete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.

Unison extends that type system with,pattern matching,scoped type variables,ability types(also known asalgebraic effects).See the section onAbilitiesfor details on ability types.

Unison attributes a type to every valid expression. For example:

  • 4 Nat.< 5has typeBoolean
  • 42 Nat.+ 3`has typeNat,
  • "hello"has typeText
  • the list[1, 2, 3]has type[Nat]
  • the function(x -> x)has typeforall a. a -> a

The meanings of these types and more are explained in the sections below.

A full treatise on types is beyond the scope of this document. In short, types help enforce that Unison programs make logical sense. Every expression must be well typed, or Unison will give a compile-time type error. For example:

  • [1, 2, 3]is well typed, since lists require all elements to be of the same type.
  • 42 + "hello"is not well typed, since the type of+disallows adding numbers and text together.
  • printLine "Hello, World!"is well typed in some contexts and not others. It's a type error for instance to use I/O functions where anIOabilityis not provided.

Types are of the following general forms.

Type variables

Type variables areregular identifiersbeginning with a lowercase letter. For examplea,x0,andfooare valid type variables.

Polymorphic types

Auniversally quantifiedor "polymorphic" type has the formforall v1 v2 vn. t,wheretis a type. The typetmay involve the variablesv1throughvn.

The symbol∀is an alias forforall.

A type likeforall x. F xcan be written simply asF x(theforall xis implied) as long asxis free inF x(it is not bound by an outer scope; seeScoped type variablesbelow).

A polymorphic type may beinstantiatedat any given type. For example, the empty list[]has typeforall x. [x].So it's a type-polymorphic value. Its type can be instantiated atInt,for example, which bindsxtoIntresulting in[Int]which is also a valid type for the empty list. In fact, we can say that the empty list[]is a value of type[x]for allchoices of element typee,hence the typeforall x. [x].

Likewise the identity function(x -> x),which simply returns its argument, has a polymorphic typeforall t. t -> t.It has typet -> tfor all choices oft.

Scoped type variables

Type variables introduced by a type signature for a term remain in scope throughout the definition of that term.

For example in the following snippet, the type annotationtemp:xis telling Unison thattemphas the typexwhich is bound in the type signature, sotempandahave the same type.

ex1 : x -> y -> x
ex1 a b =
  temp : x
  temp = a
  a

temp : xrefers to the typexin the outer scope.

To explicitly shadow a type variable in scope, the variable can be reintroduced in the inner scope by a `forall` binder, as follows:

ex2 : x -> y -> x
ex2 a b =
-- doesn’t refer to x in outer scope
id : ∀ x . x -> x
id v = v
temp = id 42
id a

id : ∀ x . x -> x doesn’t refer to x in outer scope

Note that here the type variablexin the type ofidgets instantiated to two different types. FirstFunction.id 42instantiates it toNat,thenid a,instantiates it to the outer scope's typex.

Type constructors

Just as values are built using data constructors, types are built fromtype constructors.Nullary type constructors likeNat,Int,Floatare already types, but other type constructors likeListand->(seebuilt-in type constructors)take type parameters in order to yield types.Listis a unary type constructor, so it takes one type (the type of the list elements), and->is a binary type constructor.List Natis a type andNat -> Intis a type.

Kinds of Types

Types are to values askindsare to type constructors. Unison attributes a kind to every type constructor, which is determined by its number of type parameters and the kinds of those type parameters.

A type must be well kinded, just like an expression must be well typed, and for the same reason. However, there is currently no syntax for kinds and they do not appear in Unison programs (this will certainly change in a future version of Unison).

Unison’s kinds have the following forms:

  • A nullary type constructor or ordinary type has kindType.
  • A type constructor has kindk1 -> k2wherek1andk2are kinds.

For exampleList,a unary type constructor, has kindType -> Typeas it takes a type and yields a type. A binary type constructor like->has kindType -> Type -> Type,as it takes two types (it actually takes a type and yields a partially applied unary type constructor that takes the other type). A type constructor of kind(Type -> Type) -> Typeis ahigher-ordertype constructor (it takes a unary type constructor and yields a type).

Type application

A type constructor is applied to a type or another type constructor, depending on its kind, similarly to how functions are applied to arguments at the term level.C Tapplies the type constructorCto the typeT.Type application associates to the left, so the typeA B Cis the same as the type(A B) C.

Function types

The typeX -> Yis a type for functions that take arguments of typeXand yield results of typeY.Application of the binary type constructor->associates to the right, so the typeX -> Y -> Zis the same as the typeX -> (Y -> Z).

Tuple types

The type(A,B)is a type for binary tuples (pairs) of values, one of typeAand another of typeB.The type(A,B,C)is a triple, and so on.

The type(A)is the same as the typeAand is not considered a tuple.

The nullary tuple type()is the type of the unique value also written()and is pronounced “unit”.

In the standard Unison syntax, tuples ofarity2 and higher are actually of a typeTuple a bfor some typesaandb.For example,(X,Y)is syntactic shorthand for the typeTuple X (Tuple Y ()).

Tuples are either constructed with the syntactic shorthand(a,b)(seetuple literals)or with the built-inTuple.Consdata constructor:(a, b).

Built-in types

Unison provides the following built-in types:

  • Natis the type of 64-bit natural numbers, also known as unsigned integers. They range from 0 to 18,446,744,073,709,551,615.
  • Intis the type of 64-bit signed integers. They range from -9,223,372,036,854,775,808 to +9,223,372,036,854,775,807.
  • Floatis the type ofIEEE 754-1985double-precision floating point numbers.
  • Booleanis the type of Boolean expressions whose value istrueorfalse.
  • Bytesis the type of arbitrary-length 8-bit byte sequences.
  • Textis the type of arbitrary-length strings of Unicode text. They can be introduced with single quotes or triple quotes, for multi-line strings.
  • Charis the type of a single Unicode character.
  • The trivial type()(pronounced “unit”) is the type of the nullary tuple. There is a single data constructor of type()and it’s also writtensuperProgram : Boolean -> Nat superProgram bool = if Boolean.not bool then base.bug (Generic.failure "Fatal Issue Encountered" bool) else 100.

Seeliteralsfor more on how values of some of these types are constructed.

Built-in type constructors

Unison has the following built-in type constructors.

  • (->)is the constructor of function types. A typeX -> Yis the type of functions fromXtoY.
  • Tupleis the constructor of tuple types. Seetuple typesfor details on tuples.
  • Listis the constructor of list types. A typeList Tis the type of arbitrary-length sequences of values of typeT.The type[T]is an alias forList T.
  • abilities.Requestis the constructor of requests for abilities. A typeRequest A Tis the type of values received by ability handlers for the abilityAwhere current continuation requires a value of typeT.

User-defined types

New types can be declared as described in detail in theUser-defined typessection. These include ordinarydata types,unique types,andrecord types.A type declaration introduces a type, a corresponding type constructor, one or more data constructors that (collectively) construct all possible values of the type, and (in the case of record types) accessors for the named arguments of the type's single data constructor.