Bounded existentials and minimal typing (Q1127527): Difference between revisions

\(F_\leq\) is a typed lambda-calculus combining subtyping and second-order bounded quantification. It is shown that in the system obtained by adding (as primitive) bounded existential quantification the minimal type property fails. It is also shown that when the system is restricted to ``equal bounds'' (the introduction rules are of the form: If \(A\leq S\vdash T\leq U\) then \(\vdash\text{All } (A\leq S)T\leq\text{All } (A\leq S)U)\), then the minimal types do exist and an algorithm to get them is given.