[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Tue, 11 Dec 2018 at 08:30, Ningning Xie <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > To give more context, I am referring to the encoding: > > ∀ α ≤ τ₁. τ₂ ≜ ∀ α. τ₂ [α ↦ τ₁ ∧ α ]. > > (where in the rhs α is substituted by the intersection type (τ₁ ∧ α)). > > For example, we could have > > ∀ α ≤ Nat . α → Bool ≜ ∀ α. (Nat ∧ α) → Bool > This encoding is used in my thesis on type inference with subtyping, available at: https://www.cl.cam.ac.uk/~sd601/thesis.pdf (Technically, my ⊓ is not a standard intersection type but just a meet in the lattice of types, but this encoding is the same) This encoding is known to break subtyping relation for polymorphic types: > > (∀ α ≤ Real . Bool → α) ≤ (∀ α ≤ Int . Bool → α) > > which translates to a non-derivable statement: > > (∀ α . Bool → (α ∧ Real)) ≤ (∀ α . Bool → (α ∧ Int)) > This is only the case if your definition of subtyping between two polymorphic types requires one to be a subtype of the other for any given α. (This is indeed the definition used by Pierce and used in F≤). However, this is not the definition of subtyping between polymorphic types used in e.g. ML (the relation between type schemes of one being "at least as polymorphic as the other"), because in ML these type schemes are equivalent: ∀α ∀β. α → β → α ∀α ∀β. β → α → β For given α, β, these yield different types and are not related by the F≤ subtyping relation. Yet they have the same set of instances: all types of the form τ → σ → τ (and their supertypes). This suggests a different definition of subtyping between polymorphic types: one polymorphic type is a subtype of another if the first has more instances. Equivalently, one polymorphic type is a subtype of another if for every instance of the second, there is an instance of the first which is a subtype. I first came across this idea in François Pottier's thesis, available at https://hal.inria.fr/inria-00073205, where he calls it "scheme subsumption". He cites a paper, "Subtyping Constrained Types" (Valery Trifonov and Scott Smith) as the origin of the idea. Under this definition of subtyping, the statement above does actually hold: (∀ α . Bool → (α ∧ Real)) ≤ (∀ β . Bool → (β ∧ Int)) because for any β, we can choose α = β ∧ Int to make the above true. In fact, we can go further than the encoding you mentioned. It turns out that in general it is only necessary to replace the negative occurrences of a type variable with meets / intersections, making the following types equivalent: ∀ α ≤ τ. α → α ∀ α. (α ∧ τ) → α This encoding is used in my thesis as one of the main ingredients of the "biunification" algorithm, and Sections 5.2, 5.3 have more detail about it. Regards, Stephen
