[ 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 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 <[email protected]> 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 >
