From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 92E9DBBAF for ; Sat, 27 Feb 2010 07:38:33 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgEBAFpMiEuLEwExgGdsb2JhbACbMgEBCwsKBRUFHa1mAY4CBYR7 X-IronPort-AV: E=Sophos;i="4.49,549,1262559600"; d="scan'208";a="53700873" Received: from infao0809.mpi-sb.mpg.de (HELO hera.mpi-sb.mpg.de) ([139.19.1.49]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 27 Feb 2010 07:38:33 +0100 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=Message-Id:From:To:In-Reply-To: Content-Type:Content-Transfer-Encoding:Mime-Version:Subject:Date: References; bh=Riwnp8kZL3w8lpHevTGLpG4tXuL1GrB2AVzjDjAiwGU=; b=Q 3s2JrE4nxkH7U06MClUFPS64mX5PWieuS5C1Zbe9dRfh1vpD6CJJ/BjXQa/isD1N 9+cPPUKPkTEPcH358rq401bGcN6VXFfnijFUczkTBB909L+cEi0TNz+mgdOQPUhH +KGGHSPPl/D18eu8I3mRVRZtp3oLtC//CBboORm978= Received: from newzak.mpi-sb.mpg.de ([139.19.1.28]:60100) by hera.mpi-sb.mpg.de (envelope-from ) with esmtp (Exim 4.69) id 1NlGJp-0001Z3-JS for caml-list@inria.fr; Sat, 27 Feb 2010 07:38:32 +0100 Received: from c-67-180-84-64.hsd1.ca.comcast.net ([67.180.84.64]:56794 helo=[192.168.1.2]) by newzak.mpi-sb.mpg.de with esmtpsa (TLS-1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.63) (envelope-from ) id 1NlGJp-0003C3-5H for caml-list@inria.fr; Sat, 27 Feb 2010 07:38:29 +0100 Message-Id: From: Andreas Rossberg To: OCaml List In-Reply-To: <4B887AED.3090005@citycable.ch> Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v936) Subject: Re: [Caml-list] Recursive subtyping issue Date: Sat, 27 Feb 2010 07:38:25 +0100 References: <4B887AED.3090005@citycable.ch> X-Mailer: Apple Mail (2.936) X-Spam: no; 0.00; rossberg:01 rossberg:01 recursive:01 subtyping:01 guillaume:01 subtyping:01 recursive:01 wrote:01 andreas:01 andreas:01 caml-list:01 rarely:02 latter:03 types:05 mean:08 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