Re: [Caml-list] Type generalization confusion

[Reed Wilson <cedilla@gmail.com>]

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