[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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)
