bluespec-docs/content/chapter2/_index.md

104 lines
2.8 KiB
Markdown
Raw Normal View History

2025-02-12 20:54:12 +00:00
+++
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)`