自由型変数
自由な型変数
定義
型
$ \tau
型スキーム
$ \sigma
型環境
$ \Gamma
がある時に、これらに含まれる自由型変数の集合をそれぞれ
$ FTV(\tau)
$ FTV(\sigma)
$ FTV(\Gamma)
で表す
/mrsekut-book-4781912850/160
例
$ FTV(a \to b) = \{a,b\}
a
,
b
は両方とも自由型変数
$ FTV(a.a \to b) = \{b\}
a. a -> b
は型スキーム
その内、
a
はスキーム化されており、これは自由型変数とは言わない
だから
a . a->b
の自由型変数は
b
のみ