# Tag Info

6

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. ...

5

This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a Pure Type System in a quite simple way, using sorts $*_{\mathrm{mono}}$, $*_{\mathrm{poly}}$ and $\square$ along with the axioms $$*_{\mathrm{mono}}, *_{\mathrm{poly}}\ :\ \square$$ and the rules (*_{\mathrm{mono}},*_{\mathrm{mono}},*_{\...

5

Apart from what's already written in the slides you linked to, let me describe one possible approach. For studying type inference semantically we need a model in which a term can have many types, or none. This naturally leads to Curry-style typing, i.e., we think of $t : A$ as a relation where both the term $t$ and the type $A$ are meaningful by themselves. (...

3

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$. $\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the ...

Only top voted, non community-wiki answers of a minimum length are eligible