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 9C5AA7FA5E for ; Tue, 9 May 2017 07:43:52 +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-f175.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.175; 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.175 as permitted sender) identity=mailfrom; client-ip=209.85.217.175; 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-f175.google.com) identity=helo; client-ip=209.85.217.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cedilla@gmail.com"; x-sender="postmaster@mail-ua0-f175.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AzI1XExZH5UGhuFByR08nFPD/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZoMiybnLW6fgltlLVR4KTs6sC0LuK9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhz?= =?us-ascii?q?sGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVSNBDIOy?= =?us-ascii?q?YYUMAeQcI+hXs5LwqEESoRakHwSgGP/jxz1Oi3Tr3aM6yeMhEQTe0QI8Ad0Brm?= =?us-ascii?q?nbp8j1O6cTVeC1167IzTPeZP5RxTjy9pXHchElofGIR719asXRyUw1GAPEilWc?= =?us-ascii?q?s5DqPzSQ1ukUtWWQ8uluVfq3hmI5tw18piKjy8Qsh4XTmI4Z11LJ+T9kzIs3Jd?= =?us-ascii?q?C1TlNwb8S+H5tKrS6aMpN7QsM8TGFsvyY30rgGtoS6fCgO0Zgn2gTQZ+Cef4iG?= =?us-ascii?q?/x7uVuacLS13hHJif7K/iBKy/la6xuLgUcm01U5GritDktbSqnAAzwLf5tSDR/?= =?us-ascii?q?dn/Uqs2SyD2x7O5uxGO0w4iKjWJp45zr41jJUTsEDDHiHsmEXxia+bblkr9fa1?= =?us-ascii?q?5OTmZrXmooWTOpR7igH7KKsum8i/Df4kPQgJWmiX4f6826H7/U3lXLVKieU7nb?= =?us-ascii?q?XDv5DfIcQXv6q5Aw5O0oY/8Bu/FDen0NEAnXYdNl5FeRSHj5LoO17UOvz4A+2/?= =?us-ascii?q?0ByQl2JEzvrcP7DlSq7GLnXZna2pKbl04VRdxQ511ttf6ohZEJkOJfvyXgn6s9?= =?us-ascii?q?mOXTEjNAnh+evqBJ1C14cFXmTHVqSUPKLWtVag6ecmIu3Kb4gQ7mWuY8M57uLj?= =?us-ascii?q?2Cdq0WQWerOkiN5OMCi1?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AzAgAbVhFZhq/ZVdFbHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhQYSB4Nim29ylw+GJAKEYAdDFAEBAQEBAQEBAQEBEgEBAQgLCwg?= =?us-ascii?q?oL4IzIgGCPwEBAQECASMEGQEbHQEDAQsGBQQHDSoCAiEBAREBBQEcBhOKCAEDC?= =?us-ascii?q?AUIpWc/jAiBbBgFARyDCgWDWQoZJw1WgmIBAQEBAQEEAQEBAQEBARkCBhKIK4J?= =?us-ascii?q?nNIJUhRmCXwWRJ4whO45GhFORa4sqh04UH4EVNoErLyAIGRVGGYRMH4IPIDaId?= =?us-ascii?q?QEBAQ?= X-IPAS-Result: =?us-ascii?q?A0AzAgAbVhFZhq/ZVdFbHAEBBAEBCgEBFwEBBAEBCgEBhQY?= =?us-ascii?q?SB4Nim29ylw+GJAKEYAdDFAEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzIgGCPwEBA?= =?us-ascii?q?QECASMEGQEbHQEDAQsGBQQHDSoCAiEBAREBBQEcBhOKCAEDCAUIpWc/jAiBbBg?= =?us-ascii?q?FARyDCgWDWQoZJw1WgmIBAQEBAQEEAQEBAQEBARkCBhKIK4JnNIJUhRmCXwWRJ?= =?us-ascii?q?4whO45GhFORa4sqh04UH4EVNoErLyAIGRVGGYRMH4IPIDaIdQEBAQ?= X-IronPort-AV: E=Sophos;i="5.38,312,1491256800"; d="scan'208,217";a="272236422" Received: from mail-ua0-f175.google.com ([209.85.217.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 09 May 2017 07:43:51 +0200 Received: by mail-ua0-f175.google.com with SMTP id g49so63768506uaa.1 for ; Mon, 08 May 2017 22:43:51 -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=wOe+Ubln/S0q1IN1mwTm03Lqs0KqwCUahD0q2WbE96k=; b=tFTWKGIitpD+lnoaKP4d5n8sJHi/ODn/R2akrnSUZBQRdzcR8vIPpX+L3KvRgIi/EO o2HFFi+wrebXar8CjW3bd1D4gHftbxhaGQOXCzB48yZzq1Yg6G8eVkMMWvetjIMpqRkB 5RICXkmLQZvgo0Rqap4KcetCl+SWzWsSXv2eAQ9W5sYu4K6xtuWcur3N9pi9dabUIi6Y MIM+ZZ/QUBNNuNNAKukBHAfbTdxlRb9ZTpYVbhHfX5CLErc+/Rae8AatFPKZWEloaGEV L/WliFxOQ3qKu//J2Fr0W9eDB9iKp3AXt5qzACwAX8yzmWhE6Cn4qI4Ie6hZnDUrt2et gSDw== 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=wOe+Ubln/S0q1IN1mwTm03Lqs0KqwCUahD0q2WbE96k=; b=BDkXecYhkWo8HiSIDuowsHhn5Pojczr8r7sfODfaMEjbiG9TvoUTlcEdlGTVe5Wu1e 1iVAM/WA9+vcVv80qiOWWvtufZWcCV34V1ZWJw5JR5EDjGMEZuMJ66TWRaItVjqrIHE2 4YSjWPSryiC8znLpl9+sl/TuZEYITTs6zUs6y7wVCTzozHvWSurRPaWIsbS0VpAVCgsf xCvX3Tla/jPvT96MKlKt21USJR7Azd7Lf/MMv1zSDoBZ1xKMcdN5M15fZukrco7Meo4s Tl3T+iu76Uy9byLcUuqBODYfKMIa7g2T8ab0V/lugzRuU4Gf9yqjKH7gUBzXBTJgpSx4 TsxA== X-Gm-Message-State: AN3rC/72SZscQSfbZYfvIgoecOLH1MKzZAW3yOuCq0jZZXGMbP/uiE85 viMnB8oL0dB8SVVFbj4E7731BWhsHg== X-Received: by 10.159.48.144 with SMTP id j16mr23211046uab.131.1494308630352; Mon, 08 May 2017 22:43:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.31.2.19 with HTTP; Mon, 8 May 2017 22:43:49 -0700 (PDT) In-Reply-To: References: From: Reed Wilson Date: Mon, 8 May 2017 22:43:49 -0700 Message-ID: To: Gabriel Scherer Cc: caml users Content-Type: multipart/alternative; boundary=f403045e3eda18d958054f10d79f X-Validation-by: cedilla@gmail.com Subject: Re: [Caml-list] Type generalization confusion --f403045e3eda18d958054f10d79f Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable But this similar type has no problem: type 'a field =3D Int of int let a =3D Int 3 let b =3D Int (1 + 2) Both a and b receive the same generalized type. Why does the GADT style prevent this from occuring? On Mon, May 8, 2017 at 8:49 PM, Gabriel Scherer wrote: > This is the value restriction at work: only values are generalized > (often of the form "fun x -> ..."), and while (Int 3) is a value, (Int > (1 + 2)) is not. > > On Mon, May 8, 2017 at 11:32 AM, Reed Wilson wrote: > > I've been working with some of the new features introduced with GADTs, > and > > ran into a confusing instance of the "type variables that cannot be > > generalized" error. > > > > The simplified program is as follows: > > type _ field =3D Int : int -> 'a field > > let a =3D Int 3 > > let b =3D Int (1 + 2) > > let inside =3D 1 + 2 > > let c =3D Int inside > > > > ocamlc -i returns: > > type _ field =3D Int : int -> 'a field > > val a : 'a field > > val b : '_a field > > val inside : int > > val c : 'a field > > > > with b remaining non-generalized. The problem I'm having with it is that > the > > type variable doesn't depend on the value at all, so I don't see how th= at > > can prevent generalization. > > > > Also, the manual says the reason some types aren't generalized is due to > > "polymorphic mutable data structures". Nothing I created is mutable, so > why > > was generalization turned off in the first place? > > > > Finally, I'm confused why separating the function from the definition is > > enough to fix this; c is generalized simply by defining 1+2 in a separa= te > > value (which must be global, apparently). > > > > Thanks, > > Reed Wilson > > > > -- > > =C3=A7 > --=20 =C3=A7 --f403045e3eda18d958054f10d79f Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
But this similar type has no problem:

t= ype 'a field =3D Int of int
let a =3D Int 3
let b = =3D Int (1 + 2)

Both a and b receive the same gene= ralized type. Why does the GADT style prevent this from occuring?

On Mon, May 8, = 2017 at 8:49 PM, Gabriel Scherer <gabriel.scherer@gmail.com>= ; wrote:
This is the value restric= tion at work: only values are generalized
(often of the form "fun x -> ..."), and while (Int 3) is a val= ue, (Int
(1 + 2)) is not.

On Mon, May 8, 2017 at 11:32 AM, Reed Wilson <cedilla@gmail.com> wrote:
> I've been working with some of the new features introduced with GA= DTs, and
> ran into a confusing instance of the "type variables that cannot = be
> generalized" error.
>
> The simplified program is as follows:
> type _ field =3D Int : int -> 'a field
> let a =3D Int 3
> let b =3D Int (1 + 2)
> let inside =3D 1 + 2
> let c =3D Int inside
>
> ocamlc -i returns:
> type _ field =3D Int : int -> 'a field
> val a : 'a field
> val b : '_a field
> val inside : int
> val c : 'a field
>
> with b remaining non-generalized. The problem I'm having with it i= s that the
> type variable doesn't depend on the value at all, so I don't s= ee how that
> can prevent generalization.
>
> Also, the manual says the reason some types aren't generalized is = due to
> "polymorphic mutable data structures". Nothing I created is = mutable, so why
> was generalization turned off in the first place?
>
> Finally, I'm confused why separating the function from the definit= ion is
> enough to fix this; c is generalized simply by defining 1+2 in a separ= ate
> value (which must be global, apparently).
>
> Thanks,
> Reed Wilson
>
> --
> =C3=A7



--
=
=C3=A7
--f403045e3eda18d958054f10d79f--