From: Oleg <firstname.lastname@example.org> To: email@example.com Cc: firstname.lastname@example.org Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic Date: Wed, 7 Oct 2020 22:17:32 +0900 Message-ID: <20201007131732.GA4915@Melchior.localnet> (raw) In-Reply-To: <email@example.com> > As far as I understand Oleg's solutions, they all boil down to the > same idea, which I have considered, but is only half satisfactory: > that is, to publish a covariant abstract type +'a t which internally > is implemented as an abbreviation for an unparameterized type u. (See > the food/wine/fridge example, rewritten in this style, below.) Good summary! > The reason why this solution is only half satisfactory is that inside the > abstraction barrier, we have an unparameterized type u that does not express > the desired data invariant, so we cannot exploit the invariant to prove that > certain branches in the code are dead. Indeed. That was the `imperfection' that I have referred to in my message. I have two comments: first, there is the second solution, which does exploit the invariant. Second, there may be more than one abstraction barrier... That is, many implementations of the wine_food signature may be in terms of some `more basic' signature -- or just the same signature, if we are talking about term transformations (as I have just replied to Josh Berdine). Eventually we have to implement the `most basic signature', and indeed we have to drop the indices and fall into the `untyped' universe, so to speak. One hopes though that this `security kernel' is really `most basic' and its operations are few and primitive, so the correctness could be relatively easily ascertained. > Also, the user cannot perform case analysis, since the type 'a t is > abstract. This is not a problem for me, but could be a problem in > other situations. When I first mentioned tagless-final, in passing at a some conference in Oxford a decade ago, an old Oxford professor (one of fathers of SML) exclaimed: ``Isn't it bloody obvious that you cannot do pattern-matching in this style!?''. I liked his phrase. Now I like to say that pattern-matching in tagless-final style is not bloody, is not obvious and is not impossible. That it is always possible was proven by Boehm and Berarducci (their proof was one inspiration for the development of Coq, as I heard). http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Although their general method works always, often one may design simpler methods for particular pattern-matching tasks.
next prev parent reply other threads:[~2020-10-07 13:13 UTC|newest] Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-10-06 11:57 [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier 2020-10-06 16:05 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg 2020-10-06 16:45 ` François Pottier 2020-10-06 19:04 ` Josh Berdine 2020-10-06 19:18 ` [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) François Pottier 2020-10-06 20:10 ` Josh Berdine 2020-10-07 13:17 ` Oleg [this message] 2020-10-07 13:17 ` [Caml-list] Question on the covariance of a GADT (polymorphic Oleg 2020-10-07 8:10 ` David Allsopp
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=20201007131732.GA4915@Melchior.localnet \ --firstname.lastname@example.org \ --email@example.com \ --firstname.lastname@example.org \ /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
caml-list - the Caml user's mailing list This inbox may be cloned and mirrored by anyone: git clone --mirror http://inbox.vuxu.org/caml-list git clone --mirror https://inbox.ocaml.org/caml-list # If you have public-inbox 1.1+ installed, you may # initialize and index your mirror using the following commands: public-inbox-init -V1 caml-list caml-list/ http://inbox.vuxu.org/caml-list \ email@example.com public-inbox-index caml-list Example config snippet for mirrors. Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.caml-list AGPL code for this site: git clone https://public-inbox.org/public-inbox.git