Re: Type-checking with polymorphism & overloading

hat@se-46.wpa.wtb.tue.nl wrote:


> I am working on building a type-checking system for a language which
> has both polymorphism and overloading, and compile-time type checking.
> I have been looking for an algorithm for this problem, but all
> literature found so far (robinson 1965, milner 1978, cardelli
> 1986(1987?)) assumes polymorphism only. Overloading is sometimes
> mentioned, but never included in the proposed solution.


  I have been working on a project that combines type-checking,
polymorphism, and overloading. The approach depends on a description
of operations (i.e. routines and binary operators) using a type system
that can express polymorphism. Only operators can be overloaded, and
this may be a restriction that you cannot accept.


The type-checking uses a unification algorithm with `unification
variables' introduced according to the description of operations. The
idea is to use the meanings of these variables to resolve overloading
after unification. It can be useful(/necessary?) to use information
about operators in the unification. A classification mechanism is
used in the description of operators to express properties like


                this operator is a >>relation<<, i.e. the operands have
                >>the same type<< and the result type is bool


However, rather than giving up on finding the meaning of an operator
and report an error during the unification phase, the expression with
the unresolved operator is put on hold for reinvestigation in the next
phase.


After the unification phase some expressions may remain unresolved.
These are tried one by one again, with the additional information
found since they were put on hold. Now operators for which full
operand type information is available can be resolved and their result
types may be used for further bindings of type variables. Still some
may not be resolved, and these are put on further hold. If necessary,
and if overall progress has been made, the process of reinspection is
repeated until no expressions remains.


There is more to the story, depending on the kind of types you allow.
Let this suffice for now. See the topic `structured abstractions' on
my home-page for further information about the project where the
approach is used.


Sincerely
--

Return to the comp.compilers page.
Search the comp.compilers archives again.