Re: [Caml-list] inference engine

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

On Sat, 2003-09-13 at 20:01, David Baelde wrote:
>  
>  What would mean [> int] & 'a ? Which types belong to this one ?

At least int belongs. The idea is that

	[> int] & float

is an error, since it is at least int, and exactly float;
but int is not in the type float.

>  For me, the [<> ...] notion has a only meaning for objects.
> 
>  Actually, I don't understand very well your example, since
>  the constraint on x is not a good thing in ocaml (not necessary)
>  and if you remove it, "f x = x" allows polymorphism.
> 
>  Could you explain us again your idea ?

I'll try. At present, with

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

the inference engine goes:

	let f (x:int) * = x .+ 1.0 --> x is 'a
	let f (x:int) = x .+ * 1.0 --> 'a is restricted to float
	let f (x:int*) = x +. 1.0 --> float is restricted to int ERROR

where the * marks the position in the analysis: the constraint of
x to int is applied *after* the type is already deduced.

If ocaml had 'madatory typing' then the engine would go:

	let f (x:int*) = x .+ 1.0 -> x is int
	let f (x:int) = x .+ * 1.0 -> x is restriced to float ERRIR

Detecting the error here is desirable, because that's where it occurs.
Reporting, in the first case, that the constraint to int is incompatible
with the type infered (float) is not very useful, since there is no
indication HOW the inference was made, or where the error is:
the assumption is that the annotation is correct and the code
is wrong -- but the inference engine assumes the code is
correct and the annotation is wrong.

So with mandatory typing we get much better error diagnostics.
BUt Ocaml doesn't have mandatory typing: type annotations
are constraints applied *after* inference. My suggestion
is to carry the constraint into the analysis of the function
body, and diagnose a conflict as soon as possible.

To do that I'm suggesting to give x the type 'at least an int',
meaning any subsequent typing of x in the function body
must be constrainable to int -- and that is checked every time
additional information is obtained by the inference engine
to refine the type.

For another example:

	let f (x:int) = match x with | (a,b) -> ..

should give an error saying:

	let f (x:int) = match x with | (a,b) -> ..
	-------------------------------*****

	"Here x is used with type 'a * 'b,
	which is not compatible with the constraint int"


instead of

	let f(x:int) = match x with | (a,b) ->
	--------***

	"Here x is constrained to type int which
	is not compatible with type 'a * 'b"

YOu can see the second message isn't very helpful.
I KNOW it's an int. I said so. How did the compiler
decide it had type 'a * 'b?

I have to search through not only the function
body .. but also any functions that it calls.

in particular, in the case like:

	let rec f1 (x1:t1):r1 = ..
	and f2 (x2:t2):r2 = ...
	and f3 (x2:t3):r3 = ..
	...
	and f999 (x999:t999):r999 = ...

the fact the the constraints t1, r1, t2, t2, ..
are not applied until after the whole recursion
is typed, makes it almost impossible to
find a typing error, even by adding type
annotations: I'm not sure this is the case exactly,
but certainly if you forward call from
say f1 into f999, and f2 into f999, you can
get a type infered for f999 before the body
is seen, and even an error before the body,
and hence the annotation, is seen.

So the idea is simply to carry some information
into the inference process from  the annotation,
to get earlier "more precisely located" error
diagnostics.

In some circumstances, I have had to physically
reorder the functions to try to find where
the compiler got its weird typing idea from
(sure, I made an error, but it lied about
where the error was ..:)

I have a very large file which has about 30 mutually
mutually recursive functions in them that do rather nasty
lookup calculations .. its possible that the new intermodule
recursion will help here -- my functions can be fairly
logically partitioned, but they're still mutually recursive.

[Passing one to another to break the recursion is out
of the question .. they have too many arguments, it would
be too fragile]

As stated I'm not a type theorist, it's just an idea
to get some of the benefits mandatory typing would
provide, without actually having mandatory typing
(mandatory typing meaning that type annotations specify
the type, not just a constraint) -- pass the anotation
into the inference engine as a constraint not a type.


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