People who code: we want your input. Take the Survey

# Tag Info

## Hot answers tagged type-systems

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