Polymorphism, etc. -- Making Safety More Flexible

Analysis Requirements & Principles architecture:
Paradigms		 substance:
Abstractions		 structure:
Domains 		building blocks: Features surface:
Syntactics		 Defining PLs Language
List
foundational safety flexibilized

  1. Research Directions for More Flexible Type Systems
  2. Type Systems Feature Table
  3. Types: Polymorphism and Opaque Types

 
This page looks at type systems from the perspective of typing expressions to ensure execution properties, not on how to define & construct type terms and the values of a type. Adding only this aspect of a type system to a language does not allow to define new computations; in the contrary, it serves to exclude some dubious computations.

If you know further references, please don't hesitate to tell me (Ulf Schünemann), likewise if you have any suggestions.

[DTT] Gilles Barthe: Dependent Type Theory; preliminary lecture notes for APPSEM'2000.
[ITBP] Benjamin C Pierce: Intersection Types and Bounded Polymorphism; Math Struct in Comp Sci 11; Cambr Univ Pr 1996.
[HOS] Martin Steffen, Benjamin Pierce: Higher-Order Subtyping; TR ECS-LFCS-94-280; Univ Edinburgh 1994.
[PLCS] Kim Mens: An Introduction to Polymorphic Lambda Calculus with Subtyping; 1994.
[PolyP] PolyP - an extension of Haskell
[TCFD] Mark P Jones: Type Classes with Functional Dependencies; ESOP'2000; LNCS 1782.
[TMTC] Dominic Duggan, John Ophel: Type-checking multi-parameter type classes; 133-158 in JFP 12(2); Cambridge Univ Press, March 2002.

Research Directions for More Flexible Type Systems

< this colored table is optimized for Netscape 4.77 & 6.1 >
IMPREDICATIVE POLYMORPHISM
Generic/polytypic/ parametrically-overloaded functions are first class functions

Type schemes denote the generic intersection type - the intersection of types in the scheme-generated family:
all t.T : TYPE
[[all t.T]] = a:TYPE [[ T[t/a] ]]
(or with a:TYCON, or with bounds ...)

PREDICATIVE POLYMORPHISM
(syntactic sugar?)
Generic/polytypic/ parametrically-overloaded functions have (implicit) type (constructor) parameters which need to be fixed statically before they can be applied, ie. they are mappings TYPE+ -> FUNCTION (or TYCON+ -> FUNCTION, or with bounds)

Type schemes denote mappings from type (constructor) parameters to types:
all t.T : TYPE+ -> TYPE
[[all t.T]] = a:TYPE.[[ T[t/a] ]] or
(or with TYCON instead of TYPE, or with bounds ...)

How to type polytypic functions?

«A polytypic function is a function that is defined by induction on the structure of user-defined datatypes» [PolyP]:

size :: Regular d => d a -> Int
A generalisation of length on lists. Counts the number of elements of type a in a structure of type d a.
pmap :: Regular d => (a->b) -> d a -> d b
A generalisation to all regular datatypes of the normal map on lists . Applies a function to all elements in a structure.
cata :: Regular d => ((FunctorOf d) a b -> b) -> d a -> b
A generalised fold. The catamorphism is a general recursion operator that replaces datatype constructors with supplied functions.
(+) Reuse: «A number of functions have to be written over and over again on different datatypes. Examples of such functions are pretty printers, parsers, equality functions, most general unifiers, pattern matchers, rewriting functions, etc. These functions are examples of so-called polytypic functions» [PolyP]
intersection types
t1 & t2 : TYPE
[[t1 & t2]] = [[t1]] [[t2]]
The least common structural supertype of t1 and t2 is their intersection

(+) structurally transparent

  • use directly: all t<Student & Employee. List[t] -> List[t] [ITBP]
  • define type alias: interface H = { A, B, C } - called halotype [FCCA]
    		• Write their types as a type scheme all t.T which represent a family of types generated from it:
    1. Type abstraction is used to create the scheme from a type expression where t stands for a type. The scheme represents the types generated from it by substituting (universal, type-class bounded, subtype bounded, or F-bounded) types for t in T (type quantification).
    2. Type constructor abstraction is used to create the scheme from a type expression where t stands for a type constructor. The scheme represents the types generated from it by substituting (universal, or type-constructor-class bounded) type constructors for t in T (type constructor quantification).
    Generic functions, polytypic functions, and parametrically overloaded functions are used the same way, so they can be typed by the same kind of external type.
    IMPREDICATIVE OVERLOADING
    (dynamic overloading)
    Ad-hoc overloaded functions are first class functions (cf. [OOPUA])

    The combined type is a type, denoting the intersection of the types of the overloaded function's branches.

    		How to type parametrically overloaded functions?
    PARAMETERIZATION abstraction [<]:
    PARAMETRIC POLYMORPHISM

    How to type generic functions?
    (cf. type-oriented programming)
    AGGREGATION
    abstraction [<]:
    AD-HOC
    POLY-
    MORPHISM

    How to type
    ad-hoc
    overloaded
    functions    ,
    (a function f "with several types" t1, t2, etc.)     		BASIC TYPE SYSTEM
    each t:TYPE is a subset of VALUE     		direction of
    DEPENDENT TYPES
    PREDICATIVE
    OVERLOADING
    (syntactic sugar)
    In order to obtain a first-class (applicable) function, one branch of the overloaded function is chosen depending on the static context
  • type assignment is a relation (f : t1 and f : t2)
  • type f by t1 & t2 which denotes the set {t1, t2} of types
    • GENERALIZATION abstraction [<]:
    INCLUSION
    POLYMORPHISM

    How to model subclassing
    (how to type this)?
    1. subtyping
    2. hash-types
    CLASSIFICATION abstraction [<]:
    HIGHER-ORDER TYPES
    How to type existing types/type-constructors
  • for bounding the quantification of parametrically-overloaded / generic / polytypic functions
  • to type first-class type-values
    • type-classes (single parameter type predicates): each k:TYCL is a subset of TYPE

    1. to associate 1-parametrically overloaded functions [TMTC] with all types in a class

      Eg. in Haskell the iseq operation is overloaded for all types of class Eq [TCFD]:
      class Eq a where iseq :: a -> a -> Bool

      An existing type, like Bool is added explicitly and separately to a declared type-class, and its branch of the overloaded function has to be defined:
      instance Eq Bool where iseq x y = if x then y else not y

      Then iseq can be used to define the generic function neq on values of any type a from class Eq:
      neq x y = not(iseq x y).

    1. as bounds of type quantification
      eg. in type(scheme)s of parametrically overloaded and generic functions:
      iseq :: Eq a => a -> a -> Bool
      neq :: Eq a => a -> a -> Bool

    		type-constructor-classes
    each kk:TYCCL is a subset of TYCON
    generic type-classes instances (possibly type-class bounded)

    Eg. for any two types a and b belonging to Eq, also the tuple-type (a,b) belongs to Eq:
    instance Eq a, Eq b
    => Eq (a,b)
      where iseq (x,y) (a,b) =
        iseq x a && iseq y b

    		type relations ("multi-parameter type-classes")
    1. between parameter and result types of n-parametrically overloaded functions:
      Eg. multi-sorted algebraic operation [Cormack & Wright 1990], mixed-mode arithmetic operation [TMTC]:
      class HasPlus a b c where (+)::a->b->c
      Eg. record field selector [Peyton-Jones 1992] (from [TMTC])
      class HasName a b where name::a->b
      date Employee = EMPL String String Int
      instance HasName Employee String
        where name(x,y,z) = x
    2. between types of elements and types of the (not necessarily generic) matching collections [TCFD]
      class Collects e ce where
        empty :: ce
        insert :: e -> ce -> ce
    3. for monad transformers [Linang etal. 1995] (from [TMTC])
      class (Monad b, Monad (a b))
        => Monad a b where ...

    (-) Expresses only arbitrary relationships between the two type parameters. Hence, type inference will accept, if it cannot concretize the type a container, the use of a (monomorphic) container as Collects Bool ce and as Collects Char ce [TCFD].

    		type/type-constructor relations 
    class Collects e c where
  empty  :: c e
  insert :: e -> c e -> c e

    (-) Works only with generic collection types [TCFD].

    functional type relations (type-classes with functional dependencies between type parameters) [TCFD]. Eg. ce uniquely determines e: 
    class Collects e ce | ce ~> e where ...

    (+) allows to express partial 1:1 mappings between types (class E a b | a ~> b, b ~> a where ...), and combined dependencies, eg. to type arithm. ops. mixing int and floats: 

    class Mul a b c | (a,b) ~> c where
  (*) :: a -> b -> c
instance Mul Int Int Int where ...
instance Mul Int Float Float where ...
...

    Dimensions of Type Systems (in Type System Theory)

    The simply typed lambda calculus with its function types (F) has been extended to support various combinations of types for polymorphic values (P), higher-order types (H), and dependent types (D). Barendregt's lambda-cube [DTT] shows these extensions as 3 dimensions of type system development. In the Pure Type System framework [DTT], these type systems are characterized by whether and how they relate
    - type expressions (first-class types) like T, and Tx (where x occurs as free value identifier).
    - generic type schemes (second-class types); let Gt by a type or generic type where t occurs as free type identifier.
    - metatype expressions (aka kinds, type-classes, types of types) like M, and Mt (where t occurs as free type identifier).
     
    Functions (F)
    Polymorphism (P)
    Higher-Order (H)
    Dependent (D)
    impredicative
    (polymorphic types)     		predicative
    (type schemes)
    has as type type type scheme metatype metatype
    something like x:T' => Tx t:M' => Tt t:M' => Gt t:M' => Mt x:T' => Mx
    alternative syntax examples
    - no bounds:
    		T' -> T
    (not using x)     		a -> a, or
    template<class a> a& id(a&);     		Eq ?
    - with bounds:
    		Eq a => (a, a) -> bool ? int[0..x] (in context of some x:nat),
    template<int x> int len(int (&)[x]);
    for typing, e.g. value-parameterized
    values, i.e. functions
    type-parameterized values,
    esp. polymoprhic functions
    		type-parameterized types value-parameterized types,
    esp. arrays of unknown fixed length
    cf. the Type Systems Feature Table [    >]

    Type Systems Feature Table

    Type system in research, their features & their combinations, in historic order (where known)
     
    Polymorphism
    Higher-Order
    Subtypes
    Intersection
    types
    Union
    types
    Dependent
    Results
    untyped LC [Church 1930s]
    with term abstraction and application
    simply typed LC (function types) [Church 1940] (according to [HOS])
    Fomega with higher-order types 'kinds' ('*' for types, 'K -> K' for type operators), and with types, type constructors, constructors of type constructors and so on as first class citizens (according to [PLCS]) by [Girard's dissertation 1972] (according to [DTT]) +
    F2
    The 2nd order polymorphic LC
    with type abstraction and application [Girard's dissertation 1972, Reynolds 1974]     		universal (impredicative)
    in ML [Milner 1978] universal (predicative)
    intersection types by Coppo & Dezani-Ciancaglini (1978), Sallé [Coppo etal 1979, Sallé 1982], and Pottinger (1980) (according to [ITBP]) finite equivalence between rank 2 fragments of System F and rank 2 intersection system [Hirofumi Yokouchi: Embedding a Second-Order Type System into an Intersection Type System; 206-220: Information and Computation 117, 1995]
    < Cardelli's first-order calculus of subtyping (1984) +
    F<
    The now standard formulation of the subtype-bounded 2nd-order LC (the 2nd order fragment of Fomega<) by Curien & Ghelli (1992) based on Bruce & Longo's (1990) simplification and slightly generalization of Cardelli & Wegner's original language Fun [UTDAP 1985] (according to [ITBP])     		subtype bounded (impredicative) + type checking undecidable,
    but there are decidable variants
    (cf. below)
    F-bounded polymorphism explains compatibility between subclasses and baseclasses, allows typing self [Canning etal's 1989, Cook etal. 1990] F-bounded
    Fomega< - in it objects can be encoded and the interaction between subclassing and object encapsulation can be modeled
    [Cardelli 1990, Mitcehell 1990, Bruce & Mitchell 1992].
    Semantic model with PERs [Cardellig & Longo 1991]     		subtype bounded + +
    infinite intersection types Leivant 1990 (according to [ITBP]) infinite
    union types (as duals of intersection types) in 1991 by Barbanera & Dezani-Ciancaglini, by Hayashi, by Pierce (according to [ITBP]) +
    F/\ = /\ F< (2nd order)
    [B Pierce: Programming with Intersection Types and Bounded Polymorphism; PhD thesis; 1991]     		subtype bounded + finite
    Fomega/\
    [Compagnoni & Pierce 1993, Adriana B Compagnoni, Benjamin C Pierce: Higher-Order Intersection Types and Multiple Inheritance; Math Struct in Comp Sci 11; Cambr Univ Pr 1995]     		subtype bounded + + finite
    Calculus of constructions
    (Coquand & Huet)     		+ / - + +
    (Longo & Moggi) + / - +
    XML (Harper & Mitchell) - / + [typo in DTT?] + [typo in DTT?]
    Lambda omega [DTT] +
    Lambda P omega [DTT] + +
    in Automath, Elf +
    «Beginning with the influential paper, [CW85=Cardelli & Wegner's UTDAP 1985], there has been a great deal of interest in using various extensions of F<, the bounded second-order lamba calculus, as a basis for a theoretical understanding of object-oriented languages. ...
    Pierce [B Pierce: Bounded quantification is undecidable; POPL'92], proved that the problem of determining whether one type was a subtype of another is undecidable and hence so is the problem of type-checking terms of F<» [K Bruce, et al: Safe and deciable type checking in an object-oriented language; OOPSLA'93].
    Tiuryn & Urzyczyn (at LICS'96) show generally the undecidability of type inference for the combination of subtyping, parametric polymorphism and second-order types (with function types).
    «Decidable variants of F< have been proposed [CW85, KS92, CP94]» [HOS].

    Types: Polymorphism and Opaque Types

    Feature Description Argument
    Dot-notation vs. open-construct
    for using modules with opaque/existential types

    [ATDN] Luca Cardelli and Xavier Leroy: Abstract Types and the Dot Notation; DEC/SRC Research Report 56, 1990.

    		Algebra complex implementing the signature of complex numbers (see ADT) could be used by clients in two ways: 
    -- open construct
open complex as {C; cmk,cre,cim,cmul};
function csqr(x:C) = cmul(x,x);
return cre(csqr(cmk(2,3)));
    		(+) No problem with algebras being first class values.
    (-) Cannot return complex numbers from a locally opened algebra, instead the scope of open must encompass all places among which complex numbers should be exchanged. 
    -- dot notation
function csqr(x:complex.C) = complex.mul(x,x);
return complex.re(csqr(complex.make(2,3)));
    Note that complex.C is a type term containing an algebra term.     		(-) By making algebras full values, type checking will inherit undecidability from value terms (is complex.C always the same type?, is a.C = b.C?).
    (+) Ok to have algebra terms without type variables, e.g. nested algebras (alg1.alg2.C), and algebras parameterized by algebras (matrix(cartesian) vs matrix(polar)). ``[W]e can define more and more expressive calculi ... The most expressive ones ... should be able to deal with complex dependencies between first-class parametric abstractions.''
    binary methods

    K Bruce, L Cardelli, G Castagna, The Hopkins Objects Group, G Leavens, B Pierce: On binary methods; Theory and Practice of Object Systems, 1(1995), pp. 221-242.

    		Binary methods have a parameter ``like'' the receiver, e.g. isEqual. Discussed approaches for typing them: contra-variant parameters with dynamic overloading, or MyType, or ... (?) ...
    Subtyping vs. subclassing
    or
    F-bounded polymorphism (FBP)

    [TyOOL]
    A J H Simons: Rationalising Eiffel's type system; TOOLS'95.
    A J H Simons: Mixins: typing the superclass interface; Sheffield, 1995.

    		Subtying is a mechanism for reusing client code, subclassing is for reusing the server code [TyOOL]. The type for instances of a class, esp. self, and its subclasses is F-bounded. FBP corresponds to the subclass relationship rather than to the subtype relationship. (+) Separating subtypes and subclasses does not require the restriction that subclasses must be subtypes for modular type safety. And it allows to use FBP for subclassing. This allows covariant overriding of methods in subclasses (like in Eiffel), binary methods (parameters of the same type like self), and better mixin classes.
    (-) ``It was felt ... that having two independent hierarchies within a program overly complicated the program structure. ... [T]he single subtype-compatible hierarchy has been found effective.'' [Michael F Kilian: Trellis: What we have learned from a strongly typed language; Position statement OOPSLA'92]
    Analysis Requirements & Principles Paradigms Abstractions Domains Features foundational safety flexible typing Syntactics Defining PLs Language List
    Ulf Schünemann 191100