Re: Type-checking with polymorphism & overloading

fjh@cs.mu.OZ.AU (Fergus Henderson) writes:
> <hat@se-46.wpa.wtb.tue.nl> writes:
>
>>I am working on building a type-checking system for a language which
>>has both polymorphism and overloading, and compile-time type checking.
>>Surely, someone in this large world must have looked at the
>>combination of polymorpism and overloading ?
>
> I notice that quite a few of the references cited by other posters in
> this thread were papers about Haskell type classes. Haskell type
> classes were originally proposed as an alternative to overloading, but
> IMHO type classes and overloading solve different problems. The latest


That was basically my problem as well, after reading some suggested
papers. It sounds nice at first, but if you think about it carefully,
then sub-typing and overloading are 2 different things, and these
papers really address the problem of solving overloading of sub-types.


Since I don't have sub-typing, this is kind of useless to me.
Not all is lost though. Due to the kind people in this newsgroup, I
discovered this fact, I learned a lot about type systems, and about
terminology used in this field.
As a result, I am now able to write a description which is less ambiguous.
Here it comes (I prepared this text before I read your reply):
------------------------------
During the last 2 weeks,I learned a lot about type systems, and type
inference algorithms. With this information, I can now better specify the
question to which I'd like an answer.


First, a description of the language we are developing:


- The language allows polymorphism (in the literature known as generic
    polymorphism) in function DECLARATIONS in the libraries.


    Polymorphic function DEFINITIONS are not allowed. In the implementation,
    we use the polymorphic capabilities of our target language (C++).


    We use the normal quantification rule of quantifying only at the
    outermost level of the expression.






- The language allows overloading (in the literature known as ad hoc
    polymorphism) for functions (both in the libraries and in the program
    written by the user), most built-in operators (like '+'), and integer
    constants (but I don't mind having an overloaded function c()->nat,
    c()->int if that helps).






- The language is strongly typed. For type checking of expressions, this
    means that type information is available about everything used in an
    expression (if it is not available, the user has made an error).






- The language has no relations between types. In other words, it has a
    type nat, and a type int, but there is no sub-type relation between
    them.


    One of the effects of this decision is that there is no coercion from
    one type to another. In this way, users are forced to convert between
    different types explicitly (in other words, "i:int, n:nat, i:=n" should
    fail).


    This decision is also the cause for having overloaded constants
    (basically, "i:int, n:nat, n:=1, i:=1" should work without having to
    specify the type of the constant).






    At this moment, there doesn't seem to be a particular reason to limit
    the use of either polymorphism, or overloading.
    In other words, for a function f, having the declarations


    "f(int)->nat" and "f(nat)->int"


    should cause no problems, as long as the type system is able to decide
    (uniquely) which f to use.
    This should also hold for overloaded polymorphic functions.
    For example, if I would declare


    f(any)->any (with any a polymorphic type variable)


    then expressions like "i:int, i:=f(i)" can still get uniquely typed.




      Note that for expressions like "i:=f(1)" to be possible (which is what
      we want), an extra mechanism has to be introduced. I call this mechanism
      "preference types". It means that whenever I have a choice between nat
      and int (and real) for an constant, then the smallest type is chosen.
      This is different from normal sub-typing, because it only affects
      constants, not variables. (Without the mechanism, the type system has no
      way of choosing between "f(nat)->int", and "f(int)->int" (instantiated
      from the polymorphic declaration)).
      The latter mechanism is discussable. I don't really want this specific
      mechanism, I just needed a decision mechanism for types of constants, and
      this mechanism produces nice, easy to understand results.




      (The latter is important, the users are not used to writing programs,
      and anything the compiler can catch helps in reducing development time.
      The price of demanding that users are explicit is an added bonus in that
      respect.)


Objective
---------
The aim is to perform type-checking on expressions, such that after type
checking (a) each node in the expression has a single monomorphic type,
and (b) there is no other solution (in other words, the found solution
is unique).


Requirement (a) ensures that all types in the expression are
monomorphic, and can be translated to a type in the target language.
Requirement (b) ensures that the user gets no surprises.


Note that (b) is more restrictive than normal (where only existence is
required). (This requirement comes from the idea that it should be clear
to the user what the compiler is doing.)




Discussion about read literature
--------------------------------
In the literature, [Milner78] and lots of others have an insufficient
type system, because overloading is not covered.


Other articles such as [Smith94], [Jones92], extend the system of Milner
by introducing relations between types (called classes or sub-types).
Overloading is then possible as long as it fits inside the type hierarchy.


In the type system described above, there is no such structure (except
for constants maybe). They also don't demand a unique solution.
These differences excludes all those type systems as well.


And now...
----------
At this moment, I am largely empty-handed regarding scientifically
proper solutions.
I can build a solution to the above problem, but without scientific
foundations, I have no idea whether the type system will work in
a well-defined manner.


What I am looking for is a type checking algorithm, which solves the
above problem. If necessary, minor adjustments in the requirements are
possible (that's the nice thing if you build your own language!!).




References
----------
[Jones92] "Qualified types: Theory and Practice" by Mark Philip Jones,
Phdthesis 1992, Oxford


[Milner78] "A Theory of Type Polymorphism in Programming" by Robin Milner,
Journal of Computer and System Sciences, 17(1978) 348-375


[Smith94] "Principal type schemes for functional languages with
overloading and subtyping" by Geoffrey S. Smith, Science of
Computer Programming, 23(1994) 197-226
------------------------


Albert
---
The @wtb.tue.nl domain is known to bounce mail incorrectly sometimes.
If you are one of the lucky persons, please try again, and send the log
as well, so I can prove it to our postmaster. Thank you !
--

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