MLの空リストのタイプは何ですか？

Question

空リストのタイプがSML（私はPolyMLを使用しています）に何であるのでしょうか？ 私は通訳に[]を入力すると、私が出る：

val it = []: 'a list 

私が期待するものです。しかし、その後、私が入力した場合は言う：

fun f a = if a = 0 then [] else [[]]; 

が、私は得る：

val f = fn: int -> 'a list list 

[]はタイプ'a list listもを持っていることを意味すると思われました。これはどのくらい正確に機能しますか？

Answer 1

MLの用語では、値はタイプではなくタイプのスキームです。タイプスキームは、タイプの集合です。ワイルドカードを使用するタイプで、ワイルドカードは任意のタイプで置き換えることができます。ワイルドカードをタイプに置き換えることは、タイプスキームをインスタンス化すると呼ばれます。

'a listでは、'aはタイプ変数、つまりワイルドカードです。空リスト[]は、タイプスキーム'a listのインスタンスである任意のタイプで使用できます。つまり、すべてのタイプがTの場合、空のリストのタイプはT listです。たとえば、空のリストのタイプはint listで、タイプはbool listで、タイプは(int * int * int) listで、タイプはint list listです。これらのタイプはすべて、タイプスキーム'a listのインスタンスです。

変数が複数回発生する場合は、一貫して置き換える必要があります。たとえば、fn x => x（同一性関数）は、タイプスキーム'a -> 'aです。タイプint -> intとタイプbool -> boolですが、タイプはint -> boolではありません。タイプスキーム'a -> 'bの値は、タイプint -> boolでもあります。

値には複数の型があります。これはプログラミング言語の一般的な現象です。よくタイプされた値のタイプのセットが、タイプスキームのインスタンスのセットであることは、コアML言語のプロパティです。このプロパティはプリンシパルと呼ばれます.MLの型システムはプリンシパルです。 MLの具体的な実装は、公国に対する例外を持つ傾向があります。たとえば、SMLには演算子のオーバーロードによる例外があります（fn x => x + xにはint -> intとfloat -> floatの2種類があります）、オーバーロードの解決規則により、コンテキストにfloatがない場合、コンパイラはint -> intを決定します。

プリンシパルタイプスキームが少なくとも1つの変数を含む値は、多形と言われています。主体型スキームに変数が含まれていない値は、単相と言います。

ワイルドカードは、タイプスキームに置き換えることができます。これにより、元のコレクションのサブセットである別のタイプスキームが得られる。すなわち、タイプスキームは、オリジナルのより小さいタイプスキーム（精細化）である。たとえば、値[[]]は、タイプスキーム'a list listです。タイプの場合はタイプT list listです。[[]]はMLについての文献では

は、「タイプ」はしばしば「型スキーム」と交換可能に使用されるタイプint list listとタイプbool list listとタイプを(int * int * int) list listなどがあるので、それは空のリストが型を持っている「と言うのが普通です'a list "となります。タイプシステムに関する文献では、「タイプ」はしばしば、ML用語が「タイプスキーム」と呼ぶものを意味し、「グランドタイプ」などの他の用語は、変数のないタイプに使用される。