Re: [Caml-list] Understanding why Ocaml doesn't support operator overloading.

[William Lovas <wlovas@stwing.upenn.edu>]

On Fri, Nov 29, 2002 at 07:00:21PM -0500, Mike Lin wrote:
> If this is really a problem then what gets generated when you write any 
> polymorphic function at all?

I think the whole idea behind polymorphic functions is that they don't
*care* about the type that 'a is instantiated as -- generic code that works
for all instantiations can be generated.  This is only really useful for
parametrized types, like 'a list, which is why it's called parametric
polymorphism.  As an exercise, try to write a useful function that operates
on just 'a's -- you'll find it a challenge :)  (in fact, i think there's a
theorem in one of Philip Wadler's papers that says the *only* function of
type 'a -> 'a in a purely functional language is the identity function).

> The proposal is to allow constrained 
> polymorphism; the polymorphism that is already in OCaml seems to 
> supersede this with regard to the above objection.

Overloading is also known as ad-hoc polymorphism, which as i understand it
basically means "rule-based" -- you can't generate generic code, but you
can generate all possibilites and pick the right one based on some set of
rules.

Just because "constrained polymorphism" seems less powerful than fully
parametric polymorphism doesn't mean it's just as tractable.  The analogy
that immediately came to mind for me comes from theory of computation -- a
subset of a regular language is not necessarily regular, even though it's
smaller.

> I wonder if the unification algorithm can be generalized to intersect 
> sets of allowable types instead of unifying "for all" type variables. 
> It doesn't seem too ludicrous in principle but I could easily have 
> missed some nasty corner case.

The type inference algorithm simply assigns type variables to expressions,
generates a set of constraints based on how those expressions are put
together, and then `unifies' those constraints to make sure that they don't
lead to any contradictory equalities, like `int = float'.  Trying to
generalize this would mean changing the `=' relation to something more
interesting, like maybe subset containment or something.  Clearly, this
would not be a trivial undertaking..

There has been research into "intersection types", but i don't know if they
have anything to do with your proposal... maybe someone else can shed some
light?

cheers,
William
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners