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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 176C57FA5E for ; Tue, 9 May 2017 21:56:27 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cedilla@gmail.com; spf=Pass smtp.mailfrom=cedilla@gmail.com; spf=None smtp.helo=postmaster@mail-ua0-f177.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of cedilla@gmail.com) identity=pra; client-ip=209.85.217.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="cedilla@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of cedilla@gmail.com designates 209.85.217.177 as permitted sender) identity=mailfrom; client-ip=209.85.217.177; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ua0-f177.google.com) identity=helo; client-ip=209.85.217.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="postmaster@mail-ua0-f177.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ASBIcwBGG9njQSpOBqkvtz51GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ79r8WwAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj?= =?us-ascii?q?8KODw38G/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Ox?= =?us-ascii?q?d5cBAPQfMulFsoLyp1oOrR+lBQmrAuPk1zhFiWPo0qIn0uQhFQXG0xY7EtIBtX?= =?us-ascii?q?TbttT1NKMIXe+py6nIyCzOYvVL0jn+8IjFag4tre2IUL5qcsfcyVMjGx3YgliS?= =?us-ascii?q?s4DpIjGY2+YLvmOG9eRvT/ivhHQiqwxpojig2MMsio7Ri4IQ0F/E9CF5zJ8oJd?= =?us-ascii?q?KiVEJ3eNCkHIZSuiyYLYd2TcQiQ2ZnuCY+1LIKo4K0fC8PyJg/xh7fbeKIc5SQ?= =?us-ascii?q?7x79SOqcJS10iXFldb6lmRq+7EqtxvfhWsS20ltGti9FncPNtnAJ2RzT8M+HSv?= =?us-ascii?q?5l80i9xzmAygHT6uVAIU8ujqfbJJshzaQxlpoXq0jMAij2mEDugK+Makok4vSo?= =?us-ascii?q?6/jgYrj+upCTLYp0igXnPqQqm8y/Gvg4PxMVX2mb/OS8zKfs8Vf4QLVMlP02k7?= =?us-ascii?q?PWvIrUJcQB9eaFBFpx34Fr1Ba+EzruhNAVmlEDNE0fJVSBgpS/aH/UJ/WtN/qy?= =?us-ascii?q?jxyTkTNwwPaOarbsDpTJKnHrn7LofLI74ElZnllghetD7o5ZX+lSaMn4XVX84Y?= =?us-ascii?q?TV?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BnBAA+HhJZhrHZVdFdHgYMGQYMgn+CG?= =?us-ascii?q?QeDYppBBoEmcoggjm+GJAKEZgdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzIIJ?= =?us-ascii?q?DAQICASMEGQEbHQEDAQsGBQs3AgIiAREBBQEcBhMbiW0BAwgFCKY3P4wIgWwYB?= =?us-ascii?q?QEcgwoFg1IKGScNVoJiAQEBAQEBBAEBAQEBAQEZAgYShgeCJIJnNIdtgl8FkSe?= =?us-ascii?q?MXpMZggSGLIJ1hkaSeBQfgRU1gSwvIAgZFUYZhEwPEAyCAyA2hjcFgjgBAQE?= X-IPAS-Result: =?us-ascii?q?A0BnBAA+HhJZhrHZVdFdHgYMGQYMgn+CGQeDYppBBoEmcog?= =?us-ascii?q?gjm+GJAKEZgdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzIIJDAQICASMEGQEbH?= =?us-ascii?q?QEDAQsGBQs3AgIiAREBBQEcBhMbiW0BAwgFCKY3P4wIgWwYBQEcgwoFg1IKGSc?= =?us-ascii?q?NVoJiAQEBAQEBBAEBAQEBAQEZAgYShgeCJIJnNIdtgl8FkSeMXpMZggSGLIJ1h?= =?us-ascii?q?kaSeBQfgRU1gSwvIAgZFUYZhEwPEAyCAyA2hjcFgjgBAQE?= X-IronPort-AV: E=Sophos;i="5.38,316,1491256800"; d="scan'208,217";a="272385951" Received: from mail-ua0-f177.google.com ([209.85.217.177]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 09 May 2017 21:56:26 +0200 Received: by mail-ua0-f177.google.com with SMTP id g49so12768737uaa.1 for ; Tue, 09 May 2017 12:56:26 -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=87WFGtx0vC06O7aNJzFv+JddWGBSDwtJWVhpyWDX+g0=; b=TXekDNmK8kkLzR22ZrFcSVoIsJtqP5MzDgsw/8hBTCJQnsCc+9K//bKrEO0B810g6B iHw5iiXKNCk3inpHdTLDd9b65DKhoAxPSEVNoXEE58Yo9ePRrC6qhNT9iq2t0Sazgdfh YLg6ZoJ2FCwHXzf3Gd1WkT01+dCWkxGW3KEuZUlpdGgKG5n8+2+4hkrsIJSb/GFDVkJ9 EUDN14fkHnIHkViGRftnEhyYPPhW5Zbb/GF+kyUAiNsVlgz364wiuI0EBGZLfwX1vxkG etdNH798WqUzKIkHrcXfKuVAKX9eCKzOqjXfHhaj6YEj+9H9MzQjhLrIQngLEZz0NfSI focA== 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=87WFGtx0vC06O7aNJzFv+JddWGBSDwtJWVhpyWDX+g0=; b=Y840VYG1cnDNDMe7nW5LjYKLllf2G1WWz6p078hIjwrikjkMrwQ3FJaYUBdGqyxL34 vqtVN+oM5qZiaw6MwY6GwYYznu1RFQW6ogStudi8eIBjyrZJueEQYkh5oyE7uXzc0WZ/ xmssY+Dusq+NLUKpXxJOh4bdpVkBdi49XY8VZSuj+17R+N0PfPXF968tm5qYZkrZQu13 guQ3qdBTsrYHTyOzSxzF//1aaQRbwadD5RTtBAYbyximSZLVo6K8CWG5MUepAHVJ9OTA 8jvOVUAGW9SOwKSTbkrKMoRZq8OXQlLhciI/vlTcQBG73k9hOMLLR5AmC8Xpp1C+NTNp 8fPA== X-Gm-Message-State: AODbwcDJsw6HvQjVbTgvBabq3FK4PmAhTSkLwzbWaQKdbHXdAW+K/8Z2 KPMvNl+Axq7pnral9MMTo1iBOwdRld8tJVVIIw== X-Received: by 10.176.78.161 with SMTP id l33mr859830uah.24.1494359784788; Tue, 09 May 2017 12:56:24 -0700 (PDT) MIME-Version: 1.0 Received: by 10.31.2.19 with HTTP; Tue, 9 May 2017 12:56:24 -0700 (PDT) In-Reply-To: <1494320088.2074838.970492485.42DF8438@webmail.messagingengine.com> References: <1494320088.2074838.970492485.42DF8438@webmail.messagingengine.com> From: Reed Wilson Date: Tue, 9 May 2017 12:56:24 -0700 Message-ID: To: Leo White Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f403043ee8e023994b054f1cc0c0 X-Validation-by: cedilla@gmail.com Subject: Re: [Caml-list] Type generalization confusion --f403043ee8e023994b054f1cc0c0 Content-Type: text/plain; charset=UTF-8 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" 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 > > > --f403043ee8e023994b054f1cc0c0 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
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 solutio= n 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:

=C2=A0 type (_,_) field =3D
=C2=A0= | Int8 :=C2=A0('a,'b) field -> ((int -> 'a),'b) fiel= d
=C2=A0 | String :=C2=A0(int * ('a,'b) field) -> ((st= ring -> 'a),'b) field
=C2=A0 | End :=C2=A0('b,'= ;b) field

=C2=A0 let intstring =3D Int8 (String (3= , End))

In this case, intstring wou= ld be used as a template for reading/writing an 8-bit integer, followed by = a 3-byte long string. The type would be:
=C2=A0 val intstring : (= int -> string -> 'a, 'a) field

My reading/writing functions are= of the type:
=C2=A0 val to_chan : ('a, unit) fiel= d -> out_channel -> 'a
=C2= =A0 val of_chan :=C2=A0('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 re= sults in a type:
=C2=A0 val intstring_to_ch= an :=C2=A0out_channel -> int -> string -> unit
=C2=A0 val intstring_of_chan :=C2=A0(int -> string -> &#= 39;_a) -> in_channel -> '_a

<= /div>
(Note that the non-generalization of intstr= ing_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 b= y the length of some of the fields. For example:

=C2= =A0 let lookup_array =3D [| String (0, End);=C2=A0String (1, End) |]
<= div class=3D"gmail_extra">=C2=A0 let lookup_fun i =3D String (i, End)
=

These end up being the following types:
= =C2=A0 val lookup_array : (string -> '_a, '_a) field array
=
=C2=A0 val lookup_fun : int -> (string -> 'a, 'a) field<= /div>

The lookup array is nongeneralized. The func= tion works, but I'll be using this in a very tight loop which is extrem= ely 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&#= 39;t work)

No number o= f "+" or "-" in my type parameters fix the issue as the= y did with the example in my previous e-mail. Everything returns:
=
=C2=A0 Error: In this= GADT definition, the variance of some parameter cannot be checked

Thanks again f= or 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.

<= /div>

=
On May 9, 2017 01:55, "Leo White" <= leo@lpw25.net> wr= ote:
> But this similar type has no problem:
> =C2=A0type 'a field =3D Int of int
> =C2=A0let a =3D Int 3
> =C2=A0let b =3D 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 po= sitions 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:

=C2=A0 type +_ field =3D Int : int -> 'a field
=C2=A0 let a =3D Int 3
=C2=A0 let b =3D Int (1 + 2)

gives:

=C2=A0 type +_ field =3D Int : int -> 'a field
=C2=A0 val a : 'a field =3D Int 3
=C2=A0 val b : 'a field =3D Int 3

Regards,

Leo


--f403043ee8e023994b054f1cc0c0--