HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Simple, partial type-inference for System F based on type-containment

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.
Document type :
Conference papers
Complete list of metadata

Contributor : Didier Rémy Connect 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



  • HAL Id : inria-00000938, version 1



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⟩



Record views


Files downloads