Chapter 18 Types

This chapter defines the syntax for types and describes the built-in types.

Types are divided into monotypes ( $\,\langle$ ty $\rangle\,$ ) and polytypes( $\,\langle$ polyTy $\rangle\,$ ). The syntax for mono types are given below.

$\,\langle$ ty $\rangle\,$	::=	$\,\langle$ tyvar $\rangle\,$	type variable names
	$\|$	{ $($ $\,\langle$ tyrow $\rangle\,$ $)?$ }	record types
	$\|$	$\,\langle$ ty ${}_{1}$ $\rangle\,$ * $\cdots$ * $\,\langle$ ty ${}_{n}$ $\rangle\,$	tuple types ( $n\geq 2$ )
	$\|$	$\,\langle$ ty $\rangle\,$ -> $\,\langle$ ty $\rangle\,$	function types
	$\|$	$($ $\,\langle$ tySeq $\rangle\,$ $)?$ $\,\langle$ longTycon $\rangle\,$	(parameterlized) datatypes
	$\|$	( $\,\langle$ ty $\rangle\,$ )
$\,\langle$ tyrow $\rangle\,$	::=	$\,\langle$ lab $\rangle\,$ : $\,\langle$ ty $\rangle\,$ $($ , $\,\langle$ tyrow $\rangle\,$ $)?$	record field types

$\,\langle$ tyvar $\rangle\,$ are type variable names. As defined in Section 17.2, they are written as ’a，’foo or ’’a，’’foo. The latter form are for those equality type variables, which range only over types that admit equality. An type admits equality, called eqtype, is any type that does not contain function type constructor and built-in types that does not admit equality. A user defined datatype is an eqtype if it only contains eqtypes. For example, $\tau$ list defined below is an eqtype if $\tau$ is an eqtype.

datatype ’a list = nil | :: of ’a * ’a list

The function type constructor -> associates to the right so that int -> int -> int is interpreted as int -> (int -> int).

$\,\langle$ longTycon $\rangle\,$ is a type constructor names defined by datatype declarations. Atomic types such as int are type constructors without type parameters ( $\,\langle$ tySeq $\rangle\,$ ). SML#3.7.1 supports the following built-in atomic types and type constructors.

type constructor name	description	eqtype?
int	32 bit long signed integers	Yes
int64	64 bit long signed integers	Yes
int16	16 bit long signed integers	Yes
int8	8 bit long signed integers	Yes
intInf	unbounded signed integers	Yes
word	32 bit long unsigned integers	Yes
word64	64 bit long unsigned integers	Yes
word16	8 bit long unsigned integers	Yes
word8	8 bit long unsigned integers	Yes
real	floating point numbers)	No
real32	32 floating point numbers	No
char	characters	Yes
string	strings	Yes
exn	exceptions	No
unit	unit values (())	Yes
$\tau$ ref	references (pointers)	Yes
$\tau$ array	arrays	Yes
$\tau$ vector	vectors	$\tau$ がeq型ならばYes

The unit type is distinguished from the empty record type {} as a different type. This is the modification that is not backward-compatible to Standard ML.

The syntax for polytypes ( $\,\langle$ polyTy $\rangle\,$ ) are given below.

$\,\langle$ polyTy $\rangle\,$	::=	$\,\langle$ ty $\rangle\,$
	$\|$	[ $\,\langle$ boundtyvarList $\rangle\,$ . $\,\langle$ ty $\rangle\,$ ]
	$\|$	$\,\langle$ ty $\rangle\,$ -> $\,\langle$ polyTy $\rangle\,$
	$\|$	$\,\langle$ polyTy $\rangle\,$ * $\cdots$ * $\,\langle$ polyTy $\rangle\,$
	$\|$	{ $($ $\,\langle$ polyTyrow $\rangle\,$ $)?$ }
$\,\langle$ boundtyvarList $\rangle\,$	::=	$\,\langle$ boundtyvar $\rangle\,$ $($ , $\,\langle$ boundtyvarList $\rangle\,$ $)?$
$\,\langle$ boundtyvar $\rangle\,$	::=	$\,\langle$ tyvar $\rangle\,$ $\,\langle$ kind $\rangle\,$
$\,\langle$ kind $\rangle\,$	::=
	$\|$	#{ $\,\langle$ tyrow $\rangle\,$ }
	$\|$	# $\,\langle$ kindName $\rangle\,$ $\,\langle$ kind $\rangle\,$
$\,\langle$ kindName $\rangle\,$	::=	boxed $\|$ unboxed $\|$ reify $\|$ eq
$\,\langle$ polyTyrow $\rangle\,$	::=	$\,\langle$ lab $\rangle\,$ : $\,\langle$ polyTy $\rangle\,$ $($ , $\,\langle$ polyTyrow $\rangle\,$ $)?$

•

[ $\,\langle$ boundtyvarList $\rangle\,$ . $\,\langle$ ty $\rangle\,$ ] is the polymorphic type that makes the scope of bounded type variables $\,\langle$ boundtyvarList $\rangle\,$ explicitly.
•

A bound type variable may have the following kind constraints $\,\langle$ kind $\rangle\,$ . The record kind #{ $\,\langle$ tyrow $\rangle\,$ } restricts the range of the bound type variable to record types that have at least fields indicated by $\,\langle$ tyrow $\rangle\,$ . The boxed kind restricts it to the type of heap-allocated values. The unboxed kind is the complement of the boxed kind. The eq kind restricts it to eqtypes. The reify kind is just an annotation that the type reification feature is required and therefore does not restrict the range of the bound type variable.

The set of polytypes is the extension of the set of polytypes in the definition of Standard ML with record polymorphism, overloading and rank-1 polymorphism.

The following examples use a rank-1 polytype.

# fn x => (fn y => (x,y), nil);
val it = fn : [’a. ’a -> [’b. ’b -> ’a * ’b] * [’b. ’b list]]

In the interactive session, in addition to the above kinds, you may see the overload kind :: { $\,\langle$ tyList $\rangle\,$ }, which restricts the range of the bound type variable to $\,\langle$ tyList $\rangle\,$ . The current system restricts overloading to system defined primitives, and type variables with overload kind are not allowed in a user program.