[TYPES] Translation of bounded quantifications into intersection types

[Stephen Dolan]

On Thu, 13 Dec 2018 at 06:33, Giuseppe Castagna <gc at irif.fr> wrote:

>
> If you are interested in prenex polymorphism then let me point out the
> paper
> "Set-theoretic Foundation of Parametric Polymorphism and Subtyping" in
> ICFP '11
> (by Castagna & Xu) for a type system with union, intersection, and
> negation types.
> There the subtyping relation is defined semantically: τ₁ ≤ τ₂ iff for all
> possible interpretations of the type variables the first type is
> interpreted in
> a subset of the second type. This in particular implies that for every
> type
> substitution σ, τ₁ ≤ τ₂ implies τ₁σ ≤ τ₂σ
>
> In this system not only you have
>
>      Bool → (α ∧ Real)  ≤  Bool → (α  ∧ Int)
>
> but since you have "true" unions and intersections you can encode more
> general
> bounded polymorphism of the form
>
> ∀ τ₁≤ α ≤ τ₂. τ
>
> as
>
> ∀ α . τ'
>
> where τ' is obtained from τ by replacing every occurrence of α by ((τ₁v α)
> ∧ τ₂)
>

I don't think it's necessary to have "true" unions and intersections here -
it's enough that types form a lattice.

Incidentally, under the definition of subtyping I described above, a
simpler encoding is possible: replacing positive occurrences of α with (τ₁
v α) and negative occurrences of α with (τ₂ ∧ α).


The system also shows new applications of bounded polymorphism when
> combined
> with negation types. For instance if you consider the function
>
> fun x = if (x∈Int) then "ok" else x
>
> then you want to give it the type
>
> ∀ α . (Int → String) ∧ (α\Int → α\Int)
>
> that is, the type of a function that when applied to an integer it returns
> a
> string and when applied to an argument of any type that is not an integer
> returns a result of the same type (here / is the set-theoretic difference,
> i.e.
> τ₁/τ₂ = τ₁ ∧ ¬τ₂). We can express this type in bounded polymorphism as
>
> ∀ α ≤ ¬Int. (Int → String) ∧ (α → α)
>
> Notice that this type is not weird. It is exactly the type of the
> "balance"
> function as defined by Okasaki for red-black trees in his book (you can
> find the
> annotated code in section 3.3 of our POPL 15 paper "Polymorphic Functions
> with
> Set-Theoretic Types: Part 2")
>
>
> Finally, if you want to play with this kind of types, you can use the
> development version of CDuce.
>
>    git clone https://gitlab.math.univ-paris-diderot.fr/cduce/cduce.git
>
> use the cduce-next branch. In particular in the toplevel you can use two
> debug
> directives:
>
>  > debug subtype τ₁ τ₂
>
> that checks whether two types are in the subtyping relation and
>
>  > debug tallying [ ] [τ₁ , τ₂ ; .... ; τ₁' , τ₂']
>
> that returns a set of solutions (type substitutions) for the set of
> constraints
> {τ₁≤τ₂ ; .... ; τ₁'≤τ₂'}
> (see #help debug for the syntax of debug directives and
> http://www.cduce.org/manual_types_patterns.html#syntax for the syntax of
> types)
>

Thanks for the reference!

Stephen