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

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. Categories and Subject Descriptors D.3.3 [Language Constructs and Features]: Polymorphism General Terms Design, Reliability, Languages, Theory, Verification Keywords Type Inference, System F, Polymorphism, Type Reconst...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Didier Rémy
• Keywords: ICFP 2005, Keywords Type Inference, Polymorphism General Terms, Programming Languages, Type Annotations