[TYPES] Translation of bounded quantifications into intersection types

Stephen Dolan stephen.dolan at cl.cam.ac.uk
Tue Dec 11 09:18:40 EST 2018


On Tue, 11 Dec 2018 at 08:30, Ningning Xie <xnningxie at gmail.com> 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


More information about the Types-list mailing list