[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
My references are a little bit outdated but you can check:
Basic category theory for computer scientists
by Benjamin C. Pierce
Categories, Types, and Structures: An Introduction to Category Theory
for the Working
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
An older work in which you have a limited form of intersection types is:
G. Castagna and G. Chen: Dependent types with subtyping and late-bound
overloading. Information and Computation, vol. 168, n. 1, pag. 1-67,
[ 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
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The work on extensible sum types (e.g. like the polymorphic variants of OCaml)
could be interesting for you if you don’t know about it already. A notable work
on this is “A polymorphic record calculus and its
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In our ICFP 16 Paper /Set-Theoretic Types for Polymorphic Variants /we
defined type inference for polymorphic variants with recursive
set-theoretic types (type are defined coinductively with a couple of
standard
