New answers tagged pl.programming-languages
4
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}},*_{\...
4
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. (...
Top 50 recent answers are included
