123 \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})} |
123 \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})} |
124 {@{text S} \hookrightarrow (@{text xs}, @{text T})} |
124 {@{text S} \hookrightarrow (@{text xs}, @{text T})} |
125 \]\smallskip |
125 \]\smallskip |
126 |
126 |
127 \noindent |
127 \noindent |
128 which relates a type-scheme with a list of type-variables and a type. The point of this |
128 Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to |
129 definition is: given a type-scheme @{text S}, how to get access to the bound type-variables |
129 address the following problem: |
130 and the type-part of this type-scheme? The unbinding relation gives an answer, though in general |
130 Given a type-scheme @{text S}, how does one get access to the bound type-variables |
|
131 and the type-part of @{text S}? The unbinding relation gives an answer, though in general |
131 we will only get access to some type-variables and some type that are |
132 we will only get access to some type-variables and some type that are |
132 ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function |
133 ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function |
133 for alpha-equated type-schemes. |
134 for alpha-equated type-schemes. |
134 Still, with this |
135 Still, with this |
135 definition in place we can formally define when a type is an instance of a type-scheme as |
136 definition in place we can formally define when a type is an instance of a type-scheme |
|
137 as follows: |
136 |
138 |
137 \[ |
139 \[ |
138 @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"} |
140 @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"} |
139 \]\smallskip |
141 \]\smallskip |
140 |
142 |
141 \noindent |
143 \noindent |
142 meaning there exists a list of type-variables @{text xs} and a type @{text T'} to which |
144 This means there exists a list of type-variables @{text xs} and a type @{text T'} to which |
143 the type-scheme @{text S} unbinds, and there exists a substitution whose domain is |
145 the type-scheme @{text S} unbinds, and there exists a substitution whose domain is |
144 @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}. |
146 @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}. |
145 The problem with this definition is that we cannot follow the usual proofs |
147 The problem with this definition is that we cannot follow the usual proofs |
146 that are by induction on the type-part of the type-scheme (since it is under |
148 that are by induction on the type-part of the type-scheme (since it is under |
147 an existential quantifier and only an alpha-variant). The representation of |
149 an existential quantifier and only an alpha-variant). The representation of |