Re: [Caml-list] Polymorphic Variants

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-01-18 at 10:28 +0900, Jacques Garrigue wrote:
> From: Tom <tom.primozic@gmail.com>

> > > * overloading (but ocaml loathes overloading, you could say that the
> > >   total absence of overloading is essential to the language)
> > 
> > Is there a reason for that? Is it only hard to implement or are there any
> > conceptual / strategical / theoretical reasons?
> 
> There are two kinds of theoretical reasons.
> 
> 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.

> 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.

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

On point (a) I admit I often *remove* the annotations
after writing them (which I can't do in Felix). The need
for (b) is limited and quite acceptable IMHO, it just takes
a bit more experience than I have to pick when you need
annotations or explicit coercions.

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

Similarly I have had a 'pretty printer' program which prints
terms of an AST (the Felix grammar actually) and the fact I
could overload

	fun str : t -> string

meant I could usually forget what type it was I was converting
to a string. (There are something like 50 AST node types 
involved I think).

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.

Overall Felix library function declarations are considerably
more verbose than Ocaml .. but the implementation is about
the same complexity.

BTW: of course in Ocaml you can add annotations for documentation
purposes or to enforce a constraint.

> By the way, this all looks likes the "used this feature in C++"
> syndrome. 

Actually for Felix this is a legitimate reason :)

> Sure C++ is incredibly powerful. But it is built on rather
> shaky theoretical fundations.

What? C++ has theoretical foundations? 

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net