From: Nathan Mishra Linger <nathan.mishralinger@gmail.com>
To: Alain Frisch <alain@frisch.fr>
Cc: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>,
OCaML List Mailing <caml-list@inria.fr>
Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs
Date: Mon, 29 Apr 2013 12:37:11 -0400 [thread overview]
Message-ID: <CAJO0BX1rQecYyHhfyNXv4BLhxF17ghFvUT_nAUWKoKzmMCF31g@mail.gmail.com> (raw)
In-Reply-To: <517E581A.20506@frisch.fr>
Our codebase at Jane Street would not suffer from the proposed fix.
In fact, we have previously wished the type system tracked injectivity of type
constructors. Because it didn't, we wrote Type_equal.Injective [^1] for cases
when we need to track injectivity ourselves.
[^1] https://ocaml.janestreet.com/ocaml-core/latest/doc/core/Type_equal.Injective.html
On Mon, Apr 29, 2013 at 7:23 AM, Alain Frisch <alain@frisch.fr> wrote:
> On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
>>
>> What I want to know is whether anybody is using GADTs in a way that
>> would be broken if we disallow type variables under abstract types
>> (other than the predefined ones) in the return type of GADTs.
>> I.e., for instance defining a type witness type involving such abstract
>> types.
>
>
> The only abstract types in the return type of GADTs in LexiFi's code base
> code are currently either non-parametrized ones or built-in types (array,
> lazy). So we'd be fine with the proposed fix (assuming that abstract types
> are not injective).
>
> -- Alain
>
>
> --
> Caml-list mailing list. Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
next prev parent reply other threads:[~2013-04-29 16:37 UTC|newest]
Thread overview: 37+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-04-28 0:02 Jacques Garrigue
2013-04-28 2:45 ` Markus Mottl
2013-04-28 10:28 ` Jacques Garrigue
2013-04-28 5:54 ` Jacques Le Normand
2013-04-29 3:45 ` Ivan Gotovchits
2013-04-29 4:03 ` Ivan Gotovchits
2013-04-29 5:17 ` Jacques Le Normand
2013-04-29 7:58 ` Alain Frisch
2013-04-29 10:52 ` Jacques Garrigue
2013-04-29 11:23 ` Alain Frisch
2013-04-29 16:37 ` Nathan Mishra Linger [this message]
2013-04-29 23:53 ` Jacques Garrigue
2013-04-30 5:45 ` Jacques Garrigue
2013-05-04 6:46 ` Jacques Garrigue
2013-05-04 7:09 ` Gabriel Scherer
2013-05-04 12:28 ` Jacques Garrigue
2013-04-30 6:59 ` Alain Frisch
2013-04-30 7:56 ` Jacques Garrigue
2013-04-30 8:02 ` Alain Frisch
2013-04-30 8:18 ` Jacques Garrigue
2013-04-30 9:11 ` Gabriel Scherer
2013-04-30 9:55 ` Jacques Garrigue
2013-04-30 10:12 ` Leo White
2013-04-30 11:30 ` Gabriel Scherer
2013-04-30 13:06 ` Leo White
2013-04-29 7:59 ` Gabriel Scherer
2013-07-01 14:47 ` Alain Frisch
2013-07-01 23:20 ` Jacques Garrigue
2013-07-03 16:08 ` Alain Frisch
2013-07-03 16:13 ` Gabriel Scherer
2013-07-04 6:07 ` [Caml-list] Request for feedback: A problem with injectivity oleg
2013-07-04 7:35 ` Alain Frisch
2013-07-05 10:30 ` oleg
2013-07-05 12:02 ` Alain Frisch
2013-07-04 1:00 ` [Caml-list] Request for feedback: A problem with injectivity and GADTs Jacques Garrigue
2013-07-04 8:14 ` Alain Frisch
2013-07-04 8:52 ` 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=CAJO0BX1rQecYyHhfyNXv4BLhxF17ghFvUT_nAUWKoKzmMCF31g@mail.gmail.com \
--to=nathan.mishralinger@gmail.com \
--cc=alain@frisch.fr \
--cc=caml-list@inria.fr \
--cc=garrigue@math.nagoya-u.ac.jp \
/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).