[Caml-list] inference engine

[skaller <skaller@ozemail.com.au>]

In an example like:

let f (x:int) = 1 + x

the inference engine first examines:

let (f:'a -> 'b) (x:'c) = 1 + x

to specialise 'a, 'b, 'c, and then compares
the infered value of 'c with the constraint on
x, which is 'int' in this case.

For example in

let f (x:int) = x

x is first an un specialised type variable, but the
interface seen by outside clients is constrained to 

	int -> int

Having seen the typing used in polymorphic variants,
of the kind

	[> .. ] and [< .. ]

(I can never remember which is which .. )

I wonder if it isn't possible for the inference
engine to make the type of 'x' on entry to 
the function something like

	[> int ]

meaning 'at least constrainable to '"int" '.
If that were possible the following error would
be caught earlier:

	let f (x:int) = x +. 1.0

at the point 'float' is infered for x, since

	float & [> int] 

is empty. On the other hand, in the case

	let f (x:int) = x

the return type (before constraint is applied) is still

	[> int] & 'a

which is 'a. That is: by attaching 'at least T' for annotation
t (in positive position?? and at most in negative??) to the
type accumulated in the inference engine's tables, we get
earlier error diagnosis, without changing the actual result.

This is 'mandatory typing', but the type which is mandatory isn't
the one of the annotation, but 'some type wider than it'
(or, perhaps narrower in negative position ..??)

Well, I'm not a type theorist, its just an idea ..


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