typing problem with sexplib and mutually recursive polymorphic types

typing problem with sexplib and mutually recursive polymorphic types

[Yoann Padioleau]

Hi, 

I tried a slightly modified version of sexplib by jane street 
on this simple file foo.ml:

    type 'a x1 = 'a * 'a
    and x2 = int x1
    and x3 = string x1
     (* with sexp *)

and succeeded to generate another file containing the sexp_of_xx code 
in a file foo2.ml:

    open Foo
    
    let rec x1_of_sexp__ =
      let _loc = "Xxx.x1"
      in
        fun _of_a ->
          function
          | Sexp.List ([ v1; v2 ]) ->
              let v1 = _of_a v1 and v2 = _of_a v2 in (v1, v2)
          | sexp -> Conv_error.tuple_of_size_n_expected _loc 2 sexp
    and x1_of_sexp _of_a sexp =
      try x1_of_sexp__ _of_a sexp
      with
      | Conv_error.No_variant_match ((msg, sexp)) -> Conv.of_sexp_error msg sexp
    and x2_of_sexp__ =
      let _loc = "Xxx.x2" in fun sexp -> x1_of_sexp Conv.int_of_sexp sexp
    and x2_of_sexp sexp =
      try x2_of_sexp__ sexp
      with
      | Conv_error.No_variant_match ((msg, sexp)) -> Conv.of_sexp_error msg sexp
    and x3_of_sexp__ =
      let _loc = "Xxx.x3" in fun sexp -> x1_of_sexp Conv.string_of_sexp sexp
    and x3_of_sexp sexp =
      try x3_of_sexp__ sexp
      with
      | Conv_error.No_variant_match ((msg, sexp)) -> Conv.of_sexp_error msg sexp
      
    let rec sexp_of_x1 _of_a (v1, v2) =
      let v1 = _of_a v1 and v2 = _of_a v2 in Sexp.List [ v1; v2 ]
    and sexp_of_x2 v = sexp_of_x1 Conv.sexp_of_int v
    and sexp_of_x3 v = sexp_of_x1 Conv.sexp_of_string v
  

But then the ocaml type system refuses to type this second file with the
error message: 
File "foo2.ml", line 22, characters 48-67:
This expression has type Sexp.t -> string but is here used with type
  Sexp.t -> int

Apparently the problem is that ocaml was not able to generalize
the type of x1_of_sexp and that it's first utilisation with an 'int'
force the x1_of_sexp to always return an 'int' instead of a 'string'
in the second case. Is there a way to rewrite this generated code
to avoid this typing problem ? Is it because of those 
 'let _loc = ... in fun ... ->"  that distrubs the ocaml type system ?

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Markus Mottl]

On Tue, Mar 10, 2009 at 22:45, Yoann Padioleau <padator@wanadoo.fr> wrote:
> But then the ocaml type system refuses to type this second file with the
> error message:
> File "foo2.ml", line 22, characters 48-67:
> This expression has type Sexp.t -> string but is here used with type
>  Sexp.t -> int
>
> Apparently the problem is that ocaml was not able to generalize
> the type of x1_of_sexp and that it's first utilisation with an 'int'
> force the x1_of_sexp to always return an 'int' instead of a 'string'
> in the second case. Is there a way to rewrite this generated code
> to avoid this typing problem ? Is it because of those
>  'let _loc = ... in fun ... ->"  that distrubs the ocaml type system ?

This has to do with recursive type definitions, not with generating
closures with _loc.  The following is similar and does not compile
either:

  let rec foo () = []
  and bar () = "asdf" :: foo ()
  and bla () = 42 :: foo ()

These definitions are clearly sound, but the type checker doesn't get
it.  Note, however, that the following works:

  let foo () = []
  let rec bar () = "asdf" :: foo ()
  and bla () = 42 :: foo ()

You can apply the same trick in your specific example by simply moving
the type definition of x1 out of the cycle with x2 and x3.

Cheers,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[yoann padioleau]

> 
> This has to do with recursive type definitions, not with generating
> closures with _loc. The following is similar and does not compile
> either:
> 
> let rec foo () = []
> and bar () = "asdf" :: foo ()
> and bla () = 42 :: foo ()
> 
> These definitions are clearly sound, but the type checker doesn't get
> it. Note, however, that the following works:
> 
> let foo () = []
> let rec bar () = "asdf" :: foo ()
> and bla () = 42 :: foo ()
> 
> You can apply the same trick in your specific example by simply moving
> the type definition of x1 out of the cycle with x2 and x3.

Yes on this example, but what if I can't move it out because
the types really need to be mutually recursive ?


> 
> Cheers,
> Markus
> 
> -- 
> Markus Mottl http://www.ocaml.info markus.mottl@gmail.com
> 
> 

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Markus Mottl]

On Wed, Mar 11, 2009 at 02:11, yoann padioleau <padator@wanadoo.fr> wrote:
> Yes on this example, but what if I can't move it out because
> the types really need to be mutually recursive ?

I'm afraid, I don't see any straightforward way of achieving this
goal.  If the above were allowed in a truly recursive way, you'd
essentially end up with polymorphic recursion, which is undecidable.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Yitzhak Mandelbaum]

While I'm not sure it will help you in this case (because the code is  
generated), I should note that type *inference* for polymorphic  
recursion is undecidable, but type *checking* is not. Moreover, its  
pretty easy to do in OCaml (if a bit clunky).

An earlier discussion on this list covered a number of ways to do it.  
Here's one:

http://groups.google.com/group/fa.caml/msg/d85e3f62dd52d365

Cheers,
Yitzhak


On Mar 11, 2009, at 10:20 AM, Markus Mottl wrote:

> On Wed, Mar 11, 2009 at 02:11, yoann padioleau <padator@wanadoo.fr>  
> wrote:
>> Yes on this example, but what if I can't move it out because
>> the types really need to be mutually recursive ?
>
> I'm afraid, I don't see any straightforward way of achieving this
> goal.  If the above were allowed in a truly recursive way, you'd
> essentially end up with polymorphic recursion, which is undecidable.
>
> Regards,
> Markus
>
> -- 
> Markus Mottl        http://www.ocaml.info         
> markus.mottl@gmail.com
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

-----------------------------
Yitzhak Mandelbaum

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Markus Mottl]

On Wed, Mar 11, 2009 at 10:32, Yitzhak Mandelbaum
<yitzhakm@cs.princeton.edu> wrote:
> While I'm not sure it will help you in this case (because the code is
> generated), I should note that type *inference* for polymorphic recursion is
> undecidable, but type *checking* is not. Moreover, its pretty easy to do in
> OCaml (if a bit clunky).

That's true, but unlike Haskell OCaml doesn't have mandatory types.
This means the user can't force the compiler to start out with
user-provided type declarations.  The OCaml compiler will always run
type inference first and only try to unify the result with the
user-provided type declaration, i.e. when it's too late.

Of course, there are workarounds (recursive modules, polymorphic
record fields), but, as you said, they are clunky indeed...

Cheers,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Damien Doligez]

On 2009-03-11, at 15:44, Markus Mottl wrote:

> That's true, but unlike Haskell OCaml doesn't have mandatory types.
> This means the user can't force the compiler to start out with
> user-provided type declarations.  The OCaml compiler will always run
> type inference first and only try to unify the result with the
> user-provided type declaration, i.e. when it's too late.

That is not quite true any more.  For example, I changed the
type-checker a few years ago to start with the user-provided type
when typing a let rec, in order to be able to debug my large
recursive definitions.  Note that I didn't do that from scrach,
I used an infrastructure that was already present for seeding the
type inference in some cases.  IIRC, it is there for some object-
oriented reason.

Next time you have a type error on the wrong recursive call, try
annotating the function at its definition point.

For example, compare the error messages for:

   let rec f x = g x []
   and g x l =
     match l with
     | [] -> f "a"
     | [a] -> f 1
     | [a; b] -> f 2
     | _ -> f 3
   ;;

versus:

   let rec f (x : int) = g x []
   and g x l =
     match l with
     | [] -> f "a"
     | [a] -> f 1
     | [a; b] -> f 2
     | _ -> f 3
   ;;

Note that your second sentence is still right, because type annotations
are only used in this way in a limited number of cases (let rec is one
example).

-- Damien

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Markus Mottl]

On Wed, Mar 11, 2009 at 12:16, Damien Doligez <damien.doligez@inria.fr> wrote:
> That is not quite true any more.  For example, I changed the
> type-checker a few years ago to start with the user-provided type
> when typing a let rec, in order to be able to debug my large
> recursive definitions.  Note that I didn't do that from scrach,
> I used an infrastructure that was already present for seeding the
> type inference in some cases.  IIRC, it is there for some object-
> oriented reason.

Interesting, this change seems to have passed unobserved by me and is
certainly a great debugging aid.  Does this mean that eventually
polymorphic recursion might be supported by OCaml?  What's still
missing for that feature?

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Till Varoquaux]

This is a quick overview of my current understanding. Corrections by
higher authorities are welcome:

Optional type declarations in ocaml only enable to restrict given
types (not to generalize them). Although it enables better error
reporting it does not allow us to compile anything that would compile
without. This can be seen as additional constraints to enforce during
typing eg:

let f : ('a -> 'a -> 'a) = (+) 1

is fine because we have added the constraint "the return type must be
the same as both the argument types". If we were type-checking this as
'a.'a->'a->'a this would fail.

There's a caveat for formats

let f : (_,_,_) format = "%s"

and object types:

let f (v : < pol:'a.'a -> _;..> ) =
  v#pol 4;
  v#pol ()

The ability to generalize type by hand is being explored by didier
remy in MLF. I do not know how far this is from going in OCaml (if
ever).

Till



On Wed, Mar 11, 2009 at 12:43 PM, Markus Mottl <markus.mottl@gmail.com> wrote:
> On Wed, Mar 11, 2009 at 12:16, Damien Doligez <damien.doligez@inria.fr> wrote:
>> That is not quite true any more.  For example, I changed the
>> type-checker a few years ago to start with the user-provided type
>> when typing a let rec, in order to be able to debug my large
>> recursive definitions.  Note that I didn't do that from scrach,
>> I used an infrastructure that was already present for seeding the
>> type inference in some cases.  IIRC, it is there for some object-
>> oriented reason.
>
> Interesting, this change seems to have passed unobserved by me and is
> certainly a great debugging aid.  Does this mean that eventually
> polymorphic recursion might be supported by OCaml?  What's still
> missing for that feature?
>
> Regards,
> Markus
>
> --
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Yoann Padioleau]

Yitzhak Mandelbaum <yitzhakm@CS.Princeton.EDU> writes:

> While I'm not sure it will help you in this case (because the code is
> generated), 

The code is generated, but I am ok with modifying it. I use 
typeconv/sexplib/binprot and camlp4 just as a way to produce a first draft
and then I refine the result. I prefer to see the generated code
and have concrete files (and in this case in fact I have no
choice as the the default generated code is not good enough).

> I should note that type *inference* for polymorphic
> recursion is undecidable, but type *checking* is not. Moreover, its
> pretty easy to do in OCaml (if a bit clunky).
>
> An earlier discussion on this list covered a number of ways to do it.
> Here's one:
>
> http://groups.google.com/group/fa.caml/msg/d85e3f62dd52d365

Thanks. I tried the {f: 'a. 'a } trick and it works on my
simplified example but I failed using it on my original file. Never mind,
I artificially broke the mutually recursive dependency
and now it works. 

Thanks.

>
> Cheers,
> Yitzhak
>
>
> On Mar 11, 2009, at 10:20 AM, Markus Mottl wrote:
>
>> On Wed, Mar 11, 2009 at 02:11, yoann padioleau <padator@wanadoo.fr>
>> wrote:
>>> Yes on this example, but what if I can't move it out because
>>> the types really need to be mutually recursive ?
>>
>> I'm afraid, I don't see any straightforward way of achieving this
>> goal.  If the above were allowed in a truly recursive way, you'd
>> essentially end up with polymorphic recursion, which is undecidable.
>>
>> Regards,
>> Markus
>>
>> -- 
>> Markus Mottl        http://www.ocaml.info
>> markus.mottl@gmail.com
>>
>> _______________________________________________
>> Caml-list mailing list. Subscription management:
>> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>> Archives: http://caml.inria.fr
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
> -----------------------------
> Yitzhak Mandelbaum

Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Jacques Garrigue]

From: Markus Mottl <markus.mottl@gmail.com>
> On Wed, Mar 11, 2009 at 12:16, Damien Doligez <damien.doligez@inria.fr> wrote:
> > That is not quite true any more.  For example, I changed the
> > type-checker a few years ago to start with the user-provided type
> > when typing a let rec, in order to be able to debug my large
> > recursive definitions.  Note that I didn't do that from scrach,
> > I used an infrastructure that was already present for seeding the
> > type inference in some cases.  IIRC, it is there for some object-
> > oriented reason.
> 
> Interesting, this change seems to have passed unobserved by me and is
> certainly a great debugging aid.  Does this mean that eventually
> polymorphic recursion might be supported by OCaml?  What's still
> missing for that feature?

Actually I added universal type annotations and polymorphic recursion
in a branch a few years ago. The idea was to provide a basis for
implementing GADTs. But since the GADT work was not finished, it was
never merged in the main trunk.

So it would be very easy to have polymorphic recursion in ocaml.
The real question is whether it is that useful in the absence of
GADTs, knowing that you can already do it in a somewhat verbose way.

Cheers,

Jacques Garrigue