[Caml-list] inference engine

[Caml-list] inference engine

[skaller]

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

Re: [Caml-list] inference engine

[David Baelde]

 
 What would mean [> int] & 'a ? Which types belong to this one ?
 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 ?
--
 David

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

Re: [Caml-list] inference engine

[skaller]

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

Re: [Caml-list] inference engine

[Remi Vanicat]

skaller <skaller@ozemail.com.au> writes:


[...]

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

the error given by ocaml is :

# let f (x:int) = match x with | (a,b) -> 2;;
                                 ^^^^^
This pattern matches values of type 'a * 'b
but is here used to match values of type int


-- 
Rémi Vanicat
remi.vanicat@laposte.net

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

Re: [Caml-list] inference engine

[Alain.Frisch]

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

Re: [Caml-list] inference engine

[skaller]

On Sun, 2003-09-14 at 19:48, Alain.Frisch@ens.fr wrote:
> On 14 Sep 2003, skaller wrote:

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

Hmm, well the examples are invented to be like
actual code I have. So perhaps I'm not understanding
why I'm getting the false errors sometimes.


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

Re: [Caml-list] inference engine

[skaller]

On Wed, 2003-09-17 at 05:46, skaller wrote:
> On Sun, 2003-09-14 at 19:48, Alain.Frisch@ens.fr wrote:
> > On 14 Sep 2003, skaller wrote:
> 
> > > 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.
> 
> Hmm, well the examples are invented to be like
> actual code I have. So perhaps I'm not understanding
> why I'm getting the false errors sometimes.

Here's an example of what I mean (see below for explanation):
-------------------------------------------------------------------------
ocamlopt.opt  -I src  -pp 'camlp4o
/usr/local/lib/ocaml/site-lib/ulex/pa_ulex.cma' -I
/usr/local/lib/ocaml/site-lib/ulex -c src/flx_ulex.ml
File "lpsrc/flx_ulex.ipk", line 730, characters 24-9479:
This expression has type
  lexer_state =
    < adj : int -> unit; append_comment : string -> unit;
      comment_level : int; decode : (string -> string) -> string ->
string;
      decr_comment : unit; get_absolute : string -> string;
      get_comment : string; get_incdirs : string list;
      get_relative : string -> string;
      get_srcref : Ulexing.lexbuf -> string * int * int * int; inbody :
      unit; incr_comment : unit; is_at_line_start : bool;
      newline : Ulexing.lexbuf -> unit; set_comment : string -> unit;
      set_filename : string -> unit; set_line : int -> unit;
      string_of_srcref : Ulexing.lexbuf -> string >
but is here used with type Ulexing.lexbuf
 --------------------------------------------------

now, this message is quite "wrong". There is in fact no
error in the piece of code mentioned in the message.
The message actually occured previously: here it is:

        let ts = pre_flx_lex buf state in 

In this line of code, the order of the arguments
buf and state are backwards. The inference engine
deduced the types of the arguments, and
*incorrectly* decided this piece of code was correct,
and the rather large (10K character) piece of code which came
later was wrong.

In fact, that piece of code starts off:

	and pre_flx_lex state = lexer 

This is a lexer spec for the ulex package, which after
pre-processing reads:

	and pre_flx_lex state lexbuf = 

In fact, in the mli file:

val pre_flx_lex : 
  lexer_state -> 
  Ulexing.lexbuf -> 
  Flx_parse.token list

the correct interface is given. The .mli file is already
compiled, but it isn't consulted until too late to detect
my intent.

IF the type constraint were entered into the inference
engine first, the actual error would have been detected.
As it is, the source reference of the information used
by the inference engine is lost, so it can't say something
like

	"This expression has type lexer_state,
	but appears to be used here with type Ulexing.lexbuf.
	This was deduced from line xxx chars yyy-zzz"

[Where that's the line number of the place the inference
was made]

I can understand that inferences are incremental, and there 
would be a lot of pain tracking *all* the places the data came
from to make a type inference: I'm not suggesting that.

Instead, I tried to suggest that somehow the constraint
be included as early as possible. Clearly here that is NOT
the case, or the error would have been detected where
it actually occured.

Whilst I'm getting used to this, it is a large downside
for newer Ocaml programmers: C++ programmers for example
are used to really horrible template error messages,
but not *wrong* error messages (although I have to admit
some C++ error diagnostic come rather close to that :(

This isn't a complaint. I was simply trying to suggest
a possible way to improve the error reporting. 


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

Re: [Caml-list] inference engine

[Remi Vanicat]

skaller <skaller@ozemail.com.au> writes:


[...]


> [Where that's the line number of the place the inference
> was made]
>
> I can understand that inferences are incremental, and there 
> would be a lot of pain tracking *all* the places the data came
> from to make a type inference: I'm not suggesting that.

One could use the new ocaml option -dtype and .annot file, and the
emacs mode that come with. I've never try it yet, but it give type
information inside a source, even if the source does not compile.

> Instead, I tried to suggest that somehow the constraint
> be included as early as possible. Clearly here that is NOT
> the case, or the error would have been detected where
> it actually occured.

there is a problem : one can have a .ml containing :

let f x = x + 1

let f x y = string_of_int (f x) ^ y

and the .mli :

val f : int -> string -> string

then applying the constraint of the .mli to the .ml became difficult
(at least). 

but of course it could be doable.

In such a case I put the constraint into the .ml, helping me to narrow
the error.
[...]


-- 
Rémi Vanicat
remi.vanicat@laposte.net

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