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.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 276ADBBCA for ; Wed, 27 Feb 2008 09:55:05 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADO0xEfBAkMtn2dsb2JhbACQaAEBAQEBBgQGCQgYnEo X-IronPort-AV: E=Sophos;i="4.25,412,1199660400"; d="scan'208";a="7751334" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Feb 2008 09:55:05 +0100 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 m1R8t0Sk031907 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 27 Feb 2008 09:55:04 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADO0xEfBAkMtn2dsb2JhbACQaAEBAQEBBgQGCQgYnEo X-IronPort-AV: E=Sophos;i="4.25,412,1199660400"; d="scan'208";a="7751333" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Feb 2008 09:55:04 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id A158336F49A; Wed, 27 Feb 2008 09:55:03 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id jMkOKI-KzMUi; Wed, 27 Feb 2008 09:55:03 +0100 (CET) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id A22BB3712F1; Wed, 27 Feb 2008 09:53:07 +0100 (CET) Message-ID: <47C524F3.9030005@fmf.uni-lj.si> Date: Wed, 27 Feb 2008 09:53:07 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: Loup Vaillant Cc: Caml List Subject: Re: [Caml-list] Unexpected restriction in "let rec" expressions References: <6f9f8f4a0802260424o5bce2fd9i89fbfa38bb239a6a@mail.gmail.com> In-Reply-To: <6f9f8f4a0802260424o5bce2fd9i89fbfa38bb239a6a@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 47C52564.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 fixpoint:01 fixpoint:01 lambda:01 wrote:01 rec:01 caml-list:01 precisely:01 int:01 int:01 defining:02 unexpected:03 let:03 let:03 Loup Vaillant wrote: > loop :: ((a,c) -> (b,c)) -> a -> b > loop f a = b > where (b,c) = f (a,c) You said the above was a "so-called fixpoint operator". To see in what sense this really is a fixpoint operator consider the type: ((a * c) -> (b * c)) -> a -> b (1) It is equivalent (under currying-uncurrying) to (a -> (c -> b) * (c -> c)) -> a -> b (2) We could write down a term of this type if we had a way of going from type c -> c to type c. 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. Before reading on, you should try to write down a term of type (2), given that we have fix. I will bet that your brain will produce the same solution as described below. We can get a term of type (2) by defining let loop' f x = let (g, h) = f x in g (fix h) Converting from (2) back to (1) gives us an equivalent term let loop f x = let f' y = (fun z -> fst (f (y, z))), (fun z -> snd (f (y, z))) in loop' f' x or by beta-reducing: let loop f x = fst (f (x, fix (fun z -> snd (f (x, z))))) You are now free to plug in whatever you wish for fix, but presumably you would like fix to compute fixed points. This may be somewhat troublesome in an eager language, especially if c is not a function type. In fact, we may recover fix from loop as follows: let fix' f = loop (fun (_, z) -> (z, f z)) () To see that fix' is the same as fix, we just beta-eta reduce: fix' f = loop (fun (_, z) -> (z, f z)) () = fst (fix (fun z -> f z), f (fix (fun z -> f z))) = fix (fun z -> f z) = fix f Indeed, loop is a generalized fixpoint operator. But I think the nice picture drawn by Nicolas Pouillard is worth a thousand lambda terms. Best regards, Andrej 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)?