Re: [Caml-list] Type generalization confusion

[Reed Wilson <cedilla@gmail.com>]

[-- 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 --]