People who code: we want your input. Take the Survey
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. (...


4

Use an auxiliary type of positive natural numbers. data positive : Set where one : positive s0 : positive → positive -- multiply by 2 s1 : positive → positive -- multiply by 2 and add 1 data N : Set where zero : N pos : positive → N Supplemental: Another option, which I found on my whiteboard today (probably put there by Egbert Rijke months ago)...


4

$\newcommand{\Alg}{\mathsf{Alg}\ }$ $\newcommand{\NatF}{\mathsf{NatF}\ }$ $\newcommand{\Nat}{\mathsf{Nat}}$ $\newcommand{\map}{\mathrm{map}\ }$ $\newcommand{\Z}{\mathrm{Z}}$ $\newcommand{\S}{\mathrm{S}}$ I don't think this is an actual counter-example. Parametricity implies: $$∀(α : \Alg \NatF t) (g : r → t)(x : \NatF r). \\ α\ [r]\ g\ x = α\ [t]\ (λx.x)\ (\...


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 ...


2

It is false that the only well-typed occurrence of Prf has to be of the form Prf(all ...). For example, in the context with a variable p : Prop we can form the type Prf(p) which is not of the stated form. Another possibility is that we have a Prf(t) for some closed term t : Prop which is not of the form all ... but it normalizes to it. The purpose of Prf is ...


1

Ali Asaf worked out a hierachy of universes with explicit coercions (lifting) in A calculus of constructions with explicit subtyping and established a relationship with cummulative universes.


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