[Caml-list] Type generalization confusion

[Caml-list] Type generalization confusion

[Reed Wilson]

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

I've been working with some of the new features introduced with GADTs, and
ran into a confusing instance of the "type variables that cannot be
generalized" error.

The simplified program is as follows:
type _ field = Int : int -> 'a field
let a = Int 3
let b = Int (1 + 2)
let inside = 1 + 2
let c = Int inside

ocamlc -i returns:
type _ field = Int : int -> 'a field
val a : 'a field
val b : '_a field
val inside : int
val c : 'a field

with b remaining non-generalized. The problem I'm having with it is that
the type variable doesn't depend on the value at all, so I don't see how
that can prevent generalization.

Also, the manual says the reason some types aren't generalized is due to
"polymorphic mutable data structures". Nothing I created is mutable, so why
was generalization turned off in the first place?

Finally, I'm confused why separating the function from the definition is
enough to fix this; c is generalized simply by defining 1+2 in a separate
value (which must be global, apparently).

Thanks,
Reed Wilson

-- 
ç

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

Re: [Caml-list] Type generalization confusion

[Gabriel Scherer]

This is the value restriction at work: only values are generalized
(often of the form "fun x -> ..."), and while (Int 3) is a value, (Int
(1 + 2)) is not.

On Mon, May 8, 2017 at 11:32 AM, Reed Wilson <cedilla@gmail.com> wrote:
> I've been working with some of the new features introduced with GADTs, and
> ran into a confusing instance of the "type variables that cannot be
> generalized" error.
>
> The simplified program is as follows:
> type _ field = Int : int -> 'a field
> let a = Int 3
> let b = Int (1 + 2)
> let inside = 1 + 2
> let c = Int inside
>
> ocamlc -i returns:
> type _ field = Int : int -> 'a field
> val a : 'a field
> val b : '_a field
> val inside : int
> val c : 'a field
>
> with b remaining non-generalized. The problem I'm having with it is that the
> type variable doesn't depend on the value at all, so I don't see how that
> can prevent generalization.
>
> Also, the manual says the reason some types aren't generalized is due to
> "polymorphic mutable data structures". Nothing I created is mutable, so why
> was generalization turned off in the first place?
>
> Finally, I'm confused why separating the function from the definition is
> enough to fix this; c is generalized simply by defining 1+2 in a separate
> value (which must be global, apparently).
>
> Thanks,
> Reed Wilson
>
> --
> ç

Re: [Caml-list] Type generalization confusion

[Reed Wilson]

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

But this similar type has no problem:

type 'a field = Int of int
let a = Int 3
let b = Int (1 + 2)

Both a and b receive the same generalized type. Why does the GADT style
prevent this from occuring?

On Mon, May 8, 2017 at 8:49 PM, Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> This is the value restriction at work: only values are generalized
> (often of the form "fun x -> ..."), and while (Int 3) is a value, (Int
> (1 + 2)) is not.
>
> On Mon, May 8, 2017 at 11:32 AM, Reed Wilson <cedilla@gmail.com> wrote:
> > I've been working with some of the new features introduced with GADTs,
> and
> > ran into a confusing instance of the "type variables that cannot be
> > generalized" error.
> >
> > The simplified program is as follows:
> > type _ field = Int : int -> 'a field
> > let a = Int 3
> > let b = Int (1 + 2)
> > let inside = 1 + 2
> > let c = Int inside
> >
> > ocamlc -i returns:
> > type _ field = Int : int -> 'a field
> > val a : 'a field
> > val b : '_a field
> > val inside : int
> > val c : 'a field
> >
> > with b remaining non-generalized. The problem I'm having with it is that
> the
> > type variable doesn't depend on the value at all, so I don't see how that
> > can prevent generalization.
> >
> > Also, the manual says the reason some types aren't generalized is due to
> > "polymorphic mutable data structures". Nothing I created is mutable, so
> why
> > was generalization turned off in the first place?
> >
> > Finally, I'm confused why separating the function from the definition is
> > enough to fix this; c is generalized simply by defining 1+2 in a separate
> > value (which must be global, apparently).
> >
> > Thanks,
> > Reed Wilson
> >
> > --
> > ç
>



-- 
ç

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

Re: [Caml-list] Type generalization confusion

[Leo White]

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

> But this similar type has no problem:
>  type 'a field = Int of int
>  let a = Int 3
>  let b = Int (1 + 2)

This is the relaxed value restriction: `field` is covariant in it's
parameter which means that the type variable is only used in
covariant positions and so can be generalized even though the
expression is not a value.
> Both a and b receive the same generalized type. Why does the GADT
> style prevent this from occuring?
 OCaml currently just assumes that types defined with GADT syntax are
 invariant because checking of variance with GADTs is more difficult. If
 you annotate your type as covariant then it behaves the same:
  type +_ field = Int : int -> 'a field
  let a = Int 3
  let b = Int (1 + 2)

gives:

  type +_ field = Int : int -> 'a field
  val a : 'a field = Int 3
  val b : 'a field = Int 3

Regards,

Leo



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

Re: [Caml-list] Type generalization confusion

[Reed Wilson]

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

Thanks for the info! I didn't think about just telling the type system
about the variance, and this kind of fix is exactly what I was (eventually)
getting at. Unfortunately, this solution doesn't seem to work in my actual
code.

I wrote a module to read and write binary data with fixed layouts, and I'm
using a GADT to enforce typing. A simplification of my actual code:

  type (_,_) field =
  | Int8 : ('a,'b) field -> ((int -> 'a),'b) field
  | String : (int * ('a,'b) field) -> ((string -> 'a),'b) field
  | End : ('b,'b) field

  let intstring = Int8 (String (3, End))

In this case, intstring would be used as a template for reading/writing an
8-bit integer, followed by a 3-byte long string. The type would be:
  val intstring : (int -> string -> 'a, 'a) field

My reading/writing functions are of the type:

  val to_chan : ('a, unit) field -> out_channel -> 'a
  val of_chan : ('a, 'b) field -> 'a -> in_channel -> 'b

This ensures that the arguments I pass are of the correct type for the
field. Passing intstring to the field parameter of the functions results in
a type:
  val intstring_to_chan : out_channel -> int -> string -> unit
  val intstring_of_chan : (int -> string -> '_a) -> in_channel -> '_a

(Note that the non-generalization of intstring_of_chan is not a problem
since I would always pass the reading function at the same time as the
field value.)

The current issue I'm actually facing is trying to create a lookup table
for these templates, which only differ by the length of some of the fields.
For example:

  let lookup_array = [| String (0, End); String (1, End) |]
  let lookup_fun i = String (i, End)

These end up being the following types:
  val lookup_array : (string -> '_a, '_a) field array
  val lookup_fun : int -> (string -> 'a, 'a) field

The lookup array is nongeneralized. The function works, but I'll be using
this in a very tight loop which is extremely resource-intensive. I wanted
to use a lookup table to see if that runs any faster, but I can't get it to
compile. (Even using Obj.magic didn't work)

No number of "+" or "-" in my type parameters fix the issue as they did
with the example in my previous e-mail. Everything returns:
  Error: In this GADT definition, the variance of some parameter cannot be
checked

Thanks again for your help! I think I'm a bit over my head with all this,
but I'd like to figure out as much as I can.


On May 9, 2017 01:55, "Leo White" <leo@lpw25.net> wrote:

> > But this similar type has no problem:
> >  type 'a field = Int of int
> >  let a = Int 3
> >  let b = Int (1 + 2)
>
> This is the relaxed value restriction: `field` is covariant in it's
> parameter which means that the type variable is only used in covariant
> positions and so can be generalized even though the expression is not a
> value.
>
> > Both a and b receive the same generalized type. Why does the GADT style
> prevent this from occuring?
>
> OCaml currently just assumes that types defined with GADT syntax are
> invariant because checking of variance with GADTs is more difficult. If you
> annotate your type as covariant then it behaves the same:
>
>   type +_ field = Int : int -> 'a field
>   let a = Int 3
>   let b = Int (1 + 2)
>
> gives:
>
>   type +_ field = Int : int -> 'a field
>   val a : 'a field = Int 3
>   val b : 'a field = Int 3
>
> Regards,
>
> Leo
>
>
>

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

Re: [Caml-list] Type generalization confusion

[Jeremy Yallop]

On 9 May 2017 at 20:56, Reed Wilson <cedilla@gmail.com> wrote:
>   type (_,_) field =
>   | Int8 : ('a,'b) field -> ((int -> 'a),'b) field
>   | String : (int * ('a,'b) field) -> ((string -> 'a),'b) field
>   | End : ('b,'b) field
[...]
> No number of "+" or "-" in my type parameters fix the issue as they did with
> the example in my previous e-mail. Everything returns:
>   Error: In this GADT definition, the variance of some parameter cannot be
> checked

Indeed, soundness requires the parameters of 'field' to be invariant,
so there's no possibility of adding variance annotations here.

For example, the type of the End constructor makes the following
definition well typed:

  let x : (< m : int >, < m : int >) field = End

If one of the parameters (the first, say) were covariant, then that
parameter could be coerced to a supertype of < m:int >, like this

  let y = (x :> ( < >, < m : int >) field)

and then matching against y would introduce an invalid equality
between < > and < m: int >:

  match y with
    End ->
      (* Here the type checker knows by the type of End that the
         two type parameters are equal, i.e. that < > is equal to < m : int > *)
    let x = (object end) in x#m + 1

A similar argument can be made against making either parameter
contravariant.  The parameters of 'field' are therefore invariant, and
so the relaxed value restriction doesn't apply.

> The current issue I'm actually facing is trying to create a lookup table for
> these templates, which only differ by the length of some of the fields. For
> example:
>
>   let lookup_array = [| String (0, End); String (1, End) |]

The value restriction prevents generalization here, since arrays are
mutable.  If bindings of array expressions were generalized then the
following program, which writes to the array at one type (int option)
and reads from the array at a different type (string option), would be
allowed.

   let array = [| None |] in                   (* val array : 'a option array *)
   let () = array.(0) <- Some 3 in
   let Some x = array.(0) in                (* val x : 'a *)
   "abc" ^ x

So it's essential for soundness that the types of array values are not
generalized.

Re: [Caml-list] Type generalization confusion

[Reed Wilson]

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

On Tue, May 9, 2017 at 1:54 PM, Jeremy Yallop <yallop@gmail.com> wrote:

> On 9 May 2017 at 20:56, Reed Wilson <cedilla@gmail.com> wrote:
> > The current issue I'm actually facing is trying to create a lookup table
> for
> > these templates, which only differ by the length of some of the fields.
> For
> > example:
> >
> >   let lookup_array = [| String (0, End); String (1, End) |]
>
> The value restriction prevents generalization here, since arrays are
> mutable.  If bindings of array expressions were generalized then the
> following program, which writes to the array at one type (int option)
> and reads from the array at a different type (string option), would be
> allowed.
>
>    let array = [| None |] in                   (* val array : 'a option
> array *)
>    let () = array.(0) <- Some 3 in
>    let Some x = array.(0) in                (* val x : 'a *)
>    "abc" ^ x
>
> So it's essential for soundness that the types of array values are not
> generalized.
>

I suppose I should have known why the array didn't work, I just didn't
realize it since nothing I have defines a type that would have made that
unsoundness cause problems.


On Wed, May 10, 2017 at 6:29 AM, Mikhail Mandrykin <mandrykin@ispras.ru>
 wrote:

> type (_, _) field =
>   | Int8 : ('a, 'b) field -> ((int -> 'a),'b) field
>   | String : int * ('a, 'b) field -> ((string -> 'a), 'b) field
>   | End : ('b, 'b) field
> type 'a lookup_param = { f : 'b. ('a -> 'b, 'b) field } [@@unboxed]
> let lookup_array = [| { f = String (0, End) }; { f = String (1, End) } |]
> let lookup i = match lookup_array.(i) with { f } -> f
> let of_chan : ('a, 'b) field -> 'a -> in_channel -> 'b = fun _ _ _ ->
> assert
> false
> let x = of_chan (lookup 0) (fun s -> int_of_string s) stdin
> let y = of_chan (lookup 0) (fun s -> s) stdin
>

This is an interesting work-around. I had to tweak it a bit since it would
only work with templates that have one "field". For example:

  let lookup_array = [| {f = Int8 (String (0, End))} |]

fails with:

Error: This expression has type (int -> string -> 'a, 'a) field
       but an expression was expected of type
         (int -> string -> 'a, string -> 'a) field
       The type variable 'a occurs inside string -> 'a

Luckily, that's not a problem in my case since I only need this for one
field type, so I changed it to be a bit less general:

  type lookup_param = { f : 'b. (int -> string -> 'b, 'b) field }

And everything works fine. This will let me test the speed difference
between an extra pointer lookup vs. allocating ~15 words per loop for my
actual code. Honestly, my guess is that this is all academic since OCaml is
so good at small allocations, but I really wanted to know why things
weren't working.

Thanks again to everyone who responded!

-- 
ç

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

Re: [Caml-list] Type generalization confusion

[Mikhail Mandrykin]

On вторник, 9 мая 2017 г. 12:56:24 MSK Reed Wilson wrote:
> The current issue I'm actually facing is trying to create a lookup table
> for these templates, which only differ by the length of some of the fields.
> For example:
> 
>   let lookup_array = [| String (0, End); String (1, End) |]
>   let lookup_fun i = String (i, End)
Since what's needed here is actually not a generalized array type
( 'a. ((string -> 'a, 'a) field array) ),
but the generalized type of the element
( ('a. (string -> 'a, 'a) field) array ),
this could be work-around by introducing an intermediate universal type:

type (_, _) field =
  | Int8 : ('a, 'b) field -> ((int -> 'a),'b) field
  | String : int * ('a, 'b) field -> ((string -> 'a), 'b) field
  | End : ('b, 'b) field
type 'a lookup_param = { f : 'b. ('a -> 'b, 'b) field } [@@unboxed]
let lookup_array = [| { f = String (0, End) }; { f = String (1, End) } |]
let lookup i = match lookup_array.(i) with { f } -> f
let of_chan : ('a, 'b) field -> 'a -> in_channel -> 'b = fun _ _ _ -> assert 
false
let x = of_chan (lookup 0) (fun s -> int_of_string s) stdin
let y = of_chan (lookup 0) (fun s -> s) stdin

[@@unboxed] should have allowed this without any penalty of using an 
intermediate wrapper, but currently it fails:
Fatal error: exception File "bytecomp/typeopt.ml", line 97, characters 6-12: 
Assertion failed
(Typeopt.classify doesn't support universal types).
But even without [@@unboxed] this at least allows to avoid allocation of 
`String (i, End)` inside the loop.

--
Mikhail