Re: [Caml-list] Polymorphic Variants

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: skaller <skaller@users.sourceforge.net>

> > The most theoretical one is about semantics: with generic overloading,
> > all your semantics must take types into account. This is a problem as
> > most theoretical studies of lambda-calculus are based on so-called
> > erasure semantics, where types are discarded at execution. 
> 
> Can you explain this more? The kind of overloading I'm used
> to is a matter of lookup not semantics, i.e. its just syntactic
> sugar to save the human reader's memory.

Because you're doing some partial evaluation :-)
Namely you can view an overloaded function as a function taking extra
hidden parameters: the types of its arguments. If these types are
monomorphic, then you can immediately partially evaluate your function
to choose the right implementation. But if they are polymorphic, you
need to pass extra information around. This is what is done in Haskell
for instance, passing dictionnaries for type classes.
So an alternative view is that overloading is a type dependent
translation from the source code to an explicit version. You can only
drop the types after this translation. So this means that you cannot
understand the source code locally: you need to be aware of the type
information around it.

> > Reading the description below, this all looks nice, independently of
> > the semantics limitation described above. However, you can kiss
> > farewell to type inference. With such an extensive overloading, you
> > would need type annotations all over the place.
> 
> Felix makes this tradeoff. Types are deduced bottom up (s-attributes),
> so variables and function return types are calculated, but function
> parameters must be explicitly typed.

This works if you don't add either subtyping or return-type
overloading to the mix. Then you must also know the type of variables
and the return type of functions. 

> Even in Ocaml it is necessary to write some annotations
> in two cases:
> 
> (a) hard to understand error messages from type inference
> 
> (b) polymorphic variants

This is not exactly the same thing, as these annotations have no
impact on the semantics. Of course, one could say: if we have the
annotation, why not use it for the semantics? But this is another
story, with different implications.

> On the other hand some code would just be impossible
> without overloading. For example C has
> 
> 	char, short, int, long, long long
> 	unsigned versions
> 	float, double, long double
> 
> which is 13 distinct 'number' types, and I would hate
> to have to write:
> 
> 	1 int_add 2
> 	1L long_add 2L

Actually this is not only overloading that is used here, but also
automatic conversions. When writing numeric computations in ocaml, I
find it just as painful to have to add float_of_int, as to add the dot
after all operators. (In number of characters, float_of_int might be
the biggest...)
For overloading alone, the module system could help.
If we had the operators defined with different types in each of the
numeric type modules, then one could just choose the numeric type used
with "open Mynumtype". This is one of the reasons I pushed for having
a local "let open" construct... which can be simulated by "let
module", at a slight cost.

> So in some cases with inference and without overloading,
> *you need the annotations anyhow*, they just go into the
> function names in an unprincipled manner, instead of going
> into the function parameter types in a principled -- 
> and indeed syntactically enforced -- manner.

I believe this is the strongest argument for overloading: that it
allows using types in a principled way. Of course, whether this is
really principled depends on the code you write...

Jacques Garrigue