From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rossberg@mpi-sws.org>
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 39956BC37
	for <caml-list@yquem.inria.fr>; Wed, 10 Feb 2010 11:12:39 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AqIAALcVckuLEwExkWdsb2JhbACaaRUBAQEBCQsKBxMFHq4CAY4PBYRV
X-IronPort-AV: E=Sophos;i="4.49,442,1262559600"; 
   d="scan'208";a="44435955"
Received: from hera.mpi-sb.mpg.de ([139.19.1.49])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 10 Feb 2010 11:12:38 +0100
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=mpi-sb.mpg.de; s=mail200803; h=Message-ID:In-Reply-To:
	References:Date:Subject:From:To:MIME-Version:Content-Type:
	Content-Transfer-Encoding; bh=SeOC9lYvBPC9pESgTNmvd0+HUmHr5s8lJi
	wEYlQ6fa0=; b=ipsLLjRSZuB6c993NvDWyyyDbQt46FYWJ6nEZTRP8rQk14Pvfp
	HxGLSWYSvf16StWynZBMx9XywL9zNN2o5WYiTmb1z2oP2eU88rWA2BmgsOEFXFhl
	z0oKSrt1mehVl2izs2mBleoOSm2kY4iXlpqWNB4SjgVxkcAtCy4AOPB+0=
Received: from infao0525.mpi-sb.mpg.de ([139.19.1.26]:43500 helo=newmaniac.mpi-sb.mpg.de)
	by hera.mpi-sb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtp (Exim 4.69) id 1Nf9Yg-0002zE-W8
	for caml-list@yquem.inria.fr; Wed, 10 Feb 2010 11:12:37 +0100
Received: from www-data by newmaniac.mpi-sb.mpg.de with local (Exim 4.63)
	(envelope-from <rossberg@mpi-sws.org>)
	id 1Nf9Yg-0002XJ-KV
	for caml-list@yquem.inria.fr; Wed, 10 Feb 2010 11:12:34 +0100
Received: from 80.146.185.83
        (SquirrelMail authenticated user rossberg)
        by mail.mpi-sws.org with HTTP;
        Wed, 10 Feb 2010 11:12:34 +0100 (CET)
Message-ID: <35ebacb77d7cfe3694edbada6ce91229.squirrel@mail.mpi-sws.org>
In-Reply-To: <7d8707de1002092319j4d6bfca5s169914a992d57be2@mail.gmail.com>
References: <1e7471d51002091250of7a686fq537a03c9401c868f@mail.gmail.com>
    <1265752863.5482.42.camel@flake.lan.gerd-stolpmann.de>
    <7d8707de1002092319j4d6bfca5s169914a992d57be2@mail.gmail.com>
Date: Wed, 10 Feb 2010 11:12:34 +0100 (CET)
Subject: Re: [Caml-list] The need to specify 'rec' in a recursive function  
     defintion
From: rossberg@mpi-sws.org
To: caml-list@yquem.inria.fr
User-Agent: SquirrelMail/1.4.15
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-15
Content-Transfer-Encoding: 8bit
X-Priority: 3 (Normal)
Importance: Normal
X-Spam: no; 0.00; recursive:01 defintion:01 rossberg:01 andrej:01 andrej:01 gerd:01 untyped:01 recursion:01 recursive:01 typable:01 wrote:01 andreas:01 caml-list:01 explicitly:02 let:03 

"Andrej Bauer" <andrej.bauer@andrej.com> wrote:
>
> What Gerd probably meant was that the usual untyped lambda-calculus
> definition of y, which gets us recursion out of nothing isn't typeable
> because self-application requires unrestricted recursive types.

Fortunately, even that is not quite correct: Y is perfectly typable in
plain ML, you just need to introduce the recursive type it employs
explicitly:

type 'a fix = Fix of ('a fix -> 'a)
let fix f = let z = fun (Fix g' as g) x -> f (g' g) x in z (Fix z)

Now, for example:

let fac = fix (fun fac n -> if n = 0 then 1 else n * fac (n-1))
let n = fac 7

Best,
/Andreas