On 14 Sep 2003, skaller wrote:

> I'll try. At present, with
>
> 	let f (x:int) = x +. 1.0
>
> the inference engine goes:

I keep wondering if you're trying some kind of troll here, or if you're
serious. When you're saying "At present the inference engine goes..", what
do you mean? Have you tried your examples with the actual OCaml type
checker?

As a matter of fact, the type checker performs unification with the
constraints on arguments of functions as soon as possible. You don't need
any extra notion like 'mandatory typing' to do this.

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

No, that's not how it works. Try the example with OCaml.

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

Do you know about unification?

> For another example:

OCaml does report the error where you expect. Try the example with OCaml.

> 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

Again, this is wrong.


-- Alain

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