Coercions in a polymorphic type system

The idea of coercive subtyping, a theory of abbreviation for dependent type theories, is incorporated 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.

• Type: Journal
• Year: 2008
• Where: MSCS
• Authors: Zhaohui Luo
• Keywords: Corresponding Type Inference, Dependent Type Theories, MSCS 2008, Polymorphic Type