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 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 98325BC69 for ; Sat, 24 Nov 2007 06:50:28 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGtKR0fAXQImh2dsb2JhbACOSnMBAQEICik X-IronPort-AV: E=Sophos;i="4.21,459,1188770400"; d="scan'208";a="4559595" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Nov 2007 06:50:27 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id lAO5oRfY007046 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Sat, 24 Nov 2007 06:50:27 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABpKR0fAEKcgh2dsb2JhbACOSnMBAQEICik X-IronPort-AV: E=Sophos;i="4.21,459,1188770400"; d="scan'208";a="6129238" Received: from selenite.metnet.navy.mil ([192.16.167.32]) by mail3-smtp-sop.national.inria.fr with ESMTP; 24 Nov 2007 06:50:26 +0100 Received: (qmail 12101 invoked by uid 107); 24 Nov 2007 05:50:23 -0000 Received: from unknown (HELO Adric.metnet.fnmoc.navy.mil) (10.100.105.152) by selenite.metnet.navy.mil with SMTP; 24 Nov 2007 05:50:23 -0000 Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id A0FF4A9AD; Fri, 23 Nov 2007 21:47:59 -0800 (PST) To: jtbryant@valdosta.edu, Andrej.Bauer@fmf.uni-lj.si Cc: caml-list@inria.fr Subject: Re: Type issue Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20071124054759.A0FF4A9AD@Adric.metnet.fnmoc.navy.mil> Date: Fri, 23 Nov 2007 21:47:59 -0800 (PST) X-Miltered: at discorde with ID 4747BBA3.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 frisch:01 recursion:01 inference:01 recursion:01 recursive:01 recursive:01 polymorphism:01 ocaml:01 bool:01 bool:01 val:01 polymorphic:01 polymorphic:01 rec:01 As Alain Frisch mentioned, with polymorphic recursion, inference is in general impossible. Luckily, polymorphic recursion can be integrated into a HM system if we require a type annotation on polymorphically recursive functions. The annotation can come in various forms: for example, if we use recursive modules, the annotation is given in the signature. It seems using first-class polymorphism of OCaml records might be a bit simpler: type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;; type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a type ft = {ft : 'a . 'a t -> 'a};; type ft = { ft : 'a. 'a t -> 'a; } let f = let rec f' = {ft = function | Cond (c,t,e) -> if f'.ft c then f'.ft t else f'.ft e | Value x -> x} in f'.ft;; val f : 'a t -> 'a = f (Cond ((Value true),(Value 1),(Value 2)));; - : int = 1 One should think of 'ft' as marking the places where the big-lambda is introduced and eliminated. Luckily, the extended value restriction (or should I say, restricted value restriction) helps us avoid eta-expansion in the definition of f.