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 D49AE7F1AA for ; Thu, 10 Sep 2015 11:22:53 +0200 (CEST) IronPort-PHdr: 9a23:Cg3hJB8IU2SShP9uRHKM819IXTAuvvDOBiVQ1KB90e0cTK2v8tzYMVDF4r011RmSDdmdsq4MotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EleqKsRsb7tIee6aObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+C1Vv7cl9tVceaT8ZaUxC7JCXxo8NGVg3sruvBjFBV+X4WAAV2wNjhdSKwTC6xT3U423uSz/4LkukBKGNNH7GOhnEQ+p6L1mHUfl Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=postmaster@doomeer.com; spf=None smtp.mailfrom=postmaster@doomeer.com; spf=None smtp.helo=postmaster@mo4.mail-out.ovh.net Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@doomeer.com) identity=pra; client-ip=178.32.228.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="postmaster@doomeer.com"; x-sender="postmaster@doomeer.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@doomeer.com) identity=mailfrom; client-ip=178.32.228.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="postmaster@doomeer.com"; x-sender="postmaster@doomeer.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mo4.mail-out.ovh.net) identity=helo; client-ip=178.32.228.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="postmaster@doomeer.com"; x-sender="postmaster@mo4.mail-out.ovh.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CEAADlSvFVnATkILKIY6V4BpQFAQ2HcAIMgTQ4FAEBAQEBAQEBEAEBAQEBBg0JCSEugh2CBwEBAwEDIBVABgsLGgIFFgsCAgkDAgECAUUTCAKIIgwBtwGQIIN7ASuBIoUKhBqBKIUTFxqCOIFEBJVWgUiONZd1HwEBhESJOAEBAQ X-IPAS-Result: A0CEAADlSvFVnATkILKIY6V4BpQFAQ2HcAIMgTQ4FAEBAQEBAQEBEAEBAQEBBg0JCSEugh2CBwEBAwEDIBVABgsLGgIFFgsCAgkDAgECAUUTCAKIIgwBtwGQIIN7ASuBIoUKhBqBKIUTFxqCOIFEBJVWgUiONZd1HwEBhESJOAEBAQ X-IronPort-AV: E=Sophos;i="5.17,503,1437429600"; d="scan'208";a="176815112" Received: from mo4.mail-out.ovh.net ([178.32.228.4]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 10 Sep 2015 11:22:53 +0200 Received: from mail631.ha.ovh.net (b9.ovh.net [213.186.33.59]) by mo4.mail-out.ovh.net (Postfix) with SMTP id DD0E0FF9C58 for ; Thu, 10 Sep 2015 11:22:52 +0200 (CEST) Received: from localhost (HELO queueout) (127.0.0.1) by localhost with SMTP; 10 Sep 2015 11:22:51 +0200 Received: from amontsouris-652-1-86-122.w92-163.abo.wanadoo.fr (HELO ?192.168.1.15?) (postmaster@doomeer.com@92.163.109.122) by ns0.ovh.net with SMTP; 10 Sep 2015 11:22:38 +0200 Message-ID: <55F14BDA.7090309@doomeer.com> Date: Thu, 10 Sep 2015 11:22:34 +0200 From: Romain User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.7.0 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Ovh-Tracer-Id: 5466806999302531616 X-Ovh-Remote: 92.163.109.122 (amontsouris-652-1-86-122.w92-163.abo.wanadoo.fr) X-Ovh-Local: 213.186.33.20 (ns0.ovh.net) X-OVH-SPAMSTATE: OK X-OVH-SPAMSCORE: 0 X-OVH-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeekgedrudeiucetufdoteggucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenuc X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: 0 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeekgedrudeiucetufdoteggucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenuc X-Validation-by: postmaster@doomeer.com Subject: Re: [Caml-list] using a restricted subset of a polymorphic variant > method get_heading = self#get_direction heading This unifies heading (which has type [`Up | `Down]) with type dir, but types [`Up | `Down] and dir cannot be *unified*. However, [`Up | `Down] is a subtype of dir, so [`Up | `Down] can be *coerced* to type dir: method get_heading = self#get_direction (heading :> dir) Unification cannot guess coercions, so you have to annotate them by hand. This may sound confusing, but I came up with an analogy some time ago which may help. (I'm probably not the only one who came up with it.) A type can be seen as a set of values. For instance type [`Up | `Down] denotes the set of values `Up and `Down. This set is included in the set denoted by dir. [`Up | `Down] is a "subset" of dir, except we don't say "subset" but "subtype". A polymorphic type can be seen as a set of types, i.e. a set of sets of values. Type [> `Up | `Down] denotes the set of all types which contain at least `Up and `Down. In particular, it contains [`Up | `Down]. So [> `Up | `Down] can be instantiated with [`Up | `Down]. Now you see that "is an instance of" is not the same as "is a subtype of": the first is inclusion between sets of sets of values, while the second is inclusion between sets of values. Hope this helps, -- Romain Bardou