Type Inference and Overloading

Type Inference and Overloading

[Tom Primožič]

[-- Attachment #1: Type: text/plain, Size: 1361 bytes --]

I would like to pose one really perverse question (perverse because it
mentions overloading).

I have done a lot of thinking over the subject of type inference with
overloading. I have also read a lot, however, no paper satisfied me. I don't
like constraints (neither
GCaml<http://web.yl.is.s.u-tokyo.ac.jp/%7Efuruse/gcaml/>nor System
CT <http://citeseer.ist.psu.edu/camarao99type.html> like) as i find them too
difficult for the user to understand.

I have been trying to think of another mechanism for inferring overloaded
types, but have yet been unsuccessful.

Does anyone have any idea what kind of algorithm and structures would the
compiler need to deploy to correctly infer the types for these functions:

a : int -> float -> int
a : float -> int -> int

b : int -> int -> int
b : float -> int -> int

let f1 x y =
      let z = a x y in
      b x y + z

let f1 x y z =
      let r = a x z in
      let s = a z y in
      b x y + r * s

It is pretty clear to the human that f1 has type float -> int -> int,
however, it takes a bit more thinking to realize that the type of f1 is int
-> int -> float -> int. However, while human sees the whole "program" in one
glance, the computer cannot perceive a picture as a whole. Thus, some
supposedly pretty complicated algorithm should be used.

Anyone has any idea?

Tom

[-- Attachment #2: Type: text/html, Size: 2506 bytes --]

Re: [Caml-list] Type Inference and Overloading

[skaller]

On Mon, 2006-04-10 at 10:51 +0200, Tom Primožič wrote:
> I would like to pose one really perverse question (perverse because it
> mentions overloading). 
> 
> I have done a lot of thinking over the subject of type inference with
> overloading. I have also read a lot, however, no paper satisfied me. I
> don't like constraints (neither GCaml nor System CT like) as i find
> them too difficult for the user to understand. 

I couldn't understand the constraints of CT either. 

I think (if I understand correctly) that GCaml is simple.
A generic function is called 'as if it were polymorphic'.
Which implementation is used is calculated independently.
Thus there is no impact on the existing type inference
engine for calls to generics, there are new rules for
choosing the implementation based on the construction
of the generic function.

I suggest you look at the rules the new version of C# uses,
it can do both overloading and argument type inference,
with some constraints (I don't understand them either :)

> I have been trying to think of another mechanism for inferring
> overloaded types, but have yet been unsuccessful. 

Generalised Unification. Keep a set of sets of equations.
Each application leads to a set of alternatives.

For each alternative, duplicate the sets of equations,
then add that alternative to each set. Now unify as much
as possible, go on to the next set.

This is VERY expensive. A cut occurs when a function
'goes out of scope'. At the point, the type of the function
must be established (that is, for each argument's type variable,
the same assignment must exist in all the sets). If not,
the program is ambiguous.

BTW: just a pie in the sky :)

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

Re: [Caml-list] Type Inference and Overloading

[Andrej Bauer]

On Monday 10 April 2006 10:51, Tom Primožič wrote:
> I would like to pose one really perverse question (perverse because it
> mentions overloading).

To add insult to perversion, I will mention Haskell. Have you had a look at 
Haskell's type classes? They allow you to write "+" or "print" to mean many 
different things, while not doing actual overloading.

So if all you care about is usability for programmer, and not so much about 
overloading for the sake of overloading, type classes might be a nice option.

Andrej

Re: [Caml-list] Type Inference and Overloading

[Brian Hurt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: TEXT/PLAIN; charset=X-UNKNOWN; format=flowed, Size: 3753 bytes --]



On Mon, 10 Apr 2006, Tom Primo¾iè wrote:

> Does anyone have any idea what kind of algorithm and structures would the
> compiler need to deploy to correctly infer the types for these functions:
>
> a : int -> float -> int
> a : float -> int -> int

I'm not sure there is one- in fact, I don't think there is.  Consider if I 
have the following case as above, and then I type:

let g = a;;

what's the type of g?  Is it int -> float -> int or float -> int -> int?

What if I type:

let g x y = a y x;;

?  What happens if I define two functions:
val c: int -> float -> int
val c: int -> int -> int

and then say:
let h x = c 3 x;;

What type does h have?

As a more general rule, how I deal with overloading in Ocaml is to use 
modules and functors.  Say I want to implement Newton's method.  In other 
languages, I'd depend upon overloading (possibly even operator 
overloading).  In Ocaml, I'd do something like:

module type Req =
 	type t (* the type of the number system *)
 	val sub : t -> t -> t (* subtraction *)
 	val div: t -> t -> t (* division *)
 	val within_epsilon: t -> t -> bool
end

module Newtons(Alg: Req) = struct
 	let meth f df x =
 		let rec loop x =
 			let x' = Alg.sub x (Alg.div (f x) (df x)) in
 			if (Alg.within_epsilon x x') then
 				x'
 			else
 				loop x'
 		in
 		loop x
end;;

Of course, a real implementation would be more complicated than this, but 
this gets the idea across.  I could then create "overloaded" versions of 
my Newtons method just by calling the functor with the right modules, for 
example:

module Float = struct
 	type t = float
 	let sub = ( -. );;
 	let div = ( /. );;
 	let within_epsilon x y = (abs_float (x -. y)) < 1e-14;;
end;;

module FloatNewtons = Newtons(Float);;

Similiar code bits can give me Newton's method for integers (use an 
epsilon of 1), complexes, quaternions, even vectors/matricies.

Note that the performance overhead of using a functor is not signifigantly 
larger than the performance overhead of using virtual or overloaded 
functions- you're calling the sub, div, and within_epsilon functions via a 
function pointer either way.  And if you were to use ocamldefun, you could 
eliminate even that cost.

Another advantage of Ocaml's funtors over overloaded functions/operators 
is in documentation.  You can see, right up front, in the .mli file, what 
operations the algorithm needs.  And the compiler checks to make sure you 
are providing them.

The other important point to make here is that the operations provided to 
a module are not implicitly "part of" the object itself.  This is 
especially important with comparison functions (such as within_epsilon 
above)- I have come to the conclusion that comparison can *NOT* be a 
member function:
http://enfranchisedmind.com/blog/archive/2006/01/30/62
http://enfranchisedmind.com/blog/archive/2006/03/28/123

As an example of this problem in action (and how functors solve it), 
consider the above case except that sometimes I want to use a run-time 
defined value for epsilon, instead of the hardcoded 1e-14.  I could then 
do:

module FloatE = struct
 	(* floating point with variable epsilon *)
 	type t = float
 	let sub = ( -. );;
 	let div = ( /. );;
 	let epsilon = ref 1e-14;;
 	let within_epsilon x y = (abs_float (x -. y)) < !epsilon;;
end;;

module FloatENewtons = Newtons(FloatE);;


Now I have two different Newton's methods on floats: one that uses the 
fixed epsilon of 1e-14, and one that uses a variable epsilon.  Note that 
both FloatNewtons.meth and FloatENewtons.meth have the same type!  If the 
comparison method was built in, I'd need two different "types" of floats.

Brian

Re: [Caml-list] Type Inference and Overloading

[Tom Primožič]

[-- Attachment #1: Type: text/plain, Size: 1763 bytes --]

On 10/04/06, Brian Hurt <bhurt@spnz.org> wrote:
>
> > a : int -> float -> int
> > a : float -> int -> int
>
> I'm not sure there is one- in fact, I don't think there is.  Consider if I
> have the following case as above, and then I type:
>
> let g = a;;
>
> what's the type of g?  Is it int -> float -> int or float -> int -> int?


 Hm... I definitely agree that there is no way to find out the type of g in
this case, there do in fact exist 3 ways of how to deal with it:

   1. reject it (i believe this is the "right" way),
   2. have the compiler automatically overload value g, producing two
   functions, or
   3. make one value of a the /default/ value and use the type of that
   one.

As a more general rule, how I deal with overloading in Ocaml is to use
> modules and functors.
>

But I fear you might have misunderstood myself. I am in no way trying either
to convince anyone to implement overloading in OCaml nor saying that there
are no (useful) alternatives. During my quest I have scanned many threads of
this list over and over, and I know that any such suggestions and complaints
are dealt with in a pretty harsh way.

I am young and naive and full of idealistic illusions. So I believe in
overloading. As a great tool for the user. (Haskell's type classes are just
as irritating as the 1.5 + 0. type error, if you ask me.)

My point was, that in cases that function actually DO have a non-ambiguous
type (f1 : float -> int -> int, f1 : int -> int -> float -> int), while it
is quite easy for human to infer it, it (seems) extremely hard for a machine
to do so. Thus I am looking for a (hopefully cheap) mechanism to infer the
types correctly in such cases. I will deal with ambiguities in another way.

[-- Attachment #2: Type: text/html, Size: 2639 bytes --]

Re: Type Inference and Overloading

[Stefan Monnier]

> a : int -> float -> int
> a : float -> int -> int

You might want to take a look at intersection types.


        Stefan