104 lines
2.8 KiB
Markdown
104 lines
2.8 KiB
Markdown
+++
|
|
title = "Types"
|
|
weight = 2
|
|
sort_by = "weight"
|
|
insert_anchor_links = "right"
|
|
+++
|
|
|
|
Every value expression and, in particular, every value identifier in BH
|
|
has a *type*. In some cases the programmer must supply a *type
|
|
signature* specifying this and in many cases the compiler infers it
|
|
automatically. The BH programmer should be aware of types at all times.
|
|
|
|
```
|
|
type ::= btype [ "->" type ]
|
|
btype ::= [ btype ] atype
|
|
atype ::= tycon | tyvar | ( { type , } )
|
|
tycon ::= conId
|
|
```
|
|
|
|
|
|
Most type expressions have the form: *TypeConstructor* $t_1$ $\cdots$
|
|
$t_n$ where $t_1$ $\cdots$ $t_n$ are themselves type expressions, and $n
|
|
{\geq} 0$. The $t_1$ $\cdots$ $t_n$ are referred to as the *type
|
|
arguments* to the type constructor. $n$ is also called the *arity* of
|
|
the type constructor.
|
|
|
|
|
|
Familiar basic types have zero-arity type constructors (no type
|
|
arguments, $n = 0$). Examples:
|
|
|
|
- `Integer`
|
|
- `Bool`
|
|
- `String`
|
|
- `Action`
|
|
|
|
Other type constructors have arity $n > 0$; these are also known as
|
|
*parameterized types*.
|
|
|
|
Examples:
|
|
|
|
- `List Bool`
|
|
- `List (List Bool)`
|
|
- `Array Integer String`
|
|
- `Maybe Integer`
|
|
|
|
These represent the types of lists of
|
|
Booleans, lists of lists of Booleans, arrays indexed by integers and
|
|
containing strings, and an optional result possibly containing an
|
|
integer.
|
|
|
|
|
|
A type can be *polymorphic*, indicated using type variables. Examples:
|
|
|
|
- `List a`
|
|
- `List (Llist b)`
|
|
- `Array i (List String)`
|
|
|
|
|
|
These represent lists of things of some unknown type "`a`", lists of
|
|
lists of things of some unknown type "`b`", and arrays indexed by some
|
|
unknown type "`i`" and containing lists of strings.
|
|
|
|
|
|
One type constructor is given special status in the syntax. The type of
|
|
functions from arguments of type $t_1$ to results of type $t_2$ could
|
|
have been written as:
|
|
|
|
Function $t_1$ $t_2$
|
|
|
|
but in BH we write the constructor as an infix arrow:
|
|
|
|
$t_1$ -\> $t_2$
|
|
|
|
These associate to the right, *i.e.,*
|
|
|
|
$t_1$ -\> $\cdots$ -\> $t_{n-1}$ -\> $t_n$ $\equiv$ $t_1$
|
|
-\> ($\cdots$ -\> ($t_{n-1}$ -\> $t_n$))
|
|
|
|
|
|
There is one particular set of niladic type constructors that look like
|
|
numbers. These are used to represent certain "sizes". For example, the
|
|
type:
|
|
|
|
`Bit 16`
|
|
|
|
consists of the unary type constructor `Bit` applied to type represented
|
|
by the niladic type constructor "`16`". The type as a whole represents
|
|
bit vectors of length 16 bits. Similarly the type
|
|
|
|
`UInt 32`
|
|
|
|
|
|
represents the type of unsigned integers that can be represented in 32
|
|
bits. These numeric types are said to have kind `#`, rather than kind
|
|
`*` for value types.
|
|
|
|
|
|
Strings can also be used as type, having kind `$`. This is less common,
|
|
but string types are quite useful in the generics library, described in
|
|
the *Libraries Reference Guide*. Examples:
|
|
|
|
- `MetaData#("Prelude","Maybe",PrimUnit,2)`
|
|
- `MetaConsNamed#("Valid",1,1)`
|