[TYPES] Translation of bounded quantifications into intersection types

[Ningning Xie]

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 known to break subtyping relation for polymorphic types:

(∀ α ≤ Real . Bool → α)  ≤ (∀ α ≤ Int . Bool → α)

which translates to a non-derivable statement:

(∀ α . Bool → (α ∧ Real))  ≤ (∀ α . Bool → (α ∧ Int))


Thanks in advance for any pointers.


Best regards,
Ningning

On Mon, 10 Dec 2018 at 19:57, Ningning Xie <xnningxie at gmail.com> wrote:

> We have been working on an intersection type system.
>
> In the dissertation of Benjamin Pierce
> (https://www.cis.upenn.edu/~bcpierce/papers/thesis.pdf), Section 3.5.1
> and 7.9
> mentioned a rough idea of translating bounded quantifications (System
> F-sub)
> into intersection types.
>
> Wondering if there is any related work/formalization in this direction?
>
> Thanks in advance for pointers!
>
>
> Best regards,
> Ningning
>