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 618C47FA5E for ; Tue, 9 May 2017 10:54:53 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=leo@lpw25.net; spf=None smtp.mailfrom=leo@lpw25.net; spf=None smtp.helo=postmaster@out4-smtp.messagingengine.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=pra; client-ip=66.111.4.28; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=mailfrom; client-ip=66.111.4.28; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@out4-smtp.messagingengine.com) identity=helo; client-ip=66.111.4.28; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="postmaster@out4-smtp.messagingengine.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Am3vI7hPaUc+v1x4lkLsl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0LPr7rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPde?= =?us-ascii?q?RWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbY?= =?us-ascii?q?UwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhS?= =?us-ascii?q?kENzA37m7YhMNsg6xcoh2vqRJ/zZPPbY6PNvdzZLnQcMkGSWdDWMtaSixPApm7?= =?us-ascii?q?b4sKF+cPO/hXr47grFQOrRu+BBWsC/3ywTJPgn/5w6o63v8lEQHe0g0sAdIDvG?= =?us-ascii?q?7SrNrrKKcfSOa4x7TLwzXbd/5b2Dbw5JLVfhw8vP2AR719fdDPxUQsEQ7Ok0+e?= =?us-ascii?q?ppb/PzyP0+QAq2ib4PRkVeKok2MnrBxxoiSgy8s1kYnJg54Vykje+SV83ok1Ps?= =?us-ascii?q?a4R1R0Yd6lFptQuD+VN415QsMjRWFnpjw2xaEBuZ6+ZCQKyZInyADDa/GfcoWF?= =?us-ascii?q?4wjvWPuMLTtlnn5od6iziwix/ES4z+3zTMi00FJEripfldnMs2gA1xjN5ciAUf?= =?us-ascii?q?Z9+l+h2DiR2w3T8O1EJ147lbbDJ5473rEwjoYTsVjEHiLuhEr5lqqWdkE99uis?= =?us-ascii?q?6uTneanmq4SHN450jwH+Kr4hlta+AeQ+KAgOXnKU9f6y1L35rgXFR+BBh/gy16?= =?us-ascii?q?3Yq4zyJMIBp6f/DRUG/Jwk7kObAjDu79QZgXRPeFZIfzqDl5ezZhfILeyuXqT3?= =?us-ascii?q?uEiljDo+n6OOBbbmGJiYdnU=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BMBADEghFZhxwEb0JbHgYMGAEFAQsBg?= =?us-ascii?q?n+CGYNpiwuQQyGVcoIPhiQChGdBFgEBAQEBAQEBAQEBEgEBAQgNCQgoL4IzIIJ?= =?us-ascii?q?DAQICASMEGQEBOAQLCwQBMA0CAiwrijIIsU5rgWw6gwkBAQWFTIIbAQEBAQYBA?= =?us-ascii?q?QEBARsIiD02gmWFL4I+LoIxngcBpQSUQCYOgS1PLApGhGUfggskNoY4BYI4AQE?= =?us-ascii?q?B?= X-IPAS-Result: =?us-ascii?q?A0BMBADEghFZhxwEb0JbHgYMGAEFAQsBgn+CGYNpiwuQQyG?= =?us-ascii?q?VcoIPhiQChGdBFgEBAQEBAQEBAQEBEgEBAQgNCQgoL4IzIIJDAQICASMEGQEBO?= =?us-ascii?q?AQLCwQBMA0CAiwrijIIsU5rgWw6gwkBAQWFTIIbAQEBAQYBAQEBARsIiD02gmW?= =?us-ascii?q?FL4I+LoIxngcBpQSUQCYOgS1PLApGhGUfggskNoY4BYI4AQEB?= X-IronPort-AV: E=Sophos;i="5.38,313,1491256800"; d="scan'208,217";a="272276230" Received: from out4-smtp.messagingengine.com ([66.111.4.28]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 09 May 2017 10:54:52 +0200 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id 32E75209EA for ; Tue, 9 May 2017 04:54:49 -0400 (EDT) Received: from web4 ([10.202.2.214]) by compute5.internal (MEProxy); Tue, 09 May 2017 04:54:49 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lpw25.net; h= content-transfer-encoding:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-sender :x-me-sender:x-sasl-enc; s=mesmtp; bh=j4abdUmf9AnRR6TApu7R02x+Jf 1QIUyyCA19JAdi88Q=; b=dFhPBywsqYq5BkZOieYR8Uq5TquIfcfHb07Kp5jc40 soBp2oXptKKTc+T/PC1PQqB7hewjc8DRpiC+eqmfkiDbwcHntQ49p1usUV5xSn8g 4MYT83y0AQw75zYaOEdIamjqQOkdIf9YMvNUadZkNABpl78ANCPMkOZN4jit6omY I= DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-sender:x-me-sender:x-sasl-enc; s=fm1; bh=j4abdU mf9AnRR6TApu7R02x+Jf1QIUyyCA19JAdi88Q=; b=iWGWwHyqzZ0H57fagNxLM7 F+PVAlVS3jCxfjfVvo5OyCM2g99NiIsh3b/9Qt2Octn/8UeIuQeR7zz0jAhcwPlV 8hv8yu9QInXtvmafzGLaHSvypVm3sGdE0/Z/0raM71GslZgzH27+PCbfzfEpgZ0F Os3Y3sbtSuLeUY29Q8v4HLl19ckkNOQG+Wno6Xy7F9VWRonESNsUUZdEqHrY7t4u YCHYdqQoHsTfD2dr0wcPHAZKEFNLKf57iXuVtVISXEwrupILeYD6FdsHUcQOUt6S A7zTVoQr3WEY9sGZ2SvQWMv+FE5HIEF4ykxeYo3O/qeio72cRf1IV6SZVl0yyt4w == X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 11AC4BAB6F; Tue, 9 May 2017 04:54:49 -0400 (EDT) Message-Id: <1494320088.2074838.970492485.42DF8438@webmail.messagingengine.com> From: Leo White To: caml-list@inria.fr MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: multipart/alternative; boundary="_----------=_149432008820748384" X-Mailer: MessagingEngine.com Webmail Interface - ajax-6cc55fe1 In-Reply-To: Date: Tue, 09 May 2017 04:54:48 -0400 References: Subject: Re: [Caml-list] Type generalization confusion This is a multi-part message in MIME format. --_----------=_149432008820748384 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" > 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 --_----------=_149432008820748384 Content-Transfer-Encoding: 7bit Content-Type: text/html; charset="utf-8"
> 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


--_----------=_149432008820748384--