------------------------------------------------------------------------------- B O S T O N U N I V E R S I T Y Computer Science Department C O L L O Q U I U M Wednesday November 15, 1995 3:00pm (Coffee served at 2:45pm) Seminar Room / MCS 135 ------------------------------------------------------------------------------- Type Inference Without Principal Types Trevor Jim Laboratory for Computer Science Mass Institute of Technology Most type inference algorithms use a ``divide and conquer'' strategy in which the type of the whole program is constructed from the types of its parts. This strategy relies critically on a notion of PRINCIPAL TYPE, which guarantees that the type inferred for each part represents ALL POSSIBLE types for the part. The type of the whole can then be constructed from the principal types of the parts by a constraint-solving procedure, such as UNIFICATION. Many type systems do not have a general notion of principal type, preventing use of this strategy. In this talk, we demonstrate that a limited notion of principal types may be sufficient to perform type inference in such languages. Our case study is System F, the polymorphic lambda calculus, extended by Mitchell's subtyping relation. We define a limited notion of principal types, and use it to reduce type inference to a generalized unification problem. Furthermore, we show how to reduce the unification problem to a subtyping problem. Host: Assaf Kfoury ------------------------------------------------------------------------------- For colloquium info, including directions, see http://cs-www.bu.edu/colloquium For more information contact Prof. Mark Crovella -------------------------------------------------------------------------------