Re: [TYPES] type inference for mutually recursive algebraic types with subtyping

[ 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 compilation” by Ohori (TOPLAS 
1995), though it doesn’t discuss recursive types. A more recent one is 
“Extensible programming with first-class cases” by Blume, Acar, and Chae (ICFP 
2006).

These works, however, do not have true subtyping but use unification with a 
notion of kinding for type variables (Ohori) or row variables (Blume et al.).

In our work at ICFP 2016 ("Set-theoretic types for polymorphic variants” by 
Castagna, Petrucciani, and Nguyen) we have described type inference for a type 
system with polymorphic variant types, union types, and recursive types, with 
subtyping based on the “semantic subtyping” approach.

A revised version of that type inference system will be described in Tommaso 
Petrucciani’s forthcoming PhD thesis (it is currently in the hands of the 
reviewers, but I can send you a copy via PM if you wish). This is a major 
revision of our ICFP paper. In particular the proof of completeness there was 
not correct, and the thesis addresses this issue (by using techniques introduced 
in Dolan's thesis already cited in previous messages) and provides a more robust 
solution.

Cheers

Beppe