Types and type annotations

A type expression is the language Zelkova uses to talk about its own values. It appears in three places: to the right of the : in a type annotation, as the argument of a constructor in a type declaration, and inside another type expression.

This chapter specifies that language, and the two declarations that are made of type expressions: the annotation name : Type, and the type declaration that introduces a new type. The neighbouring Declarations chapter covers value and function bindings and infix declarations, and refers here for these two.

The forms of a type expression

There are six, and nothing else is a type:

Parentheses may be written around any type expression and mean grouping only: (Colour) is Colour.

module Example exposing (Colour, red)

type Colour
  = Red

red : (Colour)
red = Red

A list type needs no form of its own: it is written List a, an application like any other, and Lists specifies it with the rest of that construct. A record type — { x : Celsius, y : Celsius } — is a seventh form, specified in Records.

Type names

A type name is an uppercase-initial identifier, optionally qualified by the module it comes from. The case is what makes it a name rather than a variable — that rule and its reasoning are in Lexical structure.

module Example exposing (Celsius, freezing)

type Celsius
  = Celsius

freezing : Celsius
freezing = Celsius

A qualified name is spelled and resolved exactly as it is in an expression: the module's name, or the alias standing in for it, then a ., then the type's own name. See Modules for what an import brings into scope.

module Widget exposing (Size, small)

type Size
  = Small

small : Size
small = Small

module Main exposing (x)

import Widget

x : Widget.Size
x = Widget.small

Type variables

A type variable is a lowercase-initial identifier. It stands for a complete type, and it is universally quantified over the declaration it appears in: a variable in an annotation means the caller chooses, and the declaration must work for every choice.

module Example exposing (constant)

constant : a -> b -> a
constant x y =
  x

Nothing distinguishes one lowercase spelling from another: celsius is a type variable in exactly the way a is, and the length of a name carries no meaning.

module Example exposing (identity)

identity : celsius -> celsius
identity x =
  x

A type variable is never applied. Only a type name may head an application, so m a — a variable standing for a type constructor rather than for a type — is a syntax error:

module Example exposing (Box, lift)

type Box a
  = Box a

lift : m a -> m a
lift x =
  x

Allowing it would mean type variables ranging over type constructors as well as types, which needs a kind system — a commitment the language is not ready for. Type classes carries what that limit costs.

Applying a type to arguments

A type declared with parameters is used by applying it to that many arguments, written after the name and separated by spaces. The number of arguments must equal the number of parameters the type declaration gave it.

module Example exposing (Maybe, nothing)

type Maybe a
  = Just a
  | Nothing

nothing : Maybe a
nothing = Nothing

An argument may be any type expression. Where that expression is itself an application, a function, or a tuple, it is parenthesised — application binds tighter than everything else, so Maybe Maybe Colour would otherwise read as Maybe applied to two arguments.

module Example exposing (Maybe, nested)

type Maybe a
  = Just a
  | Nothing

nested : Maybe (Maybe a)
nested = Nothing

module Example exposing (Box, boxed)

type Box a
  = Box a

boxed : Box (a -> a)
boxed = Box keep

keep : a -> a
keep x = x

Arity is part of the application

module Example exposing (Maybe, bare)

type Maybe a
  = Just a
  | Nothing

bare : Maybe
bare = Nothing

module Example exposing (Maybe, Size, tooMany)

type Maybe a
  = Just a
  | Nothing

type Size
  = Small

tooMany : Maybe Size Size
tooMany = Nothing

The count is checked wherever a type name is applied, and a variant's arguments are no exception — a module's own declarations are in scope for each other, so a sibling named in a variant is held to its own arity:

module Example exposing (Maybe, W)

type Maybe a
  = Just a
  | Nothing

type W a
  = W Maybe a

An applied type still means what it says

Two applications of one type name are the same type exactly when their arguments are.

module Example exposing (Maybe, Size, sized)

type Maybe a
  = Just a
  | Nothing

type Size
  = Small

sized : Maybe Size
sized = Just Small

So Maybe Size and Maybe Other are two types, and one does not stand in for the other. The arguments are what separates them: the head is the same name in both.

module Example exposing (Maybe, Size, Other, mismatched)

type Maybe a
  = Just a
  | Nothing

type Size
  = Small

type Other
  = First

mismatched : Maybe Size
mismatched = Just First

The function arrow

a -> b is the type of a function from a to b. The arrow is right-associative, so a -> b -> c means a -> (b -> c) — a function of one argument returning a function — and a function of several arguments needs no parentheses.

module Example exposing (Size, clamp)

type Size
  = Small

clamp : Size -> Size -> Size
clamp a b =
  a

A function argument is the case that needs parentheses. (a -> b) -> c is a function taking a function; without them it would be a function of two arguments.

module Example exposing (Size, apply)

type Size
  = Small

apply : (Size -> Size) -> Size -> Size
apply f x =
  x

An arrow needs a type on both sides:

module Example exposing (Size, f)

type Size
  = Small

f : Size ->
f = Small

Tuple types

A tuple type is two or three types between parentheses, separated by commas. The elements may be any type expression, including another tuple.

module Example exposing (Size, first, second)

type Size
  = Small

first : (Size, Size) -> Size
first p =
  Small

second : (Size, Size, Size) -> Size
second p =
  Small

Two or three, and nothing else. There is no one-element tuple — (Colour) is grouping, as above — and no tuple of four or more. A four-element tuple is a syntax error rather than a type error found later:

module Example exposing (Size, quad)

type Size
  = Small

quad : (Size, Size, Size, Size) -> Size
quad p =
  Small

A tuple of four is where a record belongs: past three elements, position stops being a usable way to say which field is which.

The same limit applies to tuple patterns and tuple expressions, so no tuple of any other size is representable anywhere in the language.

The unit type

module Example exposing (nothingUseful)

nothingUseful : ()
nothingUseful = ()

() is the type with exactly one value, and that value is also written (). It is what a function returns when it has nothing to say, and what a function takes when it needs nothing meaningful.

Scalar types

Five types are scalar: Int, Float, Char, String and Bool. Each is declared in Zelkova like any other type — Int, Float and Bool in Basics, Char in Char, String in String — and reaches an ordinary module through the default imports.

What separates the five from every other type is that the compiler knows them, and knows each one by the qualified name of its declaration. What it knows is the representation each target gives the type, which is what the first five rows of the admitted-type table hold and what lets a facade signature name one.

A scalar is therefore identified by where it is declared and never by how it is spelled. A module declaring its own Int declares an ordinary type that shares a name, since every declaration introduces a genuinely new type: that Int is not the language's, no annotation mixes the two, and it may not cross a facade boundary as an Int.

module Example exposing (Int, zero)

type Int
  = Zero

zero : Int
zero = Zero

Four of the five are opaque. Nothing in the language builds or inspects an Int, a Float, a Char or a String: their values come from literals and from the functions of the modules declaring them. Such a declaration has no variant to write, so it writes its own name and contributes no constructor — Int is a type and never a value.

module Basics exposing (Int)

type Int = Int

Any other body is an error. The declaration is where a scalar's documentation lives, and a body naming anything but the type itself would describe a representation the language does not have.

module Basics exposing (Int)

type Int = I32

A Char is one Unicode scalar value: a code point from U+0000 to U+10FFFF other than a surrogate, U+D800 to U+DFFF. A String is a sequence of Chars, the empty one included. A surrogate is a value of neither type on any target, whatever units that target's own strings are made of.

Bool is a scalar and an ordinary union. type Bool = True | False in Basics is the whole of its definition, and True and False are constructors built and matched like any others — which is what true and false not being reserved words means. The compiler knows Bool's representation and nothing about its structure, so the self-naming rule above does not reach it. Bool in an annotation is that union:

module Basics exposing (Bool(..), yes)

type Bool = True | False

yes : Bool
yes = True

A module of zelkova-core receives the scalar names without an import. That rule belongs to the default imports, which is also where the case it covers arises — a facade underneath Basics. It supplies the five type names and nothing else, so a module reaching Bool that way can annotate one and cannot write a True.

Not implemented: Char does not compile, so it does not declare the scalar it is named for.

Type annotations

A type annotation gives a declaration a type. It is the declaration's name, a :, and a type expression.

module Example exposing (Size, grow)

type Size
  = Small

grow : Size -> Size
grow s =
  s

An exposed declaration must be annotated

A declaration named in its module's exposing list must carry an annotation. A declaration the module keeps to itself need not: it gets whatever type the checker infers for it.

The rule is drawn at the module boundary because that is where a type stops being the compiler's business and becomes a promise to someone else — the sense of promise the next section is about.

module Example exposing (Size, visible)

type Size
  = Small

visible : Size
visible =
  hidden

hidden =
  Small

visible is exposed and annotated; hidden is neither, and needs no annotation to be used by its neighbour.

Because exposing (..) exposes everything a module declares, a module written that way must annotate every top-level declaration. A module that wants unannotated helpers lists what it exposes.

module Example exposing (count)

type Size
  = Small

count = Small

count is exposed and carries no annotation, so the declaration itself is rejected. Modules shows the same rule from the importer's side: an exposed value that fails this check is left out of its module's interface, so an importer naming it finds nothing to resolve.

An annotation is a promise

An annotation is not a hint and not a starting point for inference. It is what callers rely on, so the declared type may be no more general than what the body can actually support.

f : a -> a promises to return whatever the caller passed in. A body that always returns one particular type cannot honour that, and the declaration is an error — even though there is a type (Size -> Size) that would make the body check.

module Example exposing (Size, f)

type Size
  = Small

f : a -> a
f x =
  Small

An annotation more specific than the body would allow is ordinary and useful: it is how a general function is given a narrower published type.

Where an annotation goes

An annotation is written on the line directly above the declaration it annotates, with nothing between the two — not another declaration, not a comment, not even a blank line — and a declaration carries at most one.

A comment belonging to the declaration goes above the annotation, where it reads as a comment on both.

module Example exposing (Size, first, second)

type Size
  = Small

first : Size

second : Size
second = Small

first = Small

module Example exposing (Size, spaced)

type Size
  = Small

spaced : Size

spaced = Small

module Example exposing (Size, Other, ambiguous)

type Size
  = Small

type Other
  = Other

ambiguous : Size
ambiguous : Other
ambiguous = Small

Known gap: all three blocks should be rejected here, and not one of them is rejected for the rule it breaks. Declarations are grouped by name into a map with their order thrown away, so an annotation may sit anywhere among the top-level declarations — and, position being gone entirely, a blank line between an annotation and its declaration is not noticed either. The first two blocks are accepted outright. The third is rejected, but for the wrong reason: when a name carries two annotations the last silently wins, so ambiguous is checked against Other, the body Small disagrees with it, and what the reader sees is a type mismatch rather than a repeated annotation (docs/tickets/lang-11.md).

A foreign facade is the one place an annotation stands alone: a module foreign module is annotations with no bodies at all.

An annotation may span several lines

An annotation is one declaration, so it may be carried onto following lines as long as they are indented, following Layout rules.

module Example exposing (Size, combine)

type Size
  = Small

combine :
  Size -> Size -> Size
combine a b =
  a

The conventional way to break a long signature is one argument per line, with each continuation line starting with the arrow:

module Example exposing (Size, combine)

type Size
  = Small

combine : Size
  -> Size
  -> Size
combine a b =
  a

The annotation and the declaration's parameters

A function's parameter list and its annotation have to agree. The annotation's arrows, read left to right, are the parameters, and the type after the last arrow is what the body produces. So Size -> Size describes a function of one parameter, and the declaration below it may name at most one — naming fewer leaves the rest of the type for the body to produce, which is Declarations' subject.

Naming more is an error. Here the annotation has one arrow and f a b supplies two parameters:

module Example exposing (Size, f)

type Size
  = Small

f : Size -> Size
f a b =
  a

A tuple or a parenthesised function counts as one parameter:

module Example exposing (Size, f)

type Size
  = Small

f : (Size, Size) -> Size
f p =
  Small

type declarations

A type declaration introduces a new type together with the constructors that build it. It is the keyword type, the type's name, zero or more type parameters, an =, and the variants separated by |.

module Example exposing (Colour)

type Colour
  = Red
  | Green
  | Blue

The type's name is uppercase-initial; its parameters are lowercase-initial, because they are type variables and are in scope throughout the variants.

module Example exposing (Either)

type Either a b
  = Left a
  | Right b

An uppercase parameter is a syntax error — it would be a type name, and a type declaration does not take types as parameters:

module Example exposing (Box)

type Box A
  = Box A

Each declaration introduces a genuinely new type. Two declarations of the same shape, in the same module or in different ones, are different types. A constructor may share its type's name; nothing is ambiguous, because one is a type and the other is a value.

module Example exposing (Celsius)

type Celsius
  = Celsius

A type may refer to itself, and two types declared in one module may refer to each other in either order — the declarations of a module are not read top to bottom.

module Example exposing (Chain)

type Chain
  = Link Chain
  | End

A type declaration can be exposed to other modules in two ways, and the module's exposing list is where the choice is made: naming the type on its own exposes it without its constructors, so other modules can mention Chain but cannot build or match one; naming it Chain(..) exposes the constructors too. Modules specifies both forms and why the difference matters.

What a variant may be

A variant is a constructor name followed by zero or more type arguments. That is the whole form: a variant is not a type expression, and a tuple, an arrow, or a bare type variable in variant position is not a variant.

A constructor name begins with an uppercase letter, so a lowercase name in variant position is rejected. This is the shape a mistyped constructor name takes, and the error points at the variant itself:

module Example exposing (Colour)

type Colour
  = red

A type variable is a lowercase name too, so a variable the declaration itself binds is rejected the same way when it appears in variant position instead of as an argument:

module Example exposing (Bad)

type Bad a
  = a

A tuple type in variant position is rejected:

module Example exposing (Size, Pair)

type Size
  = Small

type Pair
  = (Size, Size)

A function type is rejected, and the rejection covers the constructor written to the left of the arrow: Wrap Size -> Size is a single function type whose argument is Wrap Size, so Wrap sits inside the rejected form.

module Example exposing (Size, Wrapper)

type Size
  = Small

type Wrapper
  = Wrap Size -> Size

A variant's arguments are type expressions under the same rules as anywhere else, parenthesised as in Applying a type to arguments:

module Example exposing (Tree)

type Tree a
  = Node (Tree a) (Tree a)
  | Leaf a

A variant list has at least one variant

| appears strictly between variants — never before the first, never after the last — and a type declaration has at least one.

module Example exposing (Colour)

type Colour
  | Red

module Example exposing (Colour)

type Colour
  = Red
  |

module Example exposing (Empty)

type Empty
  =

Known gap: the first block is correctly rejected; the second and third should be and are not. A trailing | is ignored, and type Empty = declares a type with no constructors at all — something nothing can build, arrived at by accident (docs/tickets/lang-10.md).

A variant list is written with the separator leading each line, so appending a variant already touches exactly one line and a trailing | would buy nothing — which is why the trailing comma an exposing list allows has no counterpart here.

Type aliases

A type alias gives an existing type a second name. It introduces no new type: the alias and what it names are interchangeable everywhere, in both directions, including across module boundaries.

module Example exposing (Size, Pair)

type Size
  = Small

type alias Pair = (Size, Size)

Not implemented: type alias is a syntax error — the grammar reads type and then wants an uppercase name, and alias is neither (LANG-86). Several modules under std/core/src/ write aliases (Array.ignored) and the documentation comments in Maybe.zel and Result.zel use them in their examples, so this is a hole in the compiler rather than a question about the language. Every block of this section fails there.

Pair above is not a new type that happens to be a pair; it is (Size, Size), spelled differently. A function annotated Pair -> Size accepts a (Size, Size) with no conversion, and a type error mentioning one may mention the other. Where a genuinely distinct type is wanted — one the compiler will keep apart from its representation — that is a type declaration with a single variant.

An alias may take type parameters, written after its name the way a type declaration's are and in scope throughout the type it names. Every use applies it to exactly that many arguments: arity is part of the application for an alias as for a declared type, and an alias applied to fewer names no type.

module Example exposing (Size, Pair, both)

type Size
  = Small

type alias Pair a = (a, a)

both : Pair Size
both = (Small, Small)

An alias cannot name itself, directly or through another alias. It stands for the type written to the right of its =, and a type that mentions the alias has no such spelling. A recursive type is a type declaration, whose constructor is what the recursion turns on.

module Example exposing (Forever)

type alias Forever = (Forever, Forever)

An alias is exposed and imported by its name alone. It declares no constructors, so Pair(..) is an error in an exposing list and in an import.