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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 933FEBBAF for ; Sat, 27 Feb 2010 17:53:10 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmkAADPdiEuLEwExkWdsb2JhbACbGxUBAQEBCQsKBxMFHatGAY10BYR7 X-IronPort-AV: E=Sophos;i="4.49,551,1262559600"; d="scan'208";a="45677826" Received: from hera.mpi-sb.mpg.de ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 27 Feb 2010 17:53:01 +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:Subject:Mime-Version:Date: References; bh=Bu5uzZqENBi7XK8/RGjv/n3BkbVsoEWFsZIzGAipEIc=; b=N 8XuFR/vKrkxjKi3dXdKD+vN+/8TVVe3EBRiz9taHhFWcBXzieBtv0oTHXMiEfk1e OPHI3ggqoPIPfYtLCUYJbt3CbmDlElbLL/rXDGEdQ6hBrgkR+7LIGeW41XPdS/2Y oZUxy2nWPQJhQnSc0OHCIYpj/2Je5oIPGnNM9jGum0= Received: from newmaniac.mpi-sb.mpg.de ([139.19.1.26]:59102) by hera.mpi-sb.mpg.de (envelope-from ) with esmtp (Exim 4.69) id 1NlPuT-0001X6-O3; Sat, 27 Feb 2010 17:53:00 +0100 Received: from c-67-180-84-64.hsd1.ca.comcast.net ([67.180.84.64]:59569 helo=[192.168.1.2]) by newmaniac.mpi-sb.mpg.de with esmtpsa (TLS-1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.63) (envelope-from ) id 1NlPuS-00006o-OL; Sat, 27 Feb 2010 17:52:57 +0100 Message-Id: <76EDF2F2-8B02-4C97-B083-EC74630D8ECA@mpi-sws.org> From: Andreas Rossberg To: OCaml List In-Reply-To: <4B891A0C.604@citycable.ch> Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Recursive subtyping issue Mime-Version: 1.0 (Apple Message framework v936) Date: Sat, 27 Feb 2010 17:52:53 +0100 References: <4B887AED.3090005@citycable.ch> <4B88F32C.3050701@citycable.ch> <87k4tyoq3m.fsf@frosties.localdomain> <4B891A0C.604@citycable.ch> X-Mailer: Apple Mail (2.936) X-Spam: no; 0.00; rossberg:01 rossberg:01 recursive:01 subtyping:01 guillaume:01 val:01 bug:01 compiler:01 ocaml:01 node:01 oversight:01 fwiw:01 val:01 polymorphism:01 inference:01 On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote: >> # 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 = >> # let f (x : q) = (x : w);; >> Error: This expression has type q but an expression was expected of >> type w >> # Interesting, but these are vacuous type definitions. In fact, I would call it a bug that the compiler does not reject them (it does when you remove at least one of the "private"s). In any case, I don't quite understand how this pathological behaviour is supposed to help, because the types are uninhabited anyway. > I've been looking all over at this issue, but simply cannot find a > way out. While experimenting on this, I've stumbled on a number of > quirky issues with the type system. > > First one: http://ocaml.janestreet.com/?q=node/26 That's indeed a slight oversight in the design of the module type system. (FWIW, this is possible in SML.) > Second one: > >> # type 'a q = ;; >> type 'a q = < m : 'a > >> # let f : 'a q -> 'a q = fun x -> x;; >> val f : 'a q -> 'a q = >> # let o = object method m : 'a. 'a -> 'a = fun x -> x end;; val o : >> < m : 'a. 'a -> 'a > = >> # f o;; >> Error: This expression has type < m : 'a. 'a -> 'a > >> but an expression was expected of type 'b q >> The universal variable 'a would escape its scope This example would require full impredicative polymorphism, because you would need to instantiate 'a q with a polymorphic type. The ML type system does not support that, because it generally makes type inference undecidable. But see e.g. Le Botlan & Remy's work on ML^F for a more powerful approach than what we have today. /Andreas