[Prev][Next][Index][Thread]

Paper announcement

[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

This is to inform the Types Forum that we have written a
the paper 

    Typed OO functional programming with late binding
    by Zhenyu Qian and Bernd Krieg-Brueckner
    Appeared in Proc. 10th European Conf. on Object-Oriented Programming,
    Springer LNCS 1098, 1996.

The paper is available via

    http://www.informatik.uni-bremen.de/~qian/abs-foop.html


Abstract:

The paper introduces a language called TOFL, which 
(1) combines the Haskell-like and object-oriented type system, 
(2) extends the mechanism of sending messages to objects to that of sending 
messages to expressions, and
(3) supports dynamic binding mechanism.

More concretely, the language supports the following: 
(1) It allows the usual OO classes and FP algebraic data types.
    Types are constructed by algebraic datatype constructors 
    and OO classes (regarded as 0-ary type constructors).
(2) The sybtyping relation satisfies the following restrictions:
     (a) The subtyping between two classes is allowed in the usual OO style.
     (b) A type with an algebraic datatype constructors may be a subtype 
         of a class, but in this case the class cannot contain attributes.
         The style of the declaration resembles that of Haskell. 
     (c) The subtype relation for complex types is non-variant 
         at the domain position of a function type
         and co-variant at all other positions.
     (d) No subtype relation may exist between two types 
         with different heading algebraic datatype constructors.
     (e) No classes may be a subtype of a type 
         with a heading algebraic datatype constructor.
(3) The type system allows a concept of self type.
(4) The self type can occur anywhere and arbitrary times within a type 
    corresponding to the receiver-expression. But outside the type, 
    the self type can only occur at co-variant positions. Under this 
    restriction, TOFL can support binary operations naturally without 
    sacrificing the static type safty.
(5) The underlying calculus, ie. a stratified and explicitly typed 
    $\lmd$-calculus $\HM$ with overloaded functions, where 
    redefinitions and late binding become late binding of overloaded functions,
    has been proved to be confluent.

Best regards,
Zhenyu Qian

-------------
Dr. Zhenyu Qian
FB3 Informatik, Universitaet Bremen, D-28359 Bremen, Germany
http://www.informatik.uni-bremen.de/~qian
mailto:qian@informatik.uni-Bremen.de