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=2.8 required=5.0 tests=DNS_FROM_RFC_POST,SPF_NEUTRAL 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 A56F5BBAF for ; Fri, 9 Oct 2009 12:22:59 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah8BAB+szkpIDtydkGdsb2JhbACRQYkDPwEBAQEJCQwHEwOuI4E7j2EBAwMFhCUE X-IronPort-AV: E=Sophos;i="4.44,531,1249250400"; d="scan'208";a="37908121" Received: from fg-out-1718.google.com ([72.14.220.157]) by mail1-smtp-roc.national.inria.fr with ESMTP; 09 Oct 2009 12:22:59 +0200 Received: by fg-out-1718.google.com with SMTP id d23so1890376fga.3 for ; Fri, 09 Oct 2009 03:22:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:in-reply-to:references :date:message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=GxFBFn2N6SOdAj4bk56BrU3jHH8dDxFeR8Q30ZzBeyQ=; b=itwGkd10siZ2jN3uPptYwG8caEC4JcRrlhY+ktBHqxIxhBz5wK08cY95oa2p+tNtJE H9NINlDTQ45unOe85XvKCPX1dQbTjELN3Us35rMxB/IQ1jK0NVtSOAPmycYyTe/UMlzK L2S6tc+xXflO6EeBVVKv18fSGynQwimQsF4vI= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=R9XS1MHtyjio9KuTdQrSdQIf23IiptMDAKzKJWdLImh2m3DK3gYn5V/P3TyD0TNwu8 QJ3KMKPaxo7E+c+MDRV0KDdQCYyhCaam79OYwZshHTqeJyiAI6ksHvHw8IbaAX67M6gH reIb/e5PjVBeW3uTvt4zKO8yudnTXyWUp7Flc= MIME-Version: 1.0 Received: by 10.86.254.23 with SMTP id b23mr1655486fgi.21.1255083779334; Fri, 09 Oct 2009 03:22:59 -0700 (PDT) In-Reply-To: <53322.41.177.16.252.1255065941.squirrel@41.177.16.252> References: <53322.41.177.16.252.1255065941.squirrel@41.177.16.252> Date: Fri, 9 Oct 2009 11:22:59 +0100 Message-ID: Subject: Re: [Caml-list] Why type inference fails in this code From: Jeremy Yallop To: rouanvd@softwarerealisations.com Cc: caml-list@yquem.inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; inference:01 foo:01 foo:01 ocaml's:01 inference:01 undecidable:01 forall:01 forall:01 ocaml:01 ocaml:01 2009:98 polymorphic:01 caml-list:01 int:01 int:01 Dear Rouan, 2009/10/9 : > type t =3D MyInt of int | MyFloat of float | MyString of string ;; > > let foo printerf =3D function > =A0| MyInt i -> printerf string_of_int i > =A0| MyFloat x -> printerf string_of_float x > =A0| MyString s -> printerf (fun x -> x) s This fails because the variable "printerf" is used at different types inside the body of foo. OCaml's type system requires function arguments to be used at the same type everywhere they appear in the body of the function. The reason is simple: without this restriction type inference becomes undecidable. The most reasonable type for foo seems like the following: forall 'b. (forall 'a. ('a -> string) -> 'a -> 'b) -> t -> 'b which is the type of a function that constructs a value of type 'b from a value of type t using its argument function; this argument function takes a printer for any type 'a and a value of type 'a and constructs a value of type 'b. We can make two adjustments to "foo" to turn it into something that OCaml will accept. The first adjustment is to turn the argument "printerf" into an object with a single method; polymorphic types (i.e. types that use "forall") in OCaml must be wrapped in object or record types. The second adjustment is to provide a type signature, which changes the impossible problem of type /inference/ into the easier problem of type /checking/. Here is the revised definition: let foo : < p : 'a . ('a -> string) -> 'a -> 'b > -> t -> 'b =3D fun printerf -> function | MyInt i -> printerf#p string_of_int i | MyFloat x -> printerf#p string_of_float x | MyString s -> printerf#p (fun x -> x) s In order to call this function we must, of course, ensure that the first argument is an object. Here is a simple example, where the argument just returns the constructed string: foo (object method p : 'a. ('a -> string) -> 'a -> string =3D fun x -> x end) (MyInt 3) Hope this helps, Jeremy.