プログラミング言語SML#解説 3.7.1版

Chapter 18 型

本節では，型の構文およびSML#コンパイラに組み込まれている型を定義する．

型は，単相型( $\,\langle$ ty $\rangle\,$ )と多相型( $\,\langle$ polyTy $\rangle\,$ )に分類される．単相型の集合は，以下の文法であたえあれる．

$\,\langle$ ty $\rangle\,$	::=	$\,\langle$ tyvar $\rangle\,$	型変数名
	$\|$	{ $($ $\,\langle$ tyrow $\rangle\,$ $)?$ }	レコード型
	$\|$	$\,\langle$ ty ${}_{1}$ $\rangle\,$ * $\cdots$ * $\,\langle$ ty ${}_{n}$ $\rangle\,$	組型( $n\geq 2$ )
	$\|$	$\,\langle$ ty $\rangle\,$ -> $\,\langle$ ty $\rangle\,$	関数型
	$\|$	$($ $\,\langle$ tySeq $\rangle\,$ $)?$ $\,\langle$ longTycon $\rangle\,$	(パラメタ付)きデータ型
	$\|$	( $\,\langle$ ty $\rangle\,$ )
$\,\langle$ tyrow $\rangle\,$	::=	$\,\langle$ lab $\rangle\,$ : $\,\langle$ ty $\rangle\,$ $($ , $\,\langle$ tyrow $\rangle\,$ $)?$	レコードフィールドの型

$\,\langle$ tyvar $\rangle\,$ は，型の集合を動く変数である．第17.2節で定義した通り’a，’fooおよび ’’a，’’fooのように表記される．後者は同値プリミティブ演算が適用可能なeq型に限定された型変数である． eq型は，関数型とeq型ではない組み込み型（real, real32, exn）を含まない任意の型である．ユーザ定義のデータ型も，その定義に含まれる型がすべてeq型であればeq型である．従って，例えば以下のように定義される $\tau$ listは引数の型 $\tau$ がeq型であればeq型である．

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

関数型構成子->はラムダ計算の伝統に従い右結合する．したがって，int -> int -> intと記述すると，int -> (int -> int)と解釈される．

$\,\langle$ longTycon $\rangle\,$ は，datatype宣言で定義される型構成子の名前であり，宣言されたstructureのパス名で修飾される． int型等の基底型はパラメタ $\,\langle$ tySeq $\rangle\,$ を持たないデータ型である． SML#3.7.1には以下の基底型およびデータ型構成子が組み込まれている．

型構成子名	説明	eq型？
int	32ビット符号付き整数	Yes
int64	64ビット符号付き整数	Yes
int16	16ビット符号付き整数	Yes
int8	8ビット符号付き整数	Yes
intInf	桁数制限のない符号付き整数	Yes
word	32ビット符号なし整数	Yes
word64	64ビット符号なし整数	Yes
word16	16ビット符号なし整数	Yes
word8	8ビット符号なし整数	Yes
real	浮動小数点数	No
real32	32ビット浮動小数点数	No
char	文字	Yes
string	文字列	Yes
exn	例外	No
unit	ユニット値(())	Yes
$\tau$ ref	参照（ポインタ）	Yes
$\tau$ array	配列	Yes
$\tau$ vector	ベクトル	$\tau$ がeq型ならばYes

ユニット値の型unitと空のレコード型{}は異なる型として区別される．これはStandard MLに対する後方互換性の無い変更点である．

多相型の集合は以下の文法で与えられる．

$\,\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\,$ ]は，束縛型変数 $\,\langle$ boundtyvarList $\rangle\,$ のスコープが明示された多相型である．
•

束縛型変数は，その取りうる型の集合を制限する以下のカインド制約 $\,\langle$ kind $\rangle\,$ をつけることができる．レコードカインド#{ $\,\langle$ tyrow $\rangle\,$ }は， $\,\langle$ tyrow $\rangle\,$ が表すフィールドを含むレコード型に制限する． boxedカインドはヒープにアロケートされる値の型に制限する． unboxedカインドはヒープにアロケートされない値の型に制限する． eqカインドは eq型に制限する． reifyカインドは型のリーフィケーション機能を用いることの注釈であり，型変数が動く範囲を制限しない．

この集合は，Standard MLの多相型をレコード多相性およびランク１多相に拡張したものである．例えば，以下のような多相型を持つ関数が定義できる．

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

対話セッションでは，上記のカインドに加えて，オーバロードカインド:: { $\,\langle$ tyList $\rangle\,$ }がプリントされることがある．これは，型変数が動く範囲をインスタンス型 $\,\langle$ tyList $\rangle\,$ のいずれかに制限するカインドである．現在，オーバーローディングはシステム定義のプリミティブのみに限定されており，オーバーロードカインドをもつ多相型をユーザプログラムが指定することはできない．