Coercions in a polymorphic type system
Zhaohui Luo · Mathematical Structures in Computer Science · 2008
We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.