Re: [Caml-list] Odd failure to infer types

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4263 bytes --]

Indeed, a let-bound [] is generalized to a polymorphic ('a list), while a
let-bound (ref []), or (Array.make n []), is not generalized. It would be
unsound to do so as if you had a reference to a polymorphic ('a list) you
could add elements of different types in the list.

When a type variable is not generalized (polymorphic), it stays an "unknown"
of the type system until it is unified to a known type:

# let r = ref [];;
val r : '_a list ref = {contents = []}
# r := 1 :: !r;;
- : unit = ()
# r;;
- : int list ref = {contents = [1]}

'_a is sometimes called a "weakly polymorphic variable", in fact it is not
polymorphic at all. It is just an unknown.

In the code example above, the real type for '_a could be determined after
two phrases in the top level. It may also happen as a compilation unit (if
the code was written in a file instead of fed phrase-per-phrase to the
toplevel). We wouldn't observe the intermediary '_a inferred type, as the
type are inferred globally.

It is forbidden however to keep an "undetermined variable" in a module
interface. This is what the error message here says: the variable '_a could
neither be generalized (as it is not a let-bound value, but a reference
resulting from a call to the "ref" function), nor determined by unification
with something in the module.
Keeping undetermined variables in a module interface would break the
separate compilation permitted by the interface/implementation distinction
at the module level. Indeed, if a module A had undetermined variables in its
interface, and modules B and C used A, B and C would have to coordinate each
other to make sure that the instantiations they make (for the undetermined)
are compatible; you couldn't compile B with A, and C with A, separately.

The solution is to give enough indications locally, in the module, so that
the reference type can be determined:

 let states = Array.make ... ([] : (int * int * dir) list * (char * int *
int) array * string)




It also seems quite wrong to me. You should perhaps file a bug into
> Mantis if no typing expert answers.
>

I don't want to criticize your answer which was very helpful, but I would
like to point out that I have seen the "when you don't understand the type
checker, it may be a bug" reaction quite often on this list. Indeed, all
software has failures and the OCaml type checker is not exempt of bugs, most
particularly on the delicate or recently changed parts of the system (first
class modules, etc.).

In general, the type checker is quite solid. I personally find that thinking
of a tool bug when I'm stuck on something is actually counter-productive in
most situations; when debugging something, you need strong guarantees of
what "is right" and what "may have gone wrong". Insinuating doubts against
the tool (on which you have no control) is a good way, at least for me, to
not push myself into really thinking about what I could have done wrong on
my side. Therefore, I try to always assume that the tools are right (and in
my case working with the OCaml typechecker, they have never failed me),
because it saves me lots of doubts, confusion, and self-indulgence.


On Sat, Sep 3, 2011 at 1:46 PM, Guillaume Yziquel <
guillaume.yziquel@citycable.ch> wrote:
> Le Saturday 03 Sep 2011 à 13:35:22 (+0200), Philippe Veber a écrit :
>>    Hi, I'm really no typing expert and have not looked much into your
>>    code, so sorry in advance if what I say is irrelevant. Christophe got
>>    it right I think : I'd say that an array value cannot be polymorphic
>>    because it is mutable. I've quickly searched the web and found that
>>    [1]
http://mirror.ocamlcore.org/caml.inria.fr/pub/ml-archives/caml-list/
>>    2001/12/0dccd30f4582e551a674562e3ddcc03c.en.html
>
> Yes, Christophe got it right.
>
> While not having the let-restriction on [] seems right theoretically, I
> see little practical use case for it however.
>
> --
>     Guillaume Yziquel
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

[-- Attachment #2: Type: text/html, Size: 5095 bytes --]