[Caml-list] Type inference problem

[Caml-list] Type inference problem

[Vasilij Karpow]

Can anyone explain why O'Caml specializes the following:

let simple ?fn list =
  let fn = match fn with
  | Some fn -> fn
  | None -> fun t -> t in
  let rec print = function
    | [] -> ()
    | x :: xs -> print_endline (fn x); print xs
  in
  print list

let _ =
  simple ["1"];
  simple ~fn:(fun i -> string_of_int i) [1]


to: val simple : ?fn:(string -> string) -> string list -> unit

Thanks in advance.
    
P.S. A bit offtopic. I suspect this mailing list is filled with
skilled mathematicians (and just intelligent people), and since
nobody i know was able to solve my problem, here it is:
http://algol.prosalg.no/~malc/moo.ps [.dvi|.pdf|.tex]    

-- 
mailto:malc@pulsesoft.com
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type inference problem

[Remi VANICAT]

Vasilij Karpow <malc@boblycat.com> writes:

> Can anyone explain why O'Caml specializes the following:
> 
> let simple ?fn list =
>   let fn = match fn with
>   | Some fn -> fn
>   | None -> fun t -> t in
>   let rec print = function
>     | [] -> ()
>     | x :: xs -> print_endline (fn x); print xs
>   in
>   print list
> 
> let _ =
>   simple ["1"];
>   simple ~fn:(fun i -> string_of_int i) [1]
> 
> 
> to: val simple : ?fn:(string -> string) -> string list -> unit

it's easy. If the value was polymorphic, you would be authorized to
write :

simple [1; 2; 3; 4; 5]

which is unsound.


-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type inference problem

[Nils Goesche]

Vasilij Karpow <malc@boblycat.com> writes:

> P.S. A bit offtopic. I suspect this mailing list is filled with
> skilled mathematicians (and just intelligent people), and since
> nobody i know was able to solve my problem, here it is:
> http://algol.prosalg.no/~malc/moo.ps [.dvi|.pdf|.tex]    

Subtract g(n) on both sides.  You'll get a system of linear equations
which has g(0)...g(n) as solutions:

  M x = b,

where M = (m_ij), m_ij = Binom(i, j) is a lower triangular matrix.  It
is possible to write down a closed expression for M^{-1}, although
this might be a rather huge formula with many sum signs, I am not
sure.  Check some numeric text book.  Cholesky might be of help, or
maybe not; check some numeric text book.

Regards,
-- 
Nils Goesche
"Don't ask for whom the <CTRL-G> tolls."

PGP key ID 0x42B32FC9

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type inference problem

[Jacques Garrigue]

> Can anyone explain why O'Caml specializes the following:
> 
> let simple ?fn list =
>   let fn = match fn with
>   | Some fn -> fn
>   | None -> fun t -> t in
>   let rec print = function
>     | [] -> ()
>     | x :: xs -> print_endline (fn x); print xs
>   in
>   print list
> val simple : ?fn:(string -> string) -> string list -> unit

The simple answer is type inference:
  * fn and (fun t -> t) should have the same type 'a -> 'a
  * the result of (fn x) is of type string
  * consequently, 'a = string
  * and the type of fn is string -> string

Now, what you would want is to distinguish when there is a function
passed and when there is none at the type level.
You cannot do it with optional arguments, but you can use the
following encoding:

module Default : sig
  type ('a, 'b) t
  val none : ('a, 'a) t
  val some : 'a -> ('a, 'b) t
  val get : 'a -> ('b, 'a) t -> 'b
  val get_lazy : 'a Lazy.t -> ('b, 'a) t -> 'b
end = struct
  type ('a,'b) t = Dnone | Dsome of 'a
  let none = Dnone
  let some x = Dsome x
  let get d = function Dnone -> Obj.magic d | Dsome x -> x        
  let get_lazy d = function Dnone -> Obj.magic (Lazy.force d) | Dsome x -> x
end

let out ~fn x = let fn = Default.get (fun x -> x) fn in print_endline (fn x)
val out : fn:('a -> string, 'b -> 'b) Default.t -> 'a -> unit = <fun>

out ~fn:Default.none "Hello";;
out ~fn:(Default.some string_of_int) 3;;

Would it be possible to include it with optional arguments?
Theoretically, yes, but it would require a new syntax, make typing
more complex, and checking weaker (the type of the default is only
checked the first time the function is called with no argument).
I'm not sure it's worth it.

     Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type inference problem

[Brian Hurt]

On Tue, 1 Nov 2005, Jonathan Roewen wrote:

> Hi,
>
> I can't figure out what's wrong with my code =(
>
> It's on a paste site, so will only last about 24 hours or so.
> http://rafb.net/paste/results/Uux57B97.html
>
> jonathan@moonbeam:~/dst/stdlib$ ocamlc VFS.ml
> File "VFS.ml", line 106, characters 3-6:
> This expression has type int but is here used with type unit
>
> It -has- to return int ;-) But I have no idea where the type
> constraint is coming from that wants it to return unit. Change it to
> return unit, and where it's used complains it doesn't return type int
> (so that constraint is correct).

A general tactic I use in cases like this is to add type annotations. 
What is almost certainly happening is that somewhere else before this line 
in your code you are returning unit as a value, so Ocaml thinks it's 
supposed to return unit.  If you add a type annotation to explicitly state 
that it returns int, Ocaml will instead give an error where you return 
unit, allowing you to fix the problem.

Brian

Re: [Caml-list] Type inference problem

[skaller]

On Tue, 2005-11-01 at 21:19 +1300, Jonathan Roewen wrote:
> Ohh, I found it =) If without else, where return type of if is non-unit.
> 
> Is it possible compiler could flag this error a bit better? IE: when
> if returns non-unit, and there's no else?

Ocaml uses some shortcuts because it doesn't distinguish
functional from procedural code.

Felix does. It uses:

	if c1 then e1 [elif c2 then e2 ..] else ee endif

for functional code -- the 'else' is mandatory, and the expressions
e1, e2 .. ee may not be void, and must unify.

Procedural code uses

	if c do 
		... ; ... ; 
	[elif
		... ; ... ;
	..
	]

	[else
		..; .. ; 
	]
	done;

and all the ... ; entries must be (manifestly) of type void.


Now, the problem with your request is that Ocaml is
*deducing* the type of read .. it is in fact unit, so the
condition for reporting an error you state would NOT catch
any error because there isn't one.

On the other hand if you obey a reasonable style rule:

"always annotate the return type of a recursive function"

then Ocaml would have done precisely what you asked for.
Whenever you get a type error you don't understand
*add type annotations* to try to localise the problem.

I would restate your request like this: when the inference
engine reports a type error, it should provide a full traceback
of all parts of the code that lead it to deduce the conflicting
types.

I expect the error message would be hard to read.. and also that
it would greatly complicate the inference engine to actually
keep track of where all the inferences come from -- not sure
on either point.

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

Re: [Caml-list] Type inference problem

[skaller]

On Tue, 2005-11-01 at 20:58 +1300, Jonathan Roewen wrote:
> Hi,
> 
> I can't figure out what's wrong with my code =(
> 
> It's on a paste site, so will only last about 24 hours or so.
> http://rafb.net/paste/results/Uux57B97.html
> 
> jonathan@moonbeam:~/dst/stdlib$ ocamlc VFS.ml
> File "VFS.ml", line 106, characters 3-6:
> This expression has type int but is here used with type unit
> 
> It -has- to return int ;-) But I have no idea where the type
> constraint is coming from that wants it to return unit. Change it to
> return unit, and where it's used complains it doesn't return type int
> (so that constraint is correct).

You could replace this line:

    let rec write data fd buf off len =

with this one:

    let rec write data fd buf off len : int =

to find out. But I can tell you anyhow the bug is here

   let rec read data fd buf off len =
      if len + fd.offset > fd.size then read data fd buf off (fd.size - fd.offset);

in the second line:

	if true then 1;

will give the same error for the same reason: the above line is just
shorthand for:

	if true then 1 else ();

and the type of 1 and () disagree. In your case, the type of the 'then'
branch is infered to be 'unit' .. and then you go and return
an 'int' at the end of the function -- there is no 'conflict'
until that point. Declaring the return type will catch the
error where it really is, the second line of the read function.

You can fix this by:

      if len + fd.offset > fd.size then 
	ignore(read data fd buf off (fd.size - fd.offset));

or by

      if len + fd.offset > fd.size then 
	let _ =  read data fd buf off (fd.size - fd.offset) in ();



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

Re: [Caml-list] Type inference problem

[Jonathan Roewen]

Ohh, I found it =) If without else, where return type of if is non-unit.

Is it possible compiler could flag this error a bit better? IE: when
if returns non-unit, and there's no else?

Jonathan

[Caml-list] Type inference problem

[Jonathan Roewen]

Hi,

I can't figure out what's wrong with my code =(

It's on a paste site, so will only last about 24 hours or so.
http://rafb.net/paste/results/Uux57B97.html

jonathan@moonbeam:~/dst/stdlib$ ocamlc VFS.ml
File "VFS.ml", line 106, characters 3-6:
This expression has type int but is here used with type unit

It -has- to return int ;-) But I have no idea where the type
constraint is coming from that wants it to return unit. Change it to
return unit, and where it's used complains it doesn't return type int
(so that constraint is correct).

Jonathan