caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Romain <postmaster@doomeer.com>
To: caml-list@inria.fr
Subject: Re: [Caml-list] using a restricted subset of a polymorphic variant
Date: Thu, 10 Sep 2015 11:22:34 +0200	[thread overview]
Message-ID: <55F14BDA.7090309@doomeer.com> (raw)
In-Reply-To: <CAFrFfuFJqPfhkWgvdwr+vDsOYbwAi1GhEfOn-Tcttjd1yFiuOA@mail.gmail.com>

>    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

      parent reply	other threads:[~2015-09-10  9:22 UTC|newest]

Thread overview: 8+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-09-10  9:07 Martin DeMello
2015-09-10  9:12 ` Gabriel Scherer
2015-09-10  9:13 ` Edouard Evangelisti
2015-09-10 18:03   ` Martin Jambon
2015-09-10 19:14     ` Martin DeMello
2015-09-10  9:13 ` Christoph Höger
2015-09-10  9:19 ` Jacques Garrigue
2015-09-10  9:22 ` Romain [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=55F14BDA.7090309@doomeer.com \
    --to=postmaster@doomeer.com \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).