Abstract

In this talk I will show how to combine disjoint polymorphism with BCD subtyping, culminating in a very expressive calculus named Fi+. The combination is non-trivial and highly challenging in terms of coherence proof. I will then show how to adapt the proof technique in the polymorphic setting. Finally I will present a simple application of generic object algebra combinators.