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.
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