From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
To: Alexey Egorov <electreg@list.ru>
Cc: OCaML List Mailing <caml-list@inria.fr>
Subject: Re: [Caml-list] difference between locally abstract types and polymorphic annotations?
Date: Mon, 15 Aug 2016 16:26:22 +0900 [thread overview]
Message-ID: <66256FBC-26D2-4274-887E-178520DE66B3@math.nagoya-u.ac.jp> (raw)
In-Reply-To: <1471216950.691509807@f313.i.mail.ru>
On 2016/08/15 08:22, Alexey Egorov wrote:
>
> Hello,
>
> I'm noticed that GADT typechecking depends on whether free variables are annotated as locally abstract types (in form of "type a b c . <typeexpr>") or just polymoprhic annotations (in form of " 'a 'b 'c . <typeexpr> ").
>
> Code here - http://pastebin.com/36ZAjw0J
>
> What is the difference? I was thinking that both of this are equivalent, isn't it?
>
> Thanks.
They are not equivalent.
Polymorphic annotations are about checking, a posteriori, that some types are indeed polymorphic,
and also about allowing polymorphic recursion.
Locally abstract types are about creating an abstract type and using it locally. 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 “type a b c. <typeexp>” is actually a combination of the two.
Jacques
prev parent reply other threads:[~2016-08-15 7:26 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-08-14 23:22 Alexey Egorov
2016-08-15 7:26 ` Jacques Garrigue [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=66256FBC-26D2-4274-887E-178520DE66B3@math.nagoya-u.ac.jp \
--to=garrigue@math.nagoya-u.ac.jp \
--cc=caml-list@inria.fr \
--cc=electreg@list.ru \
/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).