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=1.5 required=5.0 tests=AWL,NO_REAL_NAME,SPF_FAIL 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 9358EBBCA for ; Thu, 28 Feb 2008 06:26:41 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHvUxUfAEKcgeGdsb2JhbACPcmoNAQoEBggHGp0w X-IronPort-AV: E=Sophos;i="4.25,417,1199660400"; d="scan'208";a="8698721" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 28 Feb 2008 06:26:41 +0100 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1S5QfNh009286 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 28 Feb 2008 06:26:41 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHvUxUfAEKcgeGdsb2JhbACPcmoNAQoEBggHGp0w X-IronPort-AV: E=Sophos;i="4.25,417,1199660400"; d="scan'208";a="8698720" Received: from unknown (HELO selenite.metnet.navy.mil) ([192.16.167.32]) by mail1-smtp-roc.national.inria.fr with ESMTP; 28 Feb 2008 06:26:40 +0100 Received: (qmail 28438 invoked by uid 107); 28 Feb 2008 05:26:35 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.152) by selenite.metnet.navy.mil with SMTP; 28 Feb 2008 05:26:35 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id 355ADA99B; Wed, 27 Feb 2008 21:23:36 -0800 (PST) From: oleg@okmij.org To: Andrej.Bauer@fmf.uni-lj.si Cc: caml-list@inria.fr Subject: Re: Unexpected restriction in "let rec" expressions Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org Message-Id: <20080228052336.355ADA99B@Adric.metnet.fnmoc.navy.mil> Date: Wed, 27 Feb 2008 21:23:36 -0800 (PST) X-Miltered: at concorde with ID 47C64611.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 andrej:01 fixpoint:01 val:01 int-:01 val:01 combinator:01 failwith:01 combinators:01 polymorphic:01 wrote:01 abstract:01 rec:01 precisely:01 int:01 Andrej Bauer wrote: > More precisely, consider any term > fix : (c -> c) -> c, > where the name "fix" suggests that we will plug in a fix-point operator > at the end of the day. > ... > P.S. Can someone think of anything else other than a fixpoint operator > that we could use in place of fix to get an interesting program (maybe > for special cases of c, such as c = int -> int)? `For special cases if c' makes the problem very easy. For example, let c = int: # let pseudofixint f : int = f 0;; val pseudofixint : (int -> int) -> int = or let c = int-> int # let anotherpseudofix f : int -> int = f (fun (x:int) -> x);; val anotherpseudofix : ((int -> int) -> int -> int) -> int -> int = It is only if we insist on a polymorphic function (for all c or at least c = a-> b for all a and b) that we obtain that fix must be either a fix-point combinator or a similar misbehaving term such as # let almostfix (f:'c -> 'c) = f (failwith "what could you expect");; val almostfix : ('a -> 'a) -> 'a = This is because only fix or similar misbehaving combinators let us `produce' values that do not exist (or at least, claim to produce those values). For example: # type unicorn (* abstract *) # let f (x:unicorn) = x val f : unicorn -> unicorn = Indeed, we can always demonstrate a value of the type c->c no matter how bizarre c is. Thus, expression (almostfix f) has the type unicorn and `gives' us the value of unicorns, `proving' that unicorns exist.