English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Recursive subtyping issue
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2010-02-27 (06:38)
From: Andreas Rossberg <rossberg@m...>
Subject: Re: [Caml-list] Recursive subtyping issue
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.