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=0.7 required=5.0 tests=DATE_IN_PAST_06_12 autolearn=disabled version=3.1.3 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 1151ABBAF for ; Mon, 15 Sep 2008 17:20:05 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnUCADsazkjAXQIniGdsb2JhbABBkjYBAQEPIJ8LhGA+gWQ X-IronPort-AV: E=Sophos;i="4.32,402,1217800800"; d="scan'208";a="17295887" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 15 Sep 2008 17:20:04 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m8FFK413028223 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Mon, 15 Sep 2008 17:20:04 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBAMUZzkhQW+UCgWdsb2JhbABBkjYBARAgBJ8FhGA+gWQ X-IronPort-AV: E=Sophos;i="4.32,402,1217800800"; d="scan'208";a="14962297" Received: from main.gmane.org (HELO ciao.gmane.org) ([80.91.229.2]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 15 Sep 2008 17:20:04 +0200 Received: from root by ciao.gmane.org with local (Exim 4.43) id 1KfFru-0005oX-A5 for caml-list@inria.fr; Mon, 15 Sep 2008 15:20:03 +0000 Received: from d-199-222-77.bootp.Virginia.EDU ([199.111.222.77]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 15 Sep 2008 15:20:02 +0000 Received: from weihu by d-199-222-77.bootp.Virginia.EDU with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 15 Sep 2008 15:20:02 +0000 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Wei Hu Subject: Predicativity? Date: Mon, 15 Sep 2008 07:26:14 +0000 (UTC) Message-ID: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: main.gmane.org User-Agent: Loom/3.14 (http://gmane.org/) X-Loom-IP: 199.111.222.77 (Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1; Trident/4.0; GoogleT5; .NET CLR 1.1.4322; .NET CLR 3.0.04506.30; OfficeLiveConnector.1.0; CIBA; .NET CLR 2.0.50727)) Sender: news X-Miltered: at concorde with ID 48CE7D24.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml's:01 polymorphism:01 toplevel:01 val:01 val:01 polymorphism:01 ocaml:01 let:03 let:03 applied:05 fun:08 fun:08 wrong:10 example:10 doesn't:12 Hello, Isn't OCaml's polymorphism predicative? Then, why does the following code in the interactive toplevel type check? # let id x = x;; val id : 'a -> 'a = # let f x = (id id) x;; val f : 'a -> 'a = I thought id could not be applied to itself under predicative polymorphism. Is my understanding wrong? Can you show an example that doesn't type check in OCaml, but would type check under impredicate polymorphism? Thanks!