From: Guillaume Yziquel <guillaume.yziquel@citycable.ch>
To: Andreas Rossberg <rossberg@mpi-sws.org>
Cc: OCaml List <caml-list@inria.fr>
Subject: Re: [Caml-list] Recursive subtyping issue
Date: Sat, 27 Feb 2010 11:25:48 +0100 [thread overview]
Message-ID: <4B88F32C.3050701@citycable.ch> (raw)
In-Reply-To: <FA802246-982F-46AF-8677-9FCA7F6F011A@mpi-sws.org>
Andreas Rossberg a écrit :
> 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
Antisymmetric?
> yziquel@seldon:~$ ocaml
> Objective Caml version 3.11.2
>
> # type q = private w and w = private q;;
> type q = private w
> and w = private q
> # let f (x : q) = (x : q :> w);;
> val f : q -> w = <fun>
> # let f (x : q) = (x : w);;
> Error: This expression has type q but an expression was expected of type w
> #
Not exactly, it seems.
My goal is to implement a type inference barrier.
You can do
> type 'a q = private w
and from the type inference point of view, int q and float q are two
distinct types, that you can subtype to a common type.
What I want is also to have the reverse, i.e.
> type w = private 'a q
But that doesn't work out this way because of the fact that 'a is unbound.
You can move around this specific problem by using contravariant
polymorphism, as is done in my previous email, but somehow, you cannot
have a recursive subtyping from 'a q to w and from w back to 'a q. There
always seem to be something wrong, with a problematic more or less
analoguous to adjoint functors in category theory.
Hence my last email.
All the best,
--
Guillaume Yziquel
http://yziquel.homelinux.org/
next prev parent reply other threads:[~2010-02-27 10:25 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 ` [Caml-list] " Andreas Rossberg
2010-02-27 10:25 ` Guillaume Yziquel [this message]
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=4B88F32C.3050701@citycable.ch \
--to=guillaume.yziquel@citycable.ch \
--cc=caml-list@inria.fr \
--cc=rossberg@mpi-sws.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
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).