An extension of system \(F\) with subtyping (Q1322473): Difference between revisions

System \(F_ <\), which is presented here, combines subtyping with the parametric polymorphism of Girard's system \(F\). Partially inspired by the PER semantics, it is obviously sound for it (but not complete) and differs from Curien and Ghelli's system \(F_ \leq\) by the addition of a very natural equational rule (between terms of the same type). This rule improves in particular the categorical aspects of the system: for example the usual second-order encodings for products and coproducts are here true categorical constructs. For what concerns typing judgements, \(F_ <\) is equivalent to \(F_ \leq\) and is conservative over \(F\); wrt provable equality of terms, both fail and \(F_ <\) may equate simple \(\beta\eta\)-normal forms. The expressiveness of \(F_ <\) is demonstrated by a set of examples including records.