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 2C27F7FA5E for ; Tue, 9 May 2017 22:54:48 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f174.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.220.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 209.85.220.174 as permitted sender) identity=mailfrom; client-ip=209.85.220.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-qk0-f174.google.com) identity=helo; client-ip=209.85.220.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qk0-f174.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A7bRMvxzgeg0ITOnXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?1OkRIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiS?= =?us-ascii?q?cIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CR2VBUMZfWSJCDI2h?= =?us-ascii?q?cYUAE/EMPfpEo4Tnu1cCsQeyCAuqCejyyjFInHj23agi3uolDw7GxhIvH9cOsX?= =?us-ascii?q?/Jrtr6LqMSUeSyzKnQ0D7OaPNX1i356IjMdRAhueqBXb11ccXLyEkvExnJgUmX?= =?us-ascii?q?qYzgJj6Y0PkGvWuD7+d4S+6jl2oqpxtyrzWv3MsglJfFip4PxlzZ9yh0z4A4Ls?= =?us-ascii?q?CiRkFhe96rCp5QujmaN4RoRsMiRHlluCMgxb0HvZ63ZTEKyJc7yxLGZfyLboqF?= =?us-ascii?q?7x35WOaeJjd4g31leLahiBqo7Uegzej8WtG10FZMsCVFjsHBum4R2xHX8MSKSf?= =?us-ascii?q?tw8l2/1TqRywzf8PxILEI7mKbDLp4u2L8wlp4dsUTZGS/2nV37ja+MeUUg/uio?= =?us-ascii?q?7Pznb67ppp+ZLYB0iwX+Pr4ylcy4BOQ0KhIOUHSD+eSgyL3j+lX0T6lQgf0zlq?= =?us-ascii?q?nVqZTaJcUApq6lGAJVyYYi6xOnDzi8ytgYnH8HLEhEeB2dlYTpNUvOc7jECqKF?= =?us-ascii?q?jlmg2Ahqw+vBOPW1CZjBL3zHmZ/ueL987whXzw9lnv5F4JcBKLwbLffiEn74sN?= =?us-ascii?q?jfFldtIgWwx+H/INp434IaH2mIB/nKY+vprVaU67d3cKG3b4gPtWO4cqB96g?= =?us-ascii?q?=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AZBQBELBJZf67cVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhQYSB4Nim21ylw+GJAKEZgdDFAEBAQEBAQEBAQEBEgEBCQsLCCY?= =?us-ascii?q?xQhABgWAiAYI/AQEBAQIBIwQZARsdAQMBCwYFCwMKAgImAgIhAQERAQUBHAYTi?= =?us-ascii?q?ggBAw0IpkI/jAiBbBgFARyDCgWDUwoZJw1WgmIBAQEBAQUBAQEBARsCBhJ5hzK?= =?us-ascii?q?CZzSCVIUZgl8FnUo7jkaEU4gwiTuLKodOFB+BFTaBKy8gCBkVRhmETA8cgWQ/N?= =?us-ascii?q?oNHhS0BAQE?= X-IPAS-Result: =?us-ascii?q?A0AZBQBELBJZf67cVdFdHAEBBAEBCgEBFwEBBAEBCgEBhQY?= =?us-ascii?q?SB4Nim21ylw+GJAKEZgdDFAEBAQEBAQEBAQEBEgEBCQsLCCYxQhABgWAiAYI/A?= =?us-ascii?q?QEBAQIBIwQZARsdAQMBCwYFCwMKAgImAgIhAQERAQUBHAYTiggBAw0IpkI/jAi?= =?us-ascii?q?BbBgFARyDCgWDUwoZJw1WgmIBAQEBAQUBAQEBARsCBhJ5hzKCZzSCVIUZgl8Fn?= =?us-ascii?q?Uo7jkaEU4gwiTuLKodOFB+BFTaBKy8gCBkVRhmETA8cgWQ/NoNHhS0BAQE?= X-IronPort-AV: E=Sophos;i="5.38,316,1491256800"; d="scan'208";a="272391014" Received: from mail-qk0-f174.google.com ([209.85.220.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 09 May 2017 22:54:29 +0200 Received: by mail-qk0-f174.google.com with SMTP id k74so12240643qke.1 for ; Tue, 09 May 2017 13:54:29 -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=atEUQn2/0SEmQ8iWGPN8eSGh95CbmruRawVMFMUQscQ=; b=r+3x35C22u7d53qxrLD0xpyIiB/ZX3Rltdf2kQz52c4Nxy7CeHFoKs9DWfwoxHEIkf t92Ln3vuRCAlLj6lJXHvV2VhRFfKqW/1dtQgDpGkILvY7g/8kBhnmELVORcColoU+yoC 7Ha3IVcR0usR/9y0XyQ+Mgz52OTlNDktpQ+6XZ2JvCMmD7ygkmS1BzeqEy9vPSvoFdM0 StZjQpzFGH0biOVCqewZzxKOMY9bf2PWHM/wAcgz8G+5YNQatV8qnxL0Z91Mp0fYkkXT idjxrZWjTWTDFi+fgPYMJ96N9Ca8pnIdw4v+L7AEGqWeK5qMc7YGQSsZtxNa9BWof1pX bfew== 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=atEUQn2/0SEmQ8iWGPN8eSGh95CbmruRawVMFMUQscQ=; b=pTl/moQpLRFPuc99erBRQxGNAQPMziOuMpmPbGUd+4m+g7q+VPdTeuJSw9Ri33MYIX v56cxPYKBGC176EMdaykuv9W6x/jUxj+gyLgrBiG1fPOhYvbGEUEhnQZxeyWHuAm1qmA 4ErCLKqLA34f8yxwGNMo2hbkrTmwGcdNg7SUvYGwzrbMpYUPMxWGz+qfa+hYhfy+zTaA NweMAV6VPhIAYBhYYSJnfeaapSb6k2zjlwWUP9UDazG+cKTW9DBNzr0I6Ucc9ciJa5RX zFl15TcxQAw5BgYz6SCZWB6ADUnb34owrMRW8bsZqiMdIdU+KhXpGeP/OFJACxTE/QZU yV8w== X-Gm-Message-State: AODbwcB2ppnCT1sA7MolHko1u2CkHEn+mbtJ10XaATQBRFKf3kHyibYt hMP7LWNfUV4Z4WYRHtosaHS5Iu8VpU5y X-Received: by 10.55.143.129 with SMTP id r123mr2304929qkd.98.1494363268191; Tue, 09 May 2017 13:54:28 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.185.70 with HTTP; Tue, 9 May 2017 13:54:27 -0700 (PDT) In-Reply-To: References: <1494320088.2074838.970492485.42DF8438@webmail.messagingengine.com> From: Jeremy Yallop Date: Tue, 9 May 2017 21:54:27 +0100 Message-ID: To: Reed Wilson Cc: Leo White , Caml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Type generalization confusion On 9 May 2017 at 20:56, Reed Wilson wrote: > type (_,_) field = > | Int8 : ('a,'b) field -> ((int -> 'a),'b) field > | String : (int * ('a,'b) field) -> ((string -> 'a),'b) field > | End : ('b,'b) field [...] > 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 Indeed, soundness requires the parameters of 'field' to be invariant, so there's no possibility of adding variance annotations here. For example, the type of the End constructor makes the following definition well typed: let x : (< m : int >, < m : int >) field = End If one of the parameters (the first, say) were covariant, then that parameter could be coerced to a supertype of < m:int >, like this let y = (x :> ( < >, < m : int >) field) and then matching against y would introduce an invalid equality between < > and < m: int >: match y with End -> (* Here the type checker knows by the type of End that the two type parameters are equal, i.e. that < > is equal to < m : int > *) let x = (object end) in x#m + 1 A similar argument can be made against making either parameter contravariant. The parameters of 'field' are therefore invariant, and so the relaxed value restriction doesn't apply. > 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.