# Transfer language reference

Author: Björn Bringert <bringert@cs.chalmers.se>
Last update: Fri Dec 9 11:55:35 2005

- Current implementation status
- Layout syntax
- Imports
- Function declarations
- Data type declarations
- Lambda expressions
- Local definitions
- Types
  - Function types
  - Basic types
  - Records
  - Tuples
  - Lists
- Case expressions
- Patterns
  - Constructor patterns
  - Variable patterns
  - Wildcard patterns
  - Record patterns
  - Disjunctive patterns
  - List patterns
  - Tuple patterns
  - String literal patterns
  - Integer literal patterns
- Metavariables
- Overloaded functions
  - Type class extension
  - Extending multiple classes
- Standard prelude
- Operators
  - Unary operators
  - Binary operators
- Compositional functions
- do notation

WARNING: The Transfer language is still experimental. Its syntax, type system and semantics may change without notice. I will try to help you with any problems this might cause, but I will not refrain from changing the language solely for reasons of backwards compatibility.

This document describes the features of the Transfer language. See the Transfer tutorial for an example of a Transfer program, and how to compile and use Transfer programs.

Transfer is a dependently typed functional programming language with eager evaluation. The language supports generalized algebraic datatypes, pattern matching and function overloading.

## Current implementation status

Not all features of the Transfer language have been implemented yet. The most important missing piece is the type checker. This means that there are almost no checks done on Transfer programs before they are run. It also means that the values of metavariables are not inferred. Thus metavariables cannot be used where their values matter. For example, dictionaries for overloaded functions must be given explicitly, not as metavariables.

## Layout syntax

Transfer uses layout syntax, where the indentation of a piece of code determines which syntactic block it belongs to.

To give the block structure without using layout syntax, you can enclose the block in curly braces and separate the parts of the blocks with semicolons.

For example, this case expression:

      case x of
             p1 -> e1
             p2 -> e2

is equivalent to this one:

      case x of {
             p1 -> e1 ;
             p2 -> e2
      }

Here the layout is insignificant, as the structure is given with braces and semicolons. Thus it is equivalent to:

      case x of { p1 -> e1 ; p2 -> e2 }

## Imports

A Transfer module starts with some imports. Most modules will have to import the prelude, which contains definitons used by most programs:

      import prelude

For more information about the standard prelude, see Standard prelude.

## Function declarations

Functions need to be given a type and a definition. The type is given by a typing judgement on the form:

      f : T

where `f` is the function's name, and `T` its type. See Function types for a how the types of functions are written.

The definition of the function is then given as a sequence of pattern equations. The first equation whose patterns match the function arguments is used when the function is called. Pattern equations are on the form:

      f p11 ... p1m = exp1
      ...
      f pn1 ... pnm = expn

where `p11` to `pnm` are patterns, see Patterns.

Pattern equations can also have guards, boolean expressions which determine whether to use the equation when the pattern has been matched. Pattern equations with guards are written:

      f p11 ... p1m | guard1 = exp1
      ...
      f pn1 ... pnm | guardn = expn

Pattern equations with and without guards can be mixed in the definiton of a function.

Any variables bound in the patterns are in scope in the guards and right hand sides of each pattern equation.

## Data type declarations

Transfer supports Generalized Algebraic Datatypes. They are declared thusly:

      data D : T where
           c1 : Tc1
           ...
           cn : Tcn

Here `D` is the name of the data type, `T` is the type of the type constructor, `c1` to `cn` are the data constructor names, and `Tc1` to `Tcn` are their types.

FIXME: explain the constraints on the types of type and data constructors.

## Lambda expressions

Lambda expressions are terms which express functions, without giving names to them. For example:

      \x -> x + 1

is the function which takes an argument, and returns the value of the argument + 1.

## Local definitions

To give local definition to some names, use:

      let x1 : T1 = exp1
          ...
          xn : Tn = expn
       in exp

Here, the variables `x1` to `xn` are in scope in all the expressions `exp1` to `expn`, and in `exp`. Thus let-defined functions can be mutually recursive.

## Types

### Function types

Functions types are of the form:

      A -> B

This is the type of functions which take an argument of type `A` and returns a result of type `B`.

To write functions which take more than one argument, we use currying. A function which takes n arguments is a function which takes one argument and returns a function which takes n-1 arguments. Thus,

      A -> (B -> C)

or, equivalently, since `->` associates to the right:

      A -> B -> C

is the type of functions which take teo arguments, the first of type `A` and the second of type `B`. This arrangement lets us do partial application of function to fewer arguments than the function is declared to take, returning a new function which takes the rest of the arguments.

#### Dependent function types

In a function type, the value of an argument can be used later in the type. Such dependent function types are written:

      (x : A) -> B

Here, `x` is in scope in `B`.

### Basic types

#### Integers

The type of integers is called `Integer`. Standard decmial integer literals, such as `0` and `1234` are used to represent values of this type.

#### Floating-point numbers

The only currently supported floating-point type is `Double`, which supports IEEE-754 double-precision floating-point numbers. Double literals are written in decimal notation, e.g. `123.456`.

#### Strings

There is a primitive `String` type. String literals are written with double quotes, e.g. `"this is a string"`. FIXME: This might be replaced by a list of characters representation in the future.

#### Booleans

Booleans are not a built-in type, though some features of the Transfer language depend on them. The `Bool` type is defined in the Standard prelude.

      data Bool : Type where
              True : Bool
              False : Bool

In addition to normal pattern matching on booleans, you can use the built-in if-expression:

      if exp1 then exp2 else exp3

where `exp1` must be an expression of type `Bool`.

### Records

#### Record types

Record types are created by using a `sig` expression:

      sig { l1 : T1; ... ; ln : Tn }

Here, `l1` to `ln` are the field labels and `T1` to `Tn` are field types.

#### Record values

Record values are constructed using `rec` expressions:

      rec { l1 = exp1; ... ; ln = expn }

#### Record projection

Fields are selected from records using the `.` operator. This expression selects the field `l` from the record value `r`:

      r.l

#### Records and layout syntax

The curly braces and semicolons are simply explicit layout syntax, so the record type and record expression above can also be written as:

      sig l1 : T1
          ...
          ln : Tn

      rec l1 = exp1
          ...
          ln = expn

#### Record subtyping

A record of some type R1 can be used as a record of any type R2 such that for every field `p1 : T1` in R2, `p1 : T1` is also a field of T1.

### Tuples

Tuples on the form:

      (exp1, ..., expn)

are syntactic sugar for records with fields `p1` to `pn`. The expression above is equivalent to:

      rec { p1 = exp1; ... ; pn = expn }

### Lists

The `List` type is not built-in, though there is some special syntax for it. The list type is declared as:

      data List : Type -> Type where
              Nil : (A:Type) -> List A
              Cons : (A:Type) -> A -> List A -> List A

The empty list can be written as `[]`. There is an operator `::` which can be used instead of `Cons`. These are just syntactic sugar for expressions using `Nil` and `Cons`, with the type arguments hidden.

## Case expressions

Pattern matching is done in pattern equations and with the `case` construct:

      case exp of
           p1 | guard1 -> rhs1
           ...
           pn | guardn -> rhsn

where `p1` to `pn` are patterns, see Patterns. `guard1` to `guardn` are boolean expressions. Case arms can also be written without guards, such as:

           pk -> rhsk

This is the same as writing:

           pk | True -> rhsk

## Patterns

### Constructor patterns

Constructor patterns are written as:

      C p1 ... pn

where `C` is a data constructor which takes `n` arguments. If the value to be matched is `C v1 ... vn`, then `v1` to `vn` will be matched against `p1` to `pn`.

### Variable patterns

A variable pattern is a single identifier:

      x

A variable pattern matches any value, and binds the variable name to the value. A variable may not occur more than once in a pattern. Note that variable patterns may not use the same identifier as data constructors which are in scope, since they will then be interpreted as constructor patterns.

### Wildcard patterns

Wildcard patterns are written with a single underscore:

      _

Wildcard patterns match all values and bind no variables.

### Record patterns

Record patterns match record values:

      rec { l1 = p1; ... ; ln = pn }

A record value matches a record pattern if the record value has all the fields `l1` to `ln`, and their values match `p1` to `pn`.

Note that a record value may have more fields than the record pattern. The values of these fields do not influence the pattern matching.

### Disjunctive patterns

It is possible to write a pattern on the form:

      p1 || ... || pn

A value will match this pattern if it matches any of the patterns `p1` to `pn`. FIXME: talk about how this is expanded

### List patterns

When pattern matching on lists, there are two special constructs. A whole list can by matched be a list of patterns:

      [p1, ... , pn]

This pattern will match lists of length n, such that each element in the list matches the corresponding pattern. The empty list pattern:

      []

is a special case of this. It matches the empty list, oddly enough.

Non-empty lists can also be matched with `::`-patterns:

      p1::p2

This pattern matches non-empty lists such that the first element of the list matches `p1` and the rest of the list matches `p2`.

### Tuple patterns

Tuples patterns on the form:

      (p1, ... , pn)

are syntactic sugar for record patterns, in the same way as tuple expressions, see Tuples.

### String literal patterns

String literals can be used as patterns.

### Integer literal patterns

Integer literals can be used as patterns.

## Metavariables

Metavariables are written as questions marks:

      ?

A metavariable is a way to tell the type checker that: "you should be able to figure out what this should be, I can't be bothered to tell you".

Metavariables can be used to avoid having to give type and dictionary arguments explicitly.

## Overloaded functions

In Transfer, functions can be overloaded by having them take a record of functions as an argument. For example, the functions for equality and inequality in the Transfer Prelude are defined as:

      Eq : Type -> Type
      Eq A = sig eq : A -> A -> Bool

      eq : (A : Type) -> Eq A -> A -> A -> Bool
      eq _ d = d.eq

      neq : (A : Type) -> Eq A -> A -> A -> Bool
      neq A d x y = not (eq A d x y)

We call `Eq` a type class, though it's actually just a record type used to pass function implementations to overloaded functions. We call a value of type `Eq A` an Eq dictionary for the type A. The dictionary is used to look up the version of some function for the particular type we want to use the function on. Thus, in order to use the `eq` function on two integers, we need a dictionary of type `Eq Integer`:

      eq_Integer : Eq Integer
      eq_Integer = rec eq = prim_eq_Integer

where `prim_eq_Integer` is the built-in equality function for integers. To check whether two numbers `x` and `y` are equal, we can then call the overloaded `eq` function with the dictionary:

      eq Integer eq_Integer x y

Giving the type at which to use the overloaded function, and the appropriate dictionary can be cumbersome. Metavariables come to the rescue:

      eq ? ? x y

The type checker can in most cases figure out the values of the type and dictionary arguments. NOTE: this is not implemented yet.

### Type class extension

By using record subtyping, see Record subtyping, we can create type classes which extend other type classes. A dictionary for the new type class can also be used as a dictionary for old type class.

For example, we can extend the `Eq` type class above to `Ord`, a type class for orderings:

      Ord : Type -> Type
      Ord A = sig eq : A -> A -> Bool
                  compare : A -> A -> Ordering

To extend an existing class, we keep the fields of the class we want to extend, and add any new fields that we want. Because of record subtyping, for any type `A`, a value of type `Ord A` is also a value of type `Eq A`.

### Extending multiple classes

A type class can also extend several classes, by simply having all the fields from all the classes we want to extend. The `Num` class in the Standard prelude is an example of this.

## Standard prelude

The standard prelude, see prelude.tra, contains definitions of a number of standard types, functions and type classes.

## Operators

Most built-in operators in the Transfer language are translated to calls to overloaded functions. This means that they can be used at any type for which there is a dictionary for the type class in question.

### Unary operators

Operator | Precedence | Translation
--- | --- | ---
`-` | 10 | `-x => negate ? ? x`

### Binary operators

Operator | Precedence | Associativity | Translation of `x op y`
--- | --- | --- | ---
`>>=` | 3 | left | `bind ? ? x y`
`>>` | 3 | left | `bind ? ? x (\_ -> y)`
`||` | 4 | right | `if x then True else y`
`&&` | 5 | right | `if x then y else False`
`==` | 6 | none | `eq ? ? x y`
`/=` | 6 | none | `neq ? ? x y`
`<` | 6 | none | `lt ? ? x y`
`<=` | 6 | none | `le ? ? x y`
`>` | 6 | none | `gt ? ? x y`
`>=` | 6 | none | `ge ? ? x y`
`::` | 7 | right | `Cons ? ? x y`
`+` | 8 | left | `plus ? ? x y`
`-` | 8 | left | `minus ? ? x y`
`*` | 9 | left | `times ? ? x y`
`/` | 9 | left | `div ? ? x y`
`%` | 9 | left | `mod ? ? x y`

## Compositional functions

## do notation

Sequences of operations in the Monad type class can be written using do-notation, like in Haskell:

      do x <- f
         y <- g x
         h y

is equivalent to:

      f >>= \x -> g x >>= \y -> h y