From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
To: OCaml List <caml-list@inria.fr>
Subject: [Caml-list] Propagating types to pattern-matching
Date: Tue, 15 Jan 2013 14:59:34 +0900 [thread overview]
Message-ID: <A597868B-9524-4233-92C1-BA4ED411644F@math.nagoya-u.ac.jp> (raw)
Dear Camlers,
It is a bit unusual, but this message is about changes in trunk.
As you may be aware from past threads, since the introduction of GADTs
in 4.00, some type information is propagated to pattern-matching, to allow
it to refine types.
More recently, types have started being used to disambiguate constructors
and record fields, which means some more dependency on type information
in pattern-matching.
However, a weakness of this approach was that propagation was disabled
as soon as a pattern contained polymorphic variants. The reason is that
typing rules for polymorphic variants in patterns and expression are subtly
different, and mixing information without care would lose principality.
At long last I have removed this restriction on the presence of polymorphic
variants, but this has some consequences on typing:
* while type information is now propagated, information about possibly
present constructors still has to be discarded. For instance this means that
the following code will not be typed as you could expect:
let f (x : [< `A | `B]) = match x with `A -> 1 | _ -> 2;;
val f : [< `A | `B > `A ] -> int
What happens is that inside pattern-matching, only required constructors
are propagated, which reduces the type of x to [> ] (a polymorphic variant
type with any constructor…)
As before, to give an upper bound to the matched type, the type annotation
must be inside a pattern:
let f = function (`A : [< `A | `B]) -> 1 | _ -> 2;;
val f : [< `A | `B ] -> int = <fun>
* the propagation of type information may lead to failure in some cases that
where typable before:
type ab = [ `A | `B ];;
let f (x : [`A]) = match x with #ab -> 1;;
Error: This pattern matches values of type [? `A | `B ]
but a pattern was expected which matches values of type [ `A ]
The second variant type does not allow tag(s) `B
During pattern-matching it is not allowed to match on absent type constructors,
even though the type of the patterns would eventually be [< `A | `B], which allows
discarding `B. ([? `A | `B] denotes a type obeying the rules of pattern-matching)
* for the sake of coherence, even if a type was not propagated because it
was not known when typing a pattern-matching, we are still going to fail if a
matched constructor appears to be absent after typing the whole function.
(This only applies to propagable types, i.e. polymorphic variant types that
contain only required constructors)
In particular the last two points are important, because previously such uses
would not have triggered even a warning.
The idea is that allowing propagation of types is more important than
keeping some not really useful corner cases, but if this is of concern
to you, I'm interested in feedback.
Jacques Garrigue
next reply other threads:[~2013-01-15 5:59 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-01-15 5:59 Jacques Garrigue [this message]
2013-02-11 15:31 ` Sebastien Mondet
2013-02-12 1:44 ` Jacques Le Normand
2013-02-12 2:28 ` Jacques Garrigue
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=A597868B-9524-4233-92C1-BA4ED411644F@math.nagoya-u.ac.jp \
--to=garrigue@math.nagoya-u.ac.jp \
--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).