From ML to MLF: graphic type constraints with efficient type inference

MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent MLF types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features--Constraints; Polymorphism; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type structure; D.3.2 [Language Classifications]: Applicative (functional) languages General Terms Algorithms, Design, Languages, Theory Keywords System F, MLF...

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Boris Yakobowski, Didier Rémy
• Keywords: ICFP 2008, ML-style Type Inference, MLF Type Inference, Programming Languages, Type Inference