From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p83BZnsZ026398 for ; Sat, 3 Sep 2011 13:35:49 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjADANUPYk7RVdQ2kGdsb2JhbABCmQeHQgGIGggUAQEBAQkJDQcUBCKBRgEBAQECARICExkBBhUPAwsBAwELBgULGiEiAREBBQEKEgYTEhCHUQSYRgqMPYJWK4ROO4htAgMGhmQEglSQWoxmPINt X-IronPort-AV: E=Sophos;i="4.68,324,1312149600"; d="scan'208";a="107574112" Received: from mail-vw0-f54.google.com ([209.85.212.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 03 Sep 2011 13:35:44 +0200 Received: by vws18 with SMTP id 18so5156870vws.27 for ; Sat, 03 Sep 2011 04:35:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=dmihqLs0g+knDci814l8Jr1Hip2jdQlqW2abVUu3YSM=; b=WKrQAeBjQzkibaC9y7k/P6gEKC3VbnlnDAMtlmEtxPHOXEgdwvvotvKu7OY8zPRMYj OqFr3mst1KqQ6RzQVjEy0rN4kGxtcEkkuLBRq0Fy7aLb+frb4Nx2T7KUNllWvjCU+HCJ D0oxYfY89hFP5MPDa7UXm2YmwKDxswW446BhM= Received: by 10.52.101.227 with SMTP id fj3mr1993298vdb.367.1315049742109; Sat, 03 Sep 2011 04:35:42 -0700 (PDT) MIME-Version: 1.0 Received: by 10.221.13.202 with HTTP; Sat, 3 Sep 2011 04:35:22 -0700 (PDT) In-Reply-To: <20110903103653.GX15100@localhost> References: <87ty8uc5ph.fsf@frosties.localnet> <20110903103653.GX15100@localhost> From: Philippe Veber Date: Sat, 3 Sep 2011 13:35:22 +0200 Message-ID: To: Guillaume Yziquel Cc: Goswin von Brederlow , caml-list@inria.fr Content-Type: multipart/alternative; boundary=bcaec5485c94bd8c1004ac07e07d X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] Odd failure to infer types --bcaec5485c94bd8c1004ac07e07d Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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 http://mirror.ocamlcore.org/caml.inria.fr/pub/ml-archives/caml-list/2001/12= /0dccd30f4582e551a674562e3ddcc03c.en.html Quoting Fran=E7ois Pottier: "Any polymorphic, mutable structure is unsound and rightly rejected. A monomorphic, mutable structure that contains polymorphic data is sound, but cannot be expressed in ML's type system where universal quantification must be prenex." So it seems to me that whatever the way you try to achieve it, you simply can't define a value state of type val states : ('a list * (char * int * int) array * string) list array (implicitely for all 'a). If the compiler is right, you'll always end up with a weak type variable somewhere. my 2 cent, ph. 2011/9/3 Guillaume Yziquel > Le Saturday 03 Sep 2011 =E0 11:53:30 (+0200), Goswin von Brederlow a =E9c= rit : > > Hi, > > > > I'm implementing a solver for the game Atomix. If you don't know it then > > don't worry. It isn't relevant. > > > > I split things up into submodules and now one of the submodules does not > > infere the right types: > > > > File "Atomix.ml", line 168, characters 11-876: > > Error: The type of this module, > > sig > > type dir =3D NORTH | SOUTH | WEST | EAST > > val max_moves : int > > val cache : (string, unit) Hashtbl.t > > val states : > > ('_a list * (char * int * int) array * string) list array > > val string_of_dir : dir -> string > > val print : > > (int * int * dir) list * (char * int * int) array * string -> > unit > > val num_states : int > > end, contains type variables that cannot be generalized > > > > I believe this is wrong. In S.num_states the call to "print state" > > fixates the type for state and the "states.(d) <- state::states.(d);" > > should then fixate the missing '_a in the type for states. > > > > Anyone know why? > > It also seems quite wrong to me. You should perhaps file a bug into > Mantis if no typing expert answers. > > Did you try adding type annotations one at a time near the call to print > and the states.(d) assignment in your anonymous List.fold-ing function? > To check precisely what the type inferencer gets right and what it gets > wrong? > > I'd be curious to know whether annotating state in "states.(d) <- > state::states.(d)" solves your problem. Since it's here that the '_a in > the type of states should be fixated. > > -- > 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 > > --bcaec5485c94bd8c1004ac07e07d Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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

http://mirror.oca= mlcore.org/caml.inria.fr/pub/ml-archives/caml-list/2001/12/0dccd30f4582e551= a674562e3ddcc03c.en.html

Quoting Fran=E7ois Pottier:
"Any polymorphic, mutable structur= e is unsound and rightly rejected. A monomorphic, mutable structure that co= ntains polymorphic data is sound, but cannot be expressed in ML's type = system where universal quantification must be prenex."

So it seems to me that whatever the way you try to achieve it, you simp= ly can't define a value state of type

val states : ('a list= * (char * int * int) array * string) list array

(implicitely for al= l 'a). If the compiler is right, you'll always end up with a weak t= ype variable somewhere.

my 2 cent,

ph.


2011/9/3 Gu= illaume Yziquel <guillaume.yziquel@citycable.ch>
Le Saturday 03 Sep 2011 =E0 11:53:30 (+0200), Goswin von Brederlow a =E9cri= t :
> Hi,
>
> I'm implementing a solver for the game Atomix. If you don't kn= ow it then
> don't worry. It isn't relevant.
>
> I split things up into submodules and now one of the submodules does n= ot
> infere the right types:
>
> File "Atomix.ml", line 168, characters 11-876:
> Error: The type of this module,
> =A0 =A0 =A0 =A0sig
> =A0 =A0 =A0 =A0 =A0type dir =3D NORTH | SOUTH | WEST | EAST
> =A0 =A0 =A0 =A0 =A0val max_moves : int
> =A0 =A0 =A0 =A0 =A0val cache : (string, unit) Hashtbl.t
> =A0 =A0 =A0 =A0 =A0val states :
> =A0 =A0 =A0 =A0 =A0 =A0('_a list * (char * int * int) array * stri= ng) list array
> =A0 =A0 =A0 =A0 =A0val string_of_dir : dir -> string
> =A0 =A0 =A0 =A0 =A0val print :
> =A0 =A0 =A0 =A0 =A0 =A0(int * int * dir) list * (char * int * int) arr= ay * string -> unit
> =A0 =A0 =A0 =A0 =A0val num_states : int
> =A0 =A0 =A0 =A0end, contains type variables that cannot be generalized=
>
> I believe this is wrong. In S.num_states the call to "print state= "
> fixates the type for state and the "states.(d) <- state::state= s.(d);"
> should then fixate the missing '_a in the type for states.
>
> Anyone know why?

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

Did you try adding type annotations one at a time near the call to print
and the states.(d) assignment in your anonymous List.fold-ing function?
To check precisely what the type inferencer gets right and what it gets
wrong?

I'd be curious to know whether annotating state in "states.(d) <= ;-
state::states.(d)" solves your problem. Since it's here that the &= #39;_a in
the type of states should be fixated.

--
=A0 =A0 Guillaume Yziquel


--
Caml-list mailing list. =A0Subscription 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


--bcaec5485c94bd8c1004ac07e07d--