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!

--
ç