From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: ** X-Spam-Status: No, score=2.2 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 6FDC7BBC6 for ; Thu, 26 Mar 2009 00:24:40 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlcGALRZyknVBJXyY2dsb2JhbACBUJQkFwgLBxG8dIN1Bg X-IronPort-AV: E=Sophos;i="4.38,422,1233529200"; d="scan'208";a="37214995" Received: from outmailhost.telefonica.net (HELO ctsmtpout2.frontal.correo) ([213.4.149.242]) by mail4-smtp-sop.national.inria.fr with ESMTP; 26 Mar 2009 00:24:40 +0100 Received: from NANA.localdomain (83.59.14.112) by ctsmtpout2.frontal.correo (7.2.056.6) (authenticated as ferferse$telefonica.net) id 49B4D713006E1120 for caml-list@inria.fr; Thu, 26 Mar 2009 00:24:39 +0100 Received: from mfp by NANA.localdomain with local (Exim 4.69) (envelope-from ) id 1LmcSc-0002Ya-Rv for caml-list@inria.fr; Thu, 26 Mar 2009 00:24:38 +0100 Date: Thu, 26 Mar 2009 00:24:38 +0100 From: Mauricio Fernandez To: caml-list@inria.fr Subject: Re: [Caml-list] polymorphic variants and recursive functions Message-ID: <20090325232438.GW8986@NANA.localdomain> Mail-Followup-To: caml-list@inria.fr References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.17+20080114 (2008-01-14) X-Spam: no; 0.00; variants:01 recursive:01 val:01 abstr:01 subtype:01 2009:98 warren:98 polymorphic:01 wrote:01 abstract:01 rec:01 caml-list:01 functions:01 variant:02 variant:02 On Wed, Mar 25, 2009 at 02:39:28PM -0700, Warren Harris wrote: > let rec eval = function > | `Arr v -> (eval_arr v : [`V] Lwt.t :> [> `V] Lwt.t) > | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t) > and eval_arr v = eval_obj v >>= arr > and eval_obj v = eval v >>= obj > > | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t) > ^^^^^^^^^^ > This expression has type [ `O | `V ] Lwt.t but is here used with type > [ `V ] Lwt.t > The second variant type does not allow tag(s) `O The Lwt.t type is abstract and invariant since no annotation has been given for the type variable (you'd need it to be type +'a t): # let a : [`O] Lwt.t = return `O;; val a : [ `O ] Lwt.t = # (a :> [`O | `V] Lwt.t);; Error: Type [ `O ] Lwt.t is not a subtype of type [ `O | `V ] Lwt.t The first variant type does not allow tag(s) `V In your example, [> `V] Lwt.t in the second line becomes [`V] Lwt.t, (the type variable is not covariant) and you cannot do [`V | `O] Lwt.t :> [`V] Lwt.t in the third line. Unfortunately, the type variable is in both variant and contravariant position in the definition of Lwt.t... -- Mauricio Fernandez - http://eigenclass.org