From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 86F9CBBAF for ; Thu, 24 Dec 2009 13:12:13 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiADANfpMkvZSMDqi2dsb2JhbACBSpoOAQoLCgcRBbhAhDME X-IronPort-AV: E=Sophos;i="4.47,448,1257116400"; d="scan'208";a="42689784" Received: from fmmailgate03.web.de ([217.72.192.234]) by mail1-smtp-roc.national.inria.fr with ESMTP; 24 Dec 2009 13:12:13 +0100 Received: from smtp05.web.de (fmsmtp05.dlan.cinetic.de [172.20.4.166]) by fmmailgate03.web.de (Postfix) with ESMTP id 7FFC013A5B555; Thu, 24 Dec 2009 13:12:12 +0100 (CET) Received: from [95.208.117.111] (helo=frosties.localdomain) by smtp05.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #314) id 1NNmW7-0006jw-00; Thu, 24 Dec 2009 13:10:07 +0100 Received: from mrvn by frosties.localdomain with local (Exim 4.69) (envelope-from ) id 1NNmW7-0004uj-DT; Thu, 24 Dec 2009 13:10:07 +0100 From: Goswin von Brederlow To: boris@yakobowski.org Cc: caml-list caml-list Subject: Re: [Caml-list] obj.magic for polymorphic record fields References: <531142069376641352@orange.fr> <87zl5cmof9.fsf@frosties.localdomain> <76c7f53f0912210600y91c9b76ib07d130cf7cf251f@mail.gmail.com> <87eimnrv1t.fsf@frosties.localdomain> <76c7f53f0912221349n409ebb0h9639c576562a87cd@mail.gmail.com> Date: Thu, 24 Dec 2009 13:10:07 +0100 In-Reply-To: <76c7f53f0912221349n409ebb0h9639c576562a87cd@mail.gmail.com> (Boris Yakobowski's message of "Tue, 22 Dec 2009 22:49:35 +0100") Message-ID: <87hbrg7eu8.fsf@frosties.localdomain> User-Agent: Gnus/5.110006 (No Gnus v0.6) XEmacs/21.4.22 (linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: goswin-v-b@web.de X-Sender: X-Provags-ID: X-Spam: no; 0.00; yakobowski:01 yakobowski:01 inference:01 type-checker:01 val:01 val:01 checker:01 inferes:01 inference:01 segfault:01 syntax:01 2009:98 mfg:98 polymorphic:01 wrote:01 Boris Yakobowski writes: > On Tue, Dec 22, 2009 at 2:35 PM, Goswin von Brederlow wrote: >> But the type inference should deduce that in >> >> (Obj.magic fn) x >> >> the 'a is actually 'b -> 'c as I am applying an argument to it. > > Sure, and it does. But it remains that the principal type of > (Obj.magic fn) is 'a, without any other constraint on 'a. The fact > that you use it with type 'b -> 'c for some 'b and 'c is irrelevant, > and the type-checker can safely draw conclusions from the principal > type. (This is similar to considering List.map (fun x -> x). It has > type 'a list -> 'a list, even though it is used with type int list -> > int list if you apply it to [1].) > > Hope this helps, > > -- > Boris Nope. # Obj.magic;; - : 'a -> 'b = # let id x = x;; val id : 'a -> 'a = # let f x y = (id x) y;; val f : ('a -> 'b) -> 'a -> 'b = The type checker inferes correctly that the 'a in id must actualy be ('a -> 'b) and gives that type to x. # let g x y = (Obj.magic x) y;; Warning X: this argument will not be used by the function. val g : 'a -> 'b -> 'c = No such luck here. I think the difference is that in Obj.magic there is no connection between the input ('a) and the output ('b). Something I think only Obj.magic has. So the type inference can not infere that the 'a in g must be of type ('d -> 'e) where 'd is compatible with 'b and 'e compatible with 'c (as in it doesn't segfault). Maybe there should be a special Obj.less_magic that preserves the number of arguments between input and output type. Obj.less_magic could only have types 'a -> 'b ('a -> 'b) -> ('c -> 'd) ('a -> 'b -> 'c) -> ('d -> 'e -> 'f) ... That would be something that needs to be hardcoded into the type inference or needs a new type syntax. But it would give verry little extra security. Obj.magic just is evil. :) MfG Goswin