unison/docs/LanguageReference.md
2019-07-30 23:24:44 -04:00

45 KiB
Raw Blame History

Unison Language Reference

(Unison version 1.0.M1)

This document is an informal reference for the Unison language, meant as an aid for Unison programmers as well as authors of implementations of the language.

  • This language reference, like the language it describes, is a work in progress and will be improved over time (GitHub link). Contributions and corrections are welcome!

A formal specification of Unison is outside the scope of this document, but links are provided to resources that describe the languages formal semantics.

Table of contents

A note on syntax

Unison is a language in which programs are not text. That is, the source of truth for a program is not its textual representation as source code, but its structured representation as an abstract syntax tree.

This document describes Unison in terms of its default (and currently, only) textual rendering into source code.

Top-Level declarations

This section describes the syntactic structure and informal semantics of Unison declarations.

A top-level declaration can appear at the top level or outermost scope of a Unison File. It can be a term binding, a user-defined data type, a user-defined ability, or a use clause.

Term Bindings

A Unison term binding consists of an optional type signature, and a term definition. For example:

timesTwo : Nat -> Nat
timesTwo x = x * 2

The first line in the above is a type signature. The type signature timesTwo : Nat -> Nat declares that the term named timesTwo is a function accepting an argument of type Nat and computes a value of type Nat. The type Nat is the type of 64-bit natural numbers starting from zero. See Unison types for details.

The second line is the term definition. The = sign splits the definition into a left-hand side, which is the term being defined, and the right-hand side, which is the definition of the term.

The general form of a term binding is:

name : Type
name p_1 p_2  p_n = expression

Type signature

name : Type is a type signature, where name is the name of the term being defined and Type is a type for that term. The name given in the type signature and the name given in the definition must be the same.

Type signatures are optional. In the absence of a type signature, Unison will automatically infer the type of a term declaration. If a type signature is present, Unison will verify that the term has the type given in the signature.

Term definition

A term definition has the form f p_1 p_2 … p_n = e where f is the name of the term being defined. The parameters p_1 through p_n are the names of parameters, if any (if the term is a function), separated by spaces. The right-hand side of the = sign is any Unison expression.

The names of the parameters as well as the name of the term are bound as local variables in the expression on the right-hand side (also known as the body of the function). When the function is called, the parameter names are bound to any arguments passed in the call. See function application for details on the call semantics of functions.

If the term takes no arguments, the term has the value of the fully evaluated expression on the right-hand side and is not a function.

The expression comprising the right-hand side can refer to the name given to the definition in the left-hand side. In that case, its a recursive definition. For example:

sumUpTo : Nat -> Nat
sumUpTo n = 
  if n < 2 then n 
  else n + sumUpto (drop n 1)

The above defines a function sumUpTo that recursively sums all the natural numbers less than some number n. As an example, sumUpTo 3 is 1 + 2 + 3, which is 6.

Note: The expression drop n 1 on line 4 above subtracts one from the natural number n. Since the natural numbers are not closed under subtraction (n - 1 is an Int), we use the operation drop which has the convention that drop n 0 = 0 for all natural numbers n. Unison's type system saves us from having to deal with negative numbers here.

Operator definitions

Operator identifiers are valid names for Unison definitions, but the syntax for defining them is slightly different. For example, we could define a binary operator ?:

(?) x y = if x == 0 then y else x 

Or we could define it using infix notation:

x ? y = if x == 0 then y else x

If we want to give the operator a qualified name, we put the qualifier inside the parentheses:

(MyNamespace.?) x y = if x == 0 then y else x 

Or if defining it infix:

x MyNamespace.? y = if x == 0 then y else x

The operator can be applied using either notation, no matter which way it's defined. See function application for details.

User-defined data types

A user-defined data type is introduced with the type keyword.

For example:

type Optional a = None | Some a

The = sign splits the definition into a left-hand side and a right-hand side, much like term definitions.

The left-hand side is the data type being defined. It gives a name for the data type and declares a new type constructor with that name (here its named Optional), followed by names for any type arguments (here there is one and its called a). These names are bound as type variables in the right-hand side. The right-hand side may also refer to the name given to the type in the left-hand side, in which case it is a recursive type declaration. Note that the fully saturated type construction Optional Nat is a type, whereas Optional by itself is a type constructor, not a type (it requires a type argument in order to construct a type).

The right-hand side consists of zero or more data constructors separated by |. These are data constructors for the type, or ways in which values of the type can be constructed. Each case declares a name for a data constructor (here the data constructors are None and Some), followed by the types of the arguments to the constructor.

When Unison compiles a type definition, it generates a term for each data constructor. Here they are the terms Some : a -> Optional a, and None : Optional a. It also generates patterns for matching on data (see Pattern Matching).

The general form of a type declaration is as follows:

type TypeConstructor p1 p2 … pn 
  = DataConstructor_1
  | DataConstructor_2
  ..
  | DataConstructor_n

User-defined abilities

A user-defined ability declaration has the following general form:

ability A p_1 p_2  p_n where
  Request_1 : Type_1
  Request_2 : Type_2
  Request_n : Type_n

This declares an ability type constructor A with type parameters p_1 through p_n, and request constructors Request_1 through Request_n.

See Abilities and Ability Handlers for more on user-defined abilities.

Use clauses

A use clause tells Unison to allow identifiers from a given namespace to be used unqualified in the code after the use clause.

In this example, the use .base.List clause allows the definition that follows it to refer to .base.List.take as simply take:

use .base.List

oneTwo = take 2 [1,2,3]

The general form of use clauses is as follows:

use namespace name_1 name_2 .. name_n

Where namespace is the namespace from which we want to use names unqualified, and name_1 through name_n are the names we want to use. If no names are given in the use clause, Unison allows all the names from the namespace to be used unqualified. There's no performance penalty for this, as use clauses are purely a syntactic convenience. When rendering code as text, Unison will insert precise use clauses that mention exactly the names it uses, even if the programmer omitted the list of names.

See the section on identifiers for more on namespaces as well as qualified and unqualified names.

Unison expressions

This section describes the syntax and informal semantics of Unison expressions.

Unisons evaluation strategy for expressions is Applicative Order Call-by-Value. See Function application for details.

Identifiers

Unison identifiers come in two flavors:

  1. Regular identifiers start with an alphabetic unicode character, emoji (which is any unicode character between 1F400 and 1FAFF inclusive), or underscore (_), followed by any number of alphanumeric characters, emoji, or the characters _, !, or '. For example, foo, _bar4, qux', and set! are valid regular identifiers.
  2. Operators consist entirely of the characters !$%^&*-=+<>.~\\/|:. For example, +, *, <>, and >>= are valid operators.

Namespace-qualified identifiers

The above describes unqualified identifiers. An identifier can also be qualified. A qualified identifier consists of a qualifier or namespace, followed by a ., followed by either a regular identifier or an operator. The qualifier is one or more regular identifiers separated by .. For example Foo.Bar.baz is a qualified identifier where Foo.Bar is the qualifier.

Absolutely qualified identifiers

Namespace-qualified identifiers described above are relative to a “current” namespace, which the programmer can set (and defaults to the root of the global namespace). To ignore the current namespace, an identifier can have an absolute qualifier. An absolutely qualified name begins with a .. For example, the name .base.List always refers to the name .base.List, regardless of the current namespace, whereas the name base.List will refer to foo.base.List if the current namespace is foo.

Note that operator identifiers may contain the character .. In order for this to not create ambiguity, the rule is as follows:

  1. . by itself is always an operator.
  2. Any other identifier beginning with . is an absolutely qualified identifier.
  3. A . immediately following a namespace is always a namespace separator.
  4. Otherwise a . is treated as part of an operator identifier.

if . is followed by whitespace or another operator character, the . is treated like an operator character. If it's followed by a regular identifier character, it's treated as a namespace separator.

Hash-qualified identifiers

Any identifier, including a namespace-qualified one, can appear hash-qualified. A hash-qualified identifier has the form x#h where x is an identifier and #h is a hash literal. The hash disambiguates names that may refer to more than one thing.

Reserved words

The following names are reserved by Unison and cannot be used as identifiers: =, :, ->, if, then, else, forall, handle, in, unique, where, use, and, or, true, false, type, ability, alias, let, namespace, case, of, with.

Blocks and statements

A block is an expression that has the general form:

statement_1
statement_2
...
statement_n
expression

A block can have zero or more statements, and the value of the whole block is the value of the final expression. A statement is either:

  1. A term definition which defines a term within the scope of the block. The definition is not visible outside this scope, and is bound to a local name. Unlike top-level definitions, a block-level definition does not result in a hash, and cannot be referenced with a hash literal.
  2. A Unison expression. In particular, blocks often contain action expressions, which are expressions evaluated solely for their effects. An action expression has type {A} T for some ability A (see Abilities and Ability Handlers) and some type T.

An example of a block (this evaluates to 16):

x = 4
y = x + 2
f a = a + y
f 10

A number of language constructs introduce blocks. These are detailed in the relevant sections of this reference. Wherever Unison expects an expression, a block can be introduced with the let keyword:

let <block>

Where <block> denotes a block as described above.

The Lexical Syntax of Blocks

The standard syntax expects statements to appear in a line-oriented layout, where whitespace is significant.

The opening keyword (let, if, then, or else, for example) introduces the block, and the position of the first character of the first statement in the block determines the top-left corner of the block. The beginning of each statement in the block must be lined up exactly with the left edge of the block. The first non-whitespace character that appears to the left of that edge (i.e. outdented) ends the block. Certain keywords also end blocks. For example, then ends the block introduced by if.

A statement or expression in a block can continue for more than one line as long as each line of the statement is indented further than the first character of the statement or expression.

For example, these are valid indentations for a block:

let 
  x = 1
  y = 2
  x + y


let x = 1
    y = 2
    x + y

Whereas these are incorrect:

let x = 1
  y = 2
  x + y

let x = 1
     y = 2
       x + y

Literals

A literal expression is a basic form of Unison expression. Unison has the following types of literals:

  • A 64-bit unsigned integer of type .base.Nat (which stands for natural number) consists of digits from 0 to 9. The smallest Nat is 0 and the largest is 18446744073709551615.
  • A 64-bit signed integer of type .base.Int consists of a natural number immediately preceded by either + or -. For example, 4 is a Nat, whereas +4 is an Int. The smallest Int is -9223372036854775808 and the largest is +9223372036854775807.
  • A 64-bit floating point number of type .base.Float consists of an optional sign (+/-), followed by two natural numbers separated by .. Floating point literals in Unison are IEEE 754-1985 double-precision numbers. For example 1.6777216 is a valid floating point literal.
  • A text literal of type .base.Text is any sequence of Unicode characters between pairs of ". The escape character is \, so a " can be included in a text literal with the escape sequence \". The full list of escape sequences is given in the Escape Sequences section below. For example, "Hello, World!" is a text literal. A text literal can span multiple lines. Newlines do not terminate text literals, but become part of the literal text.
  • There are two Boolean literals: true and false, and they have type Boolean.
  • A hash literal begins with the character #. See the section Hashes for details on the lexical form of hash literals. A hash literal is a reference to a term or type. The type or term that it references must have a definition whose hash digest matches the hash in the literal. The type of a hash literal is the same as the type of its referent. #abc123e is an example of a hash literal.
  • A literal list has the general form [v1, v2, ... vn] where v1 through vn are expressions. A literal list may be empty. For example, [], [x], and [1,2,3] are list literals. The expressions that form the elements of the list all must have the same type. If that type is T, then the type of the list literal is .base.List T or [T].
  • A function literal or lambda has the form p1 p2 ... pn -> e, where p1 through pn are regular identifiers and e is a Unison expression (the body of the lambda). The variables p1 through pn are local variables in e, and they are bound to any values passed as arguments to the function when its called (see the section Function Application for details on call semantics). For example x -> x + 2 is a function literal.
  • A tuple literal has the form (v1,v2, ..., vn) where v1 through vn are expressions. A value (a,b) has type (A,B) if a has type A and b has type B. The expression (a) is the same as the expression a. The nullary tuple () (pronounced “unit”) is of the trivial type (). See tuple types for details on these types and more ways of constructing tuples.

Escape sequences

Text literals can include the following escape sequences:

  • \0 = null character
  • \a = alert (bell)
  • \b = backspace
  • \f = form feed
  • \n = new line
  • \r = carriage return
  • \t = horizontal tab
  • \v = vertical tab
  • \\ = literal \ character
  • \' = literal ' character
  • \" = literal " character

Comments

A line comment starts with -- and is followed by any sequence of characters. A line that contains a comment cant contain anything other than a comment and whitespace. Line comments are currently ignored by Unison.

A line starting with --- and containing no other characters is a fold. Any text below the fold is ignored by Unison.

Unison does not currently support block comments. A comment can span multiple lines by adding -- to the front of each line of the comment.

Type annotations

A type annotation has the form e:T where e is an expression and T is a type. This tells Unison that e should be of type T (or a subtype of type T), and Unison will check whether this is true. It's a type error for the actual type of e to be anything other than a type that conforms to T.

Parenthesized expressions

Any expression can appear in parentheses, and an expression (e) is the same as the expression e. Parentheses can be used to delimit where an expression begins and ends. For example (f : P -> Q) y is an application of the function f of type P -> Q to the argument y. The parentheses are needed to tell Unison that y is an argument to f, not a part of the type annotation expression.

Function application

A function application f a1 a2 an applies the function f to the arguments a1 through an.

The above syntax is valid where f is a regular identifier. If the function name is an operator such as *, then the syntax for application is infix : a1 * a2. Any operator can be used in prefix position by surrounding it in parentheses: (*) a1 a2. Any regular identifier can be used infix by surrounding it in backticks: a1 `f` a2

All Unison functions are of arity 1. That is, they take exactly one argument. An n-ary function is modeled either as a unary function that returns a further function (a partially applied function) which accepts the rest of the arguments, or as a unary function that accepts a tuple.

Function application associates to the left, so the expression f a b is the same as (f a) b. If f has type T1 -> T2 -> Tn then f a is well typed only if a has type T1. The type of f a is then T2 -> Tn. The type constructor of function types, ->, associates to the right. So T1 -> T2 -> Tn parenthesizes as T1 -> (T2 -> TN).

The evaluation semantics of function application is applicative order Call-by-Value. In the expression f x y, x and y are fully evaluated in left-to-right order, then f is fully evaluated, then x and y are substituted into the body of f, and lastly the body is evaluated.

An exception to the evaluation semantics is Boolean expressions, which have non-strict semantics.

Boolean expressions

A Boolean expression has type Boolean which has two values, true and false.

Conditional expressions

A conditional expression has the form if c then t else f, where c is an expression of type Boolean, and t and f are expressions of any type, but t and f must have the same type.

Evaluation of conditional expressions is non-strict. The evaluation semantics of if c then t else f are:

  • The condition c is always evaluated.
  • If c evaluates to true, the expression t is evaluated and f remains unevaluated. The whole expression reduces to the value of t.
  • If c evaluates to false, the expression f is evaluated and t remains unevaluated. The whole expression reduces to the value of f.

The keywords if, then, and else each introduce a Block as follows:

if 
  <block>
then
  <block>
else
  <block>

Boolean conjunction and disjunction

A Boolean conjunction expression is a Boolean expression of the form and a b where a and b are Boolean expressions. Note that and is not a function, but built-in syntax.

The evaluation semantics of and a b are equivalent to if a then b else false.

A Boolean disjunction expression is a Boolean expression of the form or a b where a and b are Boolean expressions. Note that or is not a function, but built-in syntax.

The evaluation semantics of or a b are equivalent to if a then true else b.

Delayed computations

An expression can appear delayed as 'e, which is the same as _ -> e. If e has type T, then 'e has type () -> T.

If c is a delayed computation, it can be forced with !c, which is the same as c (). The expression c must have a type () -> t for some type t, in which case !c has type t.

Delayed computations are important for writing expressions that require abilities. For example:

use io

program : '{IO} ()
program = 'let
  printLine "What is your name?"
  name = !readLine
  printLine ("Hello, " ++ name)

This example defines a small I/O program. The type {IO} () by itself is not allowed as the type of a top-level definition, since the IO ability must be provided by a handler, see abilities and ability handlers). Instead, program has the type '{IO} () (note the ' indicating a delayed computation). Inside a handler for IO, this computation can be forced with !program.

Inside the program, !readLine has to be forced, as the type of io.readLine is '{IO} Text, a delayed computation which, when forced, reads a line from standard input.

Case expressions and pattern matching

A case expression has the general form:

case e of 
  pattern_1 -> block_1
  pattern_2 -> block_2
  ...
  pattern_n -> block_n

Where e is an expression, called the scrutinee of the case expression, and each case has a pattern to match against the value of the scrutinee and a block to evaluate in case it matches.

The evaluation semantics of case expressions are as follows:

  1. The scrutinee is evaluated.
  2. The first pattern is evaluated and matched against the value of the scrutinee.
  3. If the pattern matches, any variables in the pattern are substituted into the block to the right of its -> (called the match body) and the block is evaluated. If the pattern doesnt match then the next pattern is tried and so on.

It's possible for Unison to actually evaluate cases in a different order, but such evaluation should always have the same observable behavior as trying the patterns in sequence.

It is an error if none of the patterns match. In this version of Unison, the error occurs at runtime. In a future version, this should be a compile-time error.

Pattern matching

A pattern has one of the following forms:

Blank patterns

A blank pattern has the form _. It matches any expression without creating a variable binding.

For example:

case 42 of
  _ -> "Always matches"
Literal patterns

A literal pattern is a literal Boolean, Nat, Int, Float, or Text. A literal pattern matches if the scrutinee has that exact value.

For example:

case 2 + 2 of
  4 -> "Matches"
  _ -> "Doesn't match"
Variable patterns

A variable pattern is a regular identifier and matches any expression. The expression that it matches will be bound to that identifier as a variable in the match body.

For example, this expression evaluates to 3:

case 1 + 1 of
  x -> x + 1
As-patterns

An as-pattern has the form v@p where v is a regular identifier and p is a pattern. This pattern matches if p matches, and the variable v will be bound in the body to the value matching p.

For example, this expression evaluates to 3:

case 1 + 1 of
  x@4 -> x * 2
  y@2 -> y + 1
  _   -> 22
Constructor patterns

A constructor pattern has the form C p1 p2 ... pn where C is the name of a data constructor in scope, and p1 through pn are patterns such that n is the arity of C. Note that n may be zero. This pattern matches if the scrutinee reduces to a fully applied invocation of the data constructor C and the patterns p1 through pn match the arguments to the constructor.

For example, this expression uses Some and None, the constructors of the Optional type, to return the 3rd element of the list xs if present or 0 if there was no 3rd element.

case List.at 3 xs of
  None -> 0
  Some x -> x 
List patterns

A list pattern matches a List t for some type t and has one of three forms:

  1. head +: tail matches a list with at least one element. The pattern head is matched against the first element of the list and tail is matched against the suffix of the list with the first element removed.
  2. init :+ last matches a list with at least one element. The pattern init is matched against the prefix of the list with the last element removed, and last is matched against the last element of the list.
  3. A literal list pattern has the form [p1, p2, ... pn] where p1 through pn are patterns. The patterns p1 through pn are matched against the elements of the list. This pattern only matches if the length of the scrutinee is the same as the number of elements in the pattern. The pattern [] matches the empty list.

Examples:

first : [a] -> Optional a
first as = case as of
  h +: _ -> Some h
  [] -> None

last : [a] -> Optional a
last as = case as of
  _ :+ l -> Some l
  [] -> None

exactlyOne : [a] -> Boolean
exactlyOne a = case a of
  [_] -> true
  _   -> false
Tuple patterns

A tuple pattern has the form (p1, p2, ... pn) where p1 through pn are patterns. The pattern matches if the scrutinee is a tuple of the same arity as the pattern and p1 through pn match against the elements of the tuple. The pattern (p) is the same as the pattern p, and the pattern () matches the literal value () of the trivial type () (both pronounced “unit”).

For example, this expression evaluates to 4:

case (1,2,3) of
  (a,_,c) -> a + c
Ability patterns

An ability pattern only appears in an ability handler and has one of two forms (see Abilities and ability handlers for details):

  1. {C p1 p2 ... pn -> k} where C is the name of an ability constructor in scope, and p1 through pn are patterns such that n is the arity of C. Note that n may be zero. This pattern matches if the scrutinee reduces to a fully applied invocation of the ability constructor C and the patterns p1 through pn match the arguments to the constructor. The scrutinee must be of type Effect A T for some ability {A} and type T. The variable k will be bound to the continuation of the program. If the scrutinee has type Effect A T and C has type X ->{A} Y, then k has type Y -> {A} T.
  2. {p} where p is a pattern. This matches the case where the computation is pure (the value of type Effect A T calls none of the constructors of the ability {A}). A pattern match on an Effect is not complete unless this case is handled.

See the section on abilities and ability handlers for examples of ability patterns.

Guard patterns

A guard pattern has the form p | g where p is a pattern and g is a Boolean expression that may reference any variables bound in p. The pattern matches if p matches and g evaluates to true.

For example, the following expression evaluates to 6:

case 1 + 2 of
  x | x == 4 -> 0
  x | x + 1 == 4 -> 6
  _ -> 42

Hashes

A hash in Unison is a 512-bit SHA3 digest of a term or a type. The textual representation of a hash is its base32Hex Unicode encoding.

Unison attributes a hash to every term and type declaration, and the hash may be used to unambiguously refer to the term or type. As far as Unison is concerned, the hash of a term or type is its true name.

Literal hash references

A term, type, data constructor, or ability constructor may be unambiguously referenced by hash. Literal hash references have the following structure:

  • A built-in reference to a Unison built-in term or type n has a hash of the form ##n. ##Nat is an example of a built-in reference.
  • A term definition has a hash of the form #x where x is the base32Hex encoding of the hash of the term.
  • A term or type definition thats part of a cycle of mutually recursive definitions hashes to the form #x.n where x is the hash of the cycle and n is the term or types index in its cycle. A cycle has a canonical order determined by sorting all the members of the cycle by their individual hashes (with the cycle removed).
  • A data constructor hashes to the form #x#c where x is the hash of the data type definition and c is the index of that data constructor in the type definition.
  • A data constructor in a cyclic type definition hashes to the form #x.n#c where #x.n is the hash of the data type and c is the data constructors index in the type definition.

Short hashes

A hash literal may use a prefix of the base32Hex encoded SHA3 digest instead of the whole thing. For example a short hash like #r1mtr0 may be used instead of the much longer 104-character representation of the full 512-bit hash.

Unison types

This section describes informally the structure of types in Unison.

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

Unison extends that type system with, pattern matching, scoped type variables, ability types (also known as algebraic effects). See the section titled Abilities and Ability Handlers for details on ability types.

Unison attributes a type to every expression. Types are of the following general forms.

Type variables

Type variables are regular identifiers beginning with a lowercase letter. For example a, x0, and foo are valid type variables.

Universally quantified types

A universally quantified type has the form forall v1 v2 vn. t, where t is a type. The type t may involve the variables v1 through vn.

The symbol is an alias for forall.

A type like forall x. F x can be written simply as F x (the forall x is implied) as long as x is free in F x (it is not bound by an outer scope; see Scoped Type Variables below).

A universally quantified type may be instantiated at any given type. For example, the empty list [] has type forall x. List x, and it can be instantiated at Int, which binds x to Int resulting in List Int which is also a valid type for the empty list.

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 annotation temp:x is telling Unison that temp has the type x which is bound in the type signature, so temp and a have the same type.

ex1 : x -> y -> x
ex1 a b =
  -- refers to the type x in the outer scope
  temp : x
  temp = a
  a

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 =
  -- doesnt refer to x in outer scope
  id :  x . x -> x
  id x = x
  id 42
  id a

Type constructors

Just as values are built using data constructors, types are built from type constructors. Nullary type constructors like Nat, Int, Float are already types, but other type constructors like List and Tuple (see built-in type constructors) take type parameters in order to yield types. List is a unary type constructor, so it takes one type (the type of the list elements) . List Nat is a type and Tuple Nat Int is a type.

Kinds of Types

Types are to values as kinds are 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. Unisons kinds have the following forms:

  • A nullary type constructor or ordinary type has kind Type.
  • A type constructor has kind k1 -> k2 where k1 and k2 are kinds.

For example List, a unary type constructor, has kind Type -> Type (it takes a type and yields a type), a binary type constructor like Tuple has kind Type -> Type -> Type (it takes a type and yields a partially applied unary type constructor). A type constructor of kind (Type -> Type) -> Type is a higher-order type constructor (it takes a 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 T applies the type constructor C to the type T. Type application associates to the left, so the type A B C is the same as the type (A B) C.

Function types

The type X -> Y is a type for functions that take arguments of type X and yield results of type Y. Application of the binary type constructor -> associates to the right, so the type X -> Y -> Z is the same as the type X -> (Y -> Z).

Tuple types

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

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

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

In the standard Unison syntax, tuples of arity 2 and higher are actually of a type Tuple a b for some types a and b. For example, (X,Y) is syntactic shorthand for the type Tuple X (Tuple Y ()).

Tuples are either constructed with the syntactic shorthand (a,b) (see tuple literals) or with the built-in Tuple.Cons data constructor: Tuple.Cons a (Tuple.Cons b ()).

Built-in types

Unison provides the following built-in types:

  • .base.Nat is the type of 64-bit natural numbers, also known as unsigned integers. They range from 0 to 18,446,744,073,709,551,615.
  • .base.Int is 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.
  • .base.Float is the type of IEEE 754-1985 double-precision floating point numbers.
  • .base.Boolean is the type of Boolean expressions whose value is true or false.
  • .base.Bytes is the type of arbitrary-length 8-bit byte sequences.
  • .base.Text is the type of arbitrary-length strings of Unicode text.
  • The trivial type () (pronounced “unit”) is the type of the nullary tuple. There is a single data constructor of type () and its also written ().

Built-in type constructors

Unison has the following built-in type constructors.

  • (->) is the constructor of function types. A type X -> Y is the type of functions from X to Y.
  • base.Tuple is the constructor of tuple types. A type Tuple X Y is the type of pairs of values, one of type X and the other of type Y. The form (A,B) is shorthand for Tuple A (Tuple B ()), and (A,B,C) is short for Tuple A (Tuple B (Tuple C ())) and so on.
  • .base.List is the constructor of list types. A type List T is the type of arbitrary-length sequences of values of type T.
  • .base.Request is the constructor of requests for abilities. A type Request A T is the type of values received by ability handlers for the ability A where current continuation requires a value of type T.

Abilities and ability handlers

Unison provides a system of abilities and ability handlers as a means of modeling computational effects in a purely functional language. This is based on the Frank language by Sam Lindley, Conor McBride, and Craig McLaughlin (https://arxiv.org/pdf/1611.09259.pdf).

Abilities in function types

The general form for a function type in Unison is I ->{A} O, where I is the input type of the function, O is the output type, and A is the set of abilities that the function requires.

A function type in Unison like A -> B is really syntactic sugar for a type A ->{e} B where e is some set of abilities, possibly empty. A function that definitely requires no abilities has a type like A ->{} B (it has an empty set of abilities).

If a function f calls in its implementation another function requiring ability set {A}, then f will require A in its ability set as well. If f also calls a function requiring abilities {B}, then f will require abilities {A,B}.

Stated the other way around, f can only be called in contexts where the abilities {A,B} are available. Abilities are provided by handle blocks. See the Ability Handlers section below.

User-defined abilities

A user-defined ability is declared with an ability declaration such as:

ability Store v where
  get : v
  put : v -> ()

This results in a new ability type constructor Store which takes a type argument v. It also create two value-level constructors named get and put. They have the following types:

  • get : forall v. {Store v} v
  • put : forall v. v ->{Store v} ()

The type {Store v} means that the computation which results in that type requires a Store v ability and cannot be executed except in the context of an ability handler that provides the ability.

Ability handlers

A constructor {A} T for some ability A and some type T (or a function which uses such a constructor), can only be used in a scope where the ability A is provided. Abilities are provided by handle expressions:

handle h in x

This expression gives x access to abilities handled by the function h which must have the type Request A T -> T if x has type {A} T. The type constructor Request is a special builtin provided by Unison which will pass arguments of type Request A T to a handler for the ability A.

Pattern matching on ability constructors

Each constructor of an ability corresponds with a pattern that can be used for pattern matching in ability handlers. The general form of such a pattern is:

{A.c p_1 p_2 p_n -> k}

Where A is the name of the ability, c is the name of the constructor, p_1 through p_n are patterns matching the arguments to the constructor, and k is a continuation for the program. If the value matching the pattern has type Request A T and the constructor of that value had type X ->{A} Y, then k has type Y -> {A} T.

A handler can choose to call the continuation or not. For example, a handler can ignore the continuation in order to handle an ability that aborts the execution of the program:

ability Abort where
  aborting : ()

-- Returns `a` immediately if the program `e` calls `abort`
abortHandler : a -> Effect Abort a -> a
abortHandler a e = case e of 
   { Abort.aborting -> _ } -> a
   { x } -> x

p = handle abortHandler 0 in
  x = 4
  Abort.aborting
  x + 2

The program p evaluates to 0. If we remove the Abort.aborting call, it evaluates to 6.

The pattern { x } matches the case where the computation is pure (makes no further requests for the Abort ability and the continuation is empty). A pattern match on a Request is not complete unless this case is handled.

When a handler calls the continuation, it needs describe how the ability is provided in the rest of the program, usually with a recursive call, like this:

use .base Effect
 
ability Stored v where
  get : v
  put : v -> ()

storeHandler : v -> Effect (Stored v) a -> a
storeHandler storedValue s = case s of 
  {Stored.get -> k} ->
    handle storeHandler storedValue in k storedValue
  {Stored.put v -> k} ->
    handle storeHandler v in k ()
  {a} -> a

Note that the storeHandler has a handle clause that uses storeHandler itself to handle the Requestss made by the continuation. So its a recursive definition.

Name resolution and the environment

During typechecking, Unison substitutes free variables in an expression by looking them up in an environment populated from a codebase of available definitions. A Unison codebase is a database of term and type definitions, indexed by hashes and names.

A name in the environment can refer to either terms or types, or both. If a name is unambiguous (refers to only one term or type in the environment), Unison substitutes that name in the expression with a reference to the definition.

Hash literals in the program are substituted with references to the definitions in the environment whose hashes they match.

If a free variable in the program cannot be found in the environment and is not the name of another term in scope in the program itself, or if an free variable matches more than one name (its ambiguous), Unison tries type-directed name resolution.

Type-directed name resolution

During typechecking, if Unison encounters a free variable that is not a name in the environment, Unison attempts type-directed name resolution, which:

  1. Finds term definitions in the environment whose unqualified name is the same as the free variable.
  2. If exactly one of those terms would make the program typecheck when substituted for the free variable, perform that substitution and resume typechecking.

If name resolution is unable to find the definition of a name, or is unable to disambiguate an ambiguous name, Unison reports an error.