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

https://hal.inria.fr/inria-00000938
Contributor : Didier Rémy <>
Submitted on : Thursday, December 15, 2005 - 4:10:47 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on: : Friday, September 14, 2012 - 4:25:28 PM

Files

Identifiers

  • HAL Id : inria-00000938, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

126

Files downloads

403