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 ESMTP id 7461B7F72E for ; Mon, 15 Aug 2016 09:26:27 +0200 (CEST) IronPort-PHdr: 9a23:6PKZsBUJIKTZusuf+zDJakdbHIjV8LGtZVwlr6E/grcLSJyIuqrYZxSCt8tkgFKBZ4jH8fUM07OQ6PG5HzVcqs/Y7jhCKMUKDE5dz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx/q+2+36wZDPeQIA3GP7OuIrakzq5lyI6IFW2dIkcfdpjEOR4zNhQKd//StQP1WdnhLxtI+b3aVI1GBugc8n7NNKSq7gfq41HvRyBTUiNH0ptoWw7UGQBSPG3HYXU30XnxxUGECFqUiiBtai+hf948N51TmXLIXbQrcuXirqu6pvRRT0kioIHzo4632RkNEm34xBpxf0hRV02pPZe8m6PeBkf6zAcJtOSmNbRMdeSiFpB4qgb80JBuUGLO8dss/0rB0MtU3tVkGXGOrzx2oQ1TfN1qog3rFkSFme0Q== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DuAQB3bbFX/wWCBoVehBt2Brk3gX0BH4V9AoFuFAIBAQEBAQEBAV0ngjIEARMBghQBBSMdAwE1AQEOBQYOCgICGA4CAlcGJIgfCrBrZ4REBwKHNRqDewEBAQEBAQQBAQEBAQEBAQEVAQiBAYchCIJNhECDASuCL4Y8B4hRii+GHoh4gjmNCogRIBaDcIN4HjaCRYFEX4cPAQEB X-IPAS-Result: A0DuAQB3bbFX/wWCBoVehBt2Brk3gX0BH4V9AoFuFAIBAQEBAQEBAV0ngjIEARMBghQBBSMdAwE1AQEOBQYOCgICGA4CAlcGJIgfCrBrZ4REBwKHNRqDewEBAQEBAQQBAQEBAQEBAQEVAQiBAYchCIJNhECDASuCL4Y8B4hRii+GHoh4gjmNCogRIBaDcIN4HjaCRYFEX4cPAQEB X-IronPort-AV: E=Sophos;i="5.28,524,1464645600"; d="scan'208";a="231482676" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 15 Aug 2016 09:26:24 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id EB7166397 for ; Mon, 15 Aug 2016 16:26:21 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8218A3974; Mon, 15 Aug 2016 16:26:21 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=kWTnDz1vSASpbCYx8ed7VIYHyqo=; b=PGszSBm77DCSTPqz8qFrkVpEqZUR KZ3DfVi+YNMYyeLiwpT3qexTKXDZG5Aoy8o3yE1Hcbe2e3Cy5JpUENQN+JIHgisS ri/aHWoD6QVhyizC1iCxyCDo3rPFW70b1LpyZZaH4fEWp2sZsR7oM8R49y52pkrV h53NPiNjjmVvIxg= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:X-Priority:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=XwfIq6xl0kyUGTsl4jWOKj965gvn2dzTGBHLW1ndbWCXufnRXItu8TJ0LczsXScO4ntETnnb8LCNOVA63GejD7otgIMezLBLujeKJ7YlxmqBvd/66jpwXFLZ9Sw/+GjZqSkgyg5DV6OhZQO9YwrivyHm4k0ZvQqhUFrAcpDwbr8=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 37E101521; Mon, 15 Aug 2016 16:21:43 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue X-Priority: 3 (Normal) In-Reply-To: <1471216950.691509807@f313.i.mail.ru> Date: Mon, 15 Aug 2016 16:26:22 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <66256FBC-26D2-4274-887E-178520DE66B3@math.nagoya-u.ac.jp> References: <1471216950.691509807@f313.i.mail.ru> To: Alexey Egorov X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] difference between locally abstract types and polymorphic annotations? On 2016/08/15 08:22, Alexey Egorov wrote: >=20 > Hello, >=20 > I'm noticed that GADT typechecking depends on whether free variables are = annotated as locally abstract types (in form of "type a b c . ") = or just polymoprhic annotations (in form of " 'a 'b 'c . "). >=20 > Code here - http://pastebin.com/36ZAjw0J=20 >=20 > What is the difference? I was thinking that both of this are equivalent, = isn't it? >=20 > Thanks. They are not equivalent. Polymorphic annotations are about checking, a posteriori, that some types a= re indeed polymorphic, and also about allowing polymorphic recursion. Locally abstract types are about creating an abstract type and using it loc= ally. It will be turned into a type variable when you leave the scope. Only= abstract types can be refined by GADT pattern matching, not type variables. Using GADTs, you often want both refinement and polymorphic recursion, this= is why =E2=80=9Ctype a b c. =E2=80=9D is actually a combination o= f the two. Jacques=