From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 13A827FA5E for ; Wed, 10 May 2017 20:14:15 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cedilla@gmail.com; spf=Pass smtp.mailfrom=cedilla@gmail.com; spf=None smtp.helo=postmaster@mail-ua0-f172.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of cedilla@gmail.com) identity=pra; client-ip=209.85.217.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of cedilla@gmail.com designates 209.85.217.172 as permitted sender) identity=mailfrom; client-ip=209.85.217.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ua0-f172.google.com) identity=helo; client-ip=209.85.217.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="postmaster@mail-ua0-f172.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A0sOFPx21ucnOUhFlsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0VL/ad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okC?= =?us-ascii?q?YHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWhOXshRWSJPAY2y?= =?us-ascii?q?cpUBAPYaMOlCs4XwvUEDoQeiCQSuAu7k1z9GhmXx3a0/y+kvDR/J0xI9ENkTsH?= =?us-ascii?q?vUrdH1NLwVUeCz0aLFyinMYO1L1jf87IjIdgourOqDXbJ1a8XRyE0vGxnZgVWX?= =?us-ascii?q?rIzoJjWY3fkOvWiD9+dsS/6jhmo9pwxyojWj3NkghpTLi44P11zJ9zt1zYAoLt?= =?us-ascii?q?OiUkF7e8SrEJ5IuiGaKYR2RsQiTnltuCkgy70GvYe3fDUQx5g73hLfZeGLfoqW?= =?us-ascii?q?7h75W+aRJjB4hH1heL2hnRq97U+gyujkWsm11lZFsDZFn8HSunwR0xHf8MuKR/?= =?us-ascii?q?tn8ku/xDqC1Rrf5vxGLEwqjabbLoQuwr80lpodq0TDGSr2lV3qg6CIa0ok++yo?= =?us-ascii?q?6+D9bbj9qZ+cMpV7igD6Mqg0hsO/BuE4PhAUX2eH4eS8yKHj/UrhTbpWlPI2l6?= =?us-ascii?q?3ZvIneJcQava65HxRY0p0j6ha6Fzepys4UnXgBLFJfeRKIlZLlO1/UIKOwMfDq?= =?us-ascii?q?qF2plH9PxuvadunqC5DJa3zCi6vJfLBn6kcaxhBlnv5F4JcBMLwMLLrMW0vqs9?= =?us-ascii?q?qQWhQ0Pw2wx+/PB9B014dYUmWKVPzKeJjOuEOFs7p8a9KHY5UY7XOkc6Ao?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CvBwBNVxNZf6zZVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhRgHg2KaRAaBJpgBgl6DRgKEeQdCFQEBAQEBAQEBAQEBEgEBCQs?= =?us-ascii?q?LCCYxgjMiAYI/AQEBAQIBIwQZARsdAQMBCwYDAgsNKgICIQEBEQEFARwGEwiKA?= =?us-ascii?q?AEDCAUIlRSRGj+MB4FsGAUBHIMKBYNWChknDVaCYgEBAQEBAQQBAQEBAQEBGQI?= =?us-ascii?q?GEoYHhT+CVIUdgmAFkSeMKDuOSIRTkWuLLYdOFB+BFTWBLC8gCBkVRhmEToIuI?= =?us-ascii?q?DaJGQEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CvBwBNVxNZf6zZVdFdHAEBBAEBCgEBFwEBBAEBCgEBhRg?= =?us-ascii?q?Hg2KaRAaBJpgBgl6DRgKEeQdCFQEBAQEBAQEBAQEBEgEBCQsLCCYxgjMiAYI/A?= =?us-ascii?q?QEBAQIBIwQZARsdAQMBCwYDAgsNKgICIQEBEQEFARwGEwiKAAEDCAUIlRSRGj+?= =?us-ascii?q?MB4FsGAUBHIMKBYNWChknDVaCYgEBAQEBAQQBAQEBAQEBGQIGEoYHhT+CVIUdg?= =?us-ascii?q?mAFkSeMKDuOSIRTkWuLLYdOFB+BFTWBLC8gCBkVRhmEToIuIDaJGQEBAQ?= X-IronPort-AV: E=Sophos;i="5.38,320,1491256800"; d="scan'208,217";a="223163324" Received: from mail-ua0-f172.google.com ([209.85.217.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 10 May 2017 20:14:13 +0200 Received: by mail-ua0-f172.google.com with SMTP id g49so4509156uaa.1 for ; Wed, 10 May 2017 11:14:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=xSR9i+hPN0ucMAmjpKsTI4FL0m0TxdzoUROyblYtA7s=; b=UJgX4W+2RiPrAz5WuzTXnRMPJpTPFmGKQsca0hDzV4pa57YVEXpD1iTUHXS2Mb/VZK 3MoO8MBJLjKjLiniYaxFBiawD+8CmAx72aJhEjVSdoTniGjIQeqPdZRAEWTz5vabnOtc lHxTfIqszey0z/yYsitX6WIlj7QiWPyLqfTgUZiZMRQK2T/snvfhqFOUgIanZjBlEvw5 QSAGhbZ0vXds13arkepmz0Um0I/zIgAxA9YiPKBSk8hagYSTbwyBlayAQAnRYopMnqOC ey27cI4NJNipAg3osoGNfwnNeTAhuj/TGQxAx0oaUj4Gy3BNKlqdmwRZB0pfmzFmaSwi 7g8A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=xSR9i+hPN0ucMAmjpKsTI4FL0m0TxdzoUROyblYtA7s=; b=rfywCM1/jhZeWZ5pmi22PdGtK/3Mk2feZZ12pmGqkL3WED08EUseFP0act1dVTj6YW ewSsF7bptBqRkeZbKcZWoKXiHcQf5USQ52L0DEFYs93HPrWZbAMh1gTIAvAn1/4J+4/H zp3x/M3mCAj5xSLHh1xlBYNC0ya0/gIbEQ3uIY3BDvamn/JxPOpyAv1r+6afWnk9AhON qQTsTs0b2K49tIamyR5O9DdcHwvzTmkk3xzD6LZPncwTNoNTTRjIWEXp2oBwOXQw1LTo k/i+tmFFcWR3HkPj6kiBKzv7oE1AeVIDHk7L+lO7GUyWpEQrlVkMIyvQI82KvUxsVNH6 goOg== X-Gm-Message-State: AODbwcBJHrtk1ND49OtG/2mR7VopgJJv2jS8Mr9XWMXSWx6Lbp46fXx0 O7yStBNK5FqYKRVOLeXwmotX8G3Y7A== X-Received: by 10.31.98.196 with SMTP id w187mr3169797vkb.96.1494440052017; Wed, 10 May 2017 11:14:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.31.2.19 with HTTP; Wed, 10 May 2017 11:14:11 -0700 (PDT) In-Reply-To: References: <1494320088.2074838.970492485.42DF8438@webmail.messagingengine.com> From: Reed Wilson Date: Wed, 10 May 2017 11:14:11 -0700 Message-ID: To: Caml List Cc: Leo White , mandrykin@ispras.ru, Jeremy Yallop Content-Type: multipart/alternative; boundary=94eb2c07b57a70511a054f2f7033 X-Validation-by: cedilla@gmail.com Subject: Re: [Caml-list] Type generalization confusion --94eb2c07b57a70511a054f2f7033 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Tue, May 9, 2017 at 1:54 PM, Jeremy Yallop wrote: > On 9 May 2017 at 20:56, 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 =3D [| 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 =3D [| None |] in (* val array : 'a option > array *) > let () =3D array.(0) <- Some 3 in > let Some x =3D 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 wrote: > type (_, _) field =3D > | 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 =3D { f : 'b. ('a -> 'b, 'b) field } [@@unboxed] > let lookup_array =3D [| { f =3D String (0, End) }; { f =3D String (1, End= ) } |] > let lookup i =3D match lookup_array.(i) with { f } -> f > let of_chan : ('a, 'b) field -> 'a -> in_channel -> 'b =3D fun _ _ _ -> > assert > false > let x =3D of_chan (lookup 0) (fun s -> int_of_string s) stdin > let y =3D 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 =3D [| {f =3D 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 =3D { 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! --=20 =C3=A7 --94eb2c07b57a70511a054f2f7033 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

= 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&= gt; wrote:
> The c= urrent 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:
>
>=C2=A0 =C2=A0let lookup_array =3D [| String (0, End); String (1, End) |= ]

The value restriction prevents generalization here, since arrays are=
mutable.=C2=A0 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.

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

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

I suppose I should = have known why the array didn't work, I just didn't realize it sinc= e 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=C2=A0<mandrykin@ispras.ru>=C2=A0wro= te:
type (_, _) field = =3D
=C2=A0 | Int8 : ('a,= 'b) field -> ((int -> 'a),'b) field
=C2=A0 | S= tring : int * ('a, 'b) field -> ((string -> 'a), 'b) = field
=C2=A0 | End : ('b= , 'b) field
type 'a lookup_param =3D { f : 'b. ('= a -> 'b, 'b) field } [@@unboxed]
let lookup_array =3D [| { f = =3D String (0, End) }; { f =3D String (1, End) } |]
let lookup i =3D mat= ch lookup_array.(i) with { f } -> f
let of_chan : ('a, 'b) fi= eld -> 'a -> in_channel -> 'b =3D fun _ _ _ -> assertfalse
let x =3D of_chan (lookup 0) (fun s -> int_of_string s) stdin=
let y =3D of_chan (lookup 0) (fun s -> s) stdin

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

=C2=A0 let lookup_a= rray =3D [| {f =3D Int8 (String (0, End))} |]

fails with:

Er= ror: This expression has type (int -> string -> 'a, 'a) field=
=C2=A0 =C2=A0 =C2=A0 =C2=A0but an expressi= on was expected of type
=C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0(int -> string -> 'a, string -> 'a) field=
=C2=A0 =C2=A0 =C2=A0 =C2=A0The type variab= le 'a occurs inside string -> 'a

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

=C2=A0 type lookup_param =3D { f : 'b. (int -> str= ing -> 'b, 'b) field }

And everything works fine. This will let me tes= t the speed difference between an extra pointer lookup vs. allocating ~15 w= ords per loop for my actual code. Honestly, my guess is that this is all ac= ademic 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!

--
=C3=A7
--94eb2c07b57a70511a054f2f7033--