[TYPES] Translation of bounded quantifications into intersection types

[Giuseppe Castagna]

On 12/11/18 3:18 PM, Stephen Dolan wrote:
>  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. 

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 α) ∧ τ₂)

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)