Inferring types for functional methods (where method calls come for free)

Luigi Liquori (1) , Arnaud Spiwack (2)

1 KAIROS - Logical Time for Formal Embedded System Design
2 PI.R2 - Design, study and implementation of languages for proofs and programs

This paper introduces a functional calculus, called OhML that features objects and message sending via functional application. A sound (message-not-found preventing) first-order type system featuring width subtyping is presented. The paper presents also a sound and complete type inference algorithm that calculates a principal constrained type or fails.

Mots clés: functions; polymorphic-type inference; objects

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]; Informatique et langage [cs.CL]

Luigi Liquori, Arnaud Spiwack. Inferring types for functional methods (where method calls come for free). 2004. ⟨hal-01149745⟩