[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Thu, 13 Dec 2018 at 06:33, Giuseppe Castagna <[email protected]> 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
