部分型かインスタンスか

• 0 は Int のインスタンス
• Int は _ のインスタンス
• Int は Int 自身の部分型

関数適用時の型検査においては、ただの項や束縛変数が引数の型に合致するかどうかは「部分型検査」ではだめ。なぜなら、Int型を期待している引数に渡せるのは0や1であって、Int自身ではないから。だから、部分型関係ではなく「aはbのインスタンスか」という関係性が必要になる。一方で、自由変数の場合は部分型関係で大丈夫。

ある項が型tである事を期待するとき、「型tを表す値」が入ることを許容してはいけない。Int 型の引数に0や1ではなくIntを渡してはいけない。

レコード型（Dict）

• すべての$k = keys(T)$について
  • $T_k$が必須ならば、必須な$S_k$もしくは$S_{rest}$が存在し（$S_x$とする）、$S_x \leq T_k$
  • $T_k$がオプショナルならば、$S_k$もしくは$S_{rest}$が存在する時$S_x \leq T_k$
• かつ、$T_{rest}$が存在するならば
  • すべての$k = keys(S) - keys(T)$について、$S_k \leq T_{rest}$
  • かつ、$S_{rest}$が存在するならば、$S_{rest} \leq T_{rest}$

ボトム型

Glispが型付けを導入したい最大の動機は、

• 安全性: 不正な計算を事前に見抜きたい（通常の言語はこれ）
• VP（ビジュアルプログラミング）親和性: 型に合った適切な値を入力できるコントロールを表示したい
• エラープルーフ性: 一部の実行時エラーのせいでプロジェクト全体がプレビューできなくなる自体を防ぐ

「ボトム型はすべての型の部分型である」という定義に倣って、ボトム型とそれ以外の型との合併はボトムが無視される。（例: (| () Int) → Int）つまり、全ての関数がボトムを返し得る（=部分関数）し、それはHaskellでいうMaybe型のように返り値として明示する必要はない。この問題は何かというと、あらゆる値はどう型付けされようと、ボトムである可能性を排除できない為に、仮に型検証が済んでいるにしても実行時にその値がボトムかどうかをチェックし、必要あらば引数の型デフォルトに置き換えなくてはならないということ。