Abstract : We explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified via type annotations on source terms. We allow implicit predicative type-containment and explicit impredicative type-instantiation. We obtain a core language that is both as expressive as System F and conservative over ML. Its type system has a simple logical specification and a partial type-reconstruction algorithm that are both very close to the ones for ML. We then propose a surface language where some annotations may be omitted and rebuilt by some algorithmically defined but logically incomplete elaboration mechanism.
https://hal.inria.fr/inria-00000938 Contributor : Didier RémyConnect in order to contact the contributor Submitted on : Thursday, December 15, 2005 - 4:10:47 PM Last modification on : Friday, February 4, 2022 - 3:10:22 AM Long-term archiving on: : Friday, September 14, 2012 - 4:25:28 PM
Didier Rémy. Simple, partial type-inference for System F based on type-containment. Proceedings of the tenth International Conference on Functional Programming, Sep 2005, Tallinn, Estonia. ⟨inria-00000938⟩