dale@LINC.CIS.UPENN.EDU (Dale Miller) (03/07/87)
Math/CS Logic Seminar Filter Model of Types for Flexible Programming Atsushi Ohori (ohori@cis.upenn.edu) CIS Dept, Univ of Penn 16 March 1987 In this talk, I will present a mathematical model of data types for flexible programming. This model can give precise semantics to (1) polymorphic types, (2) type inheritance used in object-oriented programming, (3) parametric types, (4) dependent types, (5) recursive types and (6) higher-order types. I will also discuss some connections to ``formulae-as-types'' principle. We consider types as properties of values and define the semantics of types as the sets of values having those properties. This idea leads us to define types as principal filters in the underlying value domain (in the sense of Scott.) Since principal filters are represented by their minimal elements, types are represented by values. Simple type constructors are then correspond to operations on the value domain. The polymorphic type constructor corresponds to the least upper bound operation. Parametric types and dependent types are represented by functions on the value domain. Since the set of all principal filters is isomorphic to the underlying value domain, the semantic space of types is isomorphic to the value domain. This property allows us to give semantics to arbitrarily higher-order types without any inconsistencies. [Talk will be in Math Seminar Room, 4th floor DRL.]