bluespec-docs/content/chapter2/_index.md

+++ 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)