From: Andreas Rossberg <rossberg@mpi-sws.org>
To: OCaml List <caml-list@inria.fr>
Subject: Re: [Caml-list] Recursive subtyping issue
Date: Sat, 27 Feb 2010 07:38:25 +0100 [thread overview]
Message-ID: <FA802246-982F-46AF-8677-9FCA7F6F011A@mpi-sws.org> (raw)
In-Reply-To: <4B887AED.3090005@citycable.ch>
On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>
> I've been struggling to have a type system where I could do the
> following subtyping:
>
> 'a t1 :> t2 and t2 :> 'a t1
Hm, what do you mean? Subtyping ought to be reflexive and
antisymmetric (although the latter is rarely proved for most type
systems), which means that your two inequations will hold if and only
if 'a t1 = t2, regardless of recursive types.
/Andreas
next prev parent reply other threads:[~2010-02-27 6:38 UTC|newest]
Thread overview: 22+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-02-27 1:52 Guillaume Yziquel
2010-02-27 6:38 ` Andreas Rossberg [this message]
2010-02-27 10:25 ` [Caml-list] " Guillaume Yziquel
2010-02-27 11:49 ` Goswin von Brederlow
2010-02-27 13:11 ` Guillaume Yziquel
2010-02-27 16:52 ` Andreas Rossberg
2010-02-27 18:10 ` Guillaume Yziquel
2010-02-27 19:52 ` Guillaume Yziquel
2010-02-27 20:32 ` Guillaume Yziquel
2010-03-01 10:55 ` Stéphane Glondu
2010-03-01 11:21 ` Guillaume Yziquel
2010-03-01 12:28 ` Stéphane Glondu
2010-03-01 12:49 ` David Allsopp
2010-03-01 13:06 ` Guillaume Yziquel
2010-03-01 12:49 ` David Allsopp
2010-03-01 13:28 ` Goswin von Brederlow
2010-03-01 20:12 ` David Allsopp
2010-03-02 10:22 ` Goswin von Brederlow
2010-03-01 13:33 ` Guillaume Yziquel
2010-03-01 20:18 ` David Allsopp
2010-02-28 9:54 ` Goswin von Brederlow
2010-02-28 11:08 ` Guillaume Yziquel
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=FA802246-982F-46AF-8677-9FCA7F6F011A@mpi-sws.org \
--to=rossberg@mpi-sws.org \
--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).