From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id A19CA7F89E for ; Sat, 22 Mar 2014 23:12:16 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yminsky@janestreet.com) identity=pra; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yminsky@janestreet.com designates 38.105.200.229 as permitted sender) identity=mailfrom; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mx5.mail.janestreet.com) identity=helo; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="postmaster@mx5.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmkBAEcKLlMmacjlnGdsb2JhbABYg0FXrAKWa4ENHg4BAQEBAQYWCTyCJQEBAQQnGQEBLAsBDwsLDQ0hIhIBBQEKEgYTEodTAxEDAgifU4sYhFUBBZcYA4cWEQaORzMHhDiYToEyjxAYKYRv X-IPAS-Result: AmkBAEcKLlMmacjlnGdsb2JhbABYg0FXrAKWa4ENHg4BAQEBAQYWCTyCJQEBAQQnGQEBLAsBDwsLDQ0hIhIBBQEKEgYTEodTAxEDAgifU4sYhFUBBZcYA4cWEQaORzMHhDiYToEyjxAYKYRv X-IronPort-AV: E=Sophos;i="4.97,711,1389740400"; d="scan'208";a="53721148" Received: from mx5.janestreet.com (HELO mx5.mail.janestreet.com) ([38.105.200.229]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 22 Mar 2014 23:12:15 +0100 Received: from tot-oib-smtp1.delacy.com ([172.27.22.15] helo=tot-smtp) by mx5.mail.janestreet.com with esmtp (Exim 4.76) (envelope-from ) id 1WRU9E-00074D-8u for caml-list@inria.fr; Sat, 22 Mar 2014 18:12:12 -0400 Received: from tot-dmz-mxgoog1.delacy.com ([172.27.224.14] helo=mxgoog2.janestreet.com) by tot-smtp with esmtps (TLSv1:AES256-SHA:256) (Exim 4.72) (envelope-from ) id 1WRU9E-0005jU-7x for caml-list@inria.fr; Sat, 22 Mar 2014 18:12:12 -0400 Received: from mail-la0-f52.google.com ([209.85.215.52]) by mxgoog2.janestreet.com with esmtp (Exim 4.76) (envelope-from ) id 1WRU9D-0006Rq-24 for caml-list@inria.fr; Sat, 22 Mar 2014 18:12:12 -0400 Received: by mail-la0-f52.google.com with SMTP id ec20so2678628lab.11 for ; Sat, 22 Mar 2014 15:12:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=mBWmQTY9r6nosQXlHTSS0K6sBDm5sd9qDgfdgfc6x70=; b=YKeZdt9ZRkrE45y/BBgmdv0nIN/vnMXtn+HPvuthJWgdLLY2EffZL0/XfOdl/OcIpZ ZOjm926eHb/MviYMlxzEtjutYYXL4aqqvL+lhECw13QZpWTiUFJIWxNo6IzjX8XYfoQL Qi4x/lC18fhcOmFSFacUc8YiBednF1+I7iS1k= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=mBWmQTY9r6nosQXlHTSS0K6sBDm5sd9qDgfdgfc6x70=; b=JQWd1vq/7ztFI8ZSP6hrPO9Q8nwQaWpA+h879XkVa+ICX6jQ4IZN2xCPoxlUmL2nP9 T3uDBd8gfyp9zLlHKbvHePl7XzdghusuI5kc4ejN53ifSYVgTlrDiQhNC0TPZ/qe0M/k Jr0Keez2aVRMRTNHjvACclA/Ru/Uj+D/sz1VFc25Y2dKvKcr91sFJPO6DBoQsY6LVPSG Zg/CWYbynmpNl3YuaB7tZljCBM27ZTGZSJtSER2BMHZiE4SwnLbdN0cpL9FenqXOTbVL RqxlRAKzOHN9xMRjhYXHsuwrdE0xO/IcardM4xt3ZqIdzuXRXDIuTw3zwyG7F3oUigeX UUSA== X-Gm-Message-State: ALoCoQlF5Khwow5eVtOxexATrtgCg7p+vrPRach6FqZxGF18AlNtNz3oGAMLeIaQBsRFKeYeARtqnYFmSo5Kw9dN9cUTVW3OwSruxLRQk7q9x+FaFJ0+z36RGgwJ9jsg5oJvmLGnT6DkODqfE73hWaJ+ybcb7nfgyA== X-Received: by 10.152.120.168 with SMTP id ld8mr39588644lab.12.1395526330384; Sat, 22 Mar 2014 15:12:10 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.152.120.168 with SMTP id ld8mr39588642lab.12.1395526330297; Sat, 22 Mar 2014 15:12:10 -0700 (PDT) Received: by 10.112.170.40 with HTTP; Sat, 22 Mar 2014 15:12:10 -0700 (PDT) In-Reply-To: <2E564C20A45F40FFA6BDB6946F088F03@erratique.ch> References: <532DEC4E.6040505@hot.ee> <2E564C20A45F40FFA6BDB6946F088F03@erratique.ch> Date: Sun, 23 Mar 2014 09:12:10 +1100 Message-ID: From: Yaron Minsky To: =?ISO-8859-1?Q?Daniel_B=FCnzli?= Cc: Misha Aizatulin , "caml-list@inria.fr" Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] typechecking Marshal is of course not type-safe, but it's still worth explaining why this happens. My type-theory is weak, but I'll do my best. A naive mental model of type-checking is that the application of [f] should require [t] to be of type [t2], and the constraint in the return value should constrain [t] to be of type [t1], and thus there should be a type-error. Here are some examples that emphasize the point. utop[2]> let z () : t1 =3D let t =3D Obj.magic () in f t; t;; val z : unit -> t1 =3D If [t] comes in as an argument, we get the expected error: utop[10]> let z t : t1 =3D f t; t;; Error: This expression has type t2 but an expression was expected of type t1 The issue here, I think, is that the result of Obj.magic (or input_value) is truly polymorphic, so it's simultaneously compatible with all types. And the fact that it's in some contexts where it's used doesn't mean its definition is constrained. A value passed in as an argument, however, is monomorphic within the body of the function. Here's a similar example, without using Obj.magic, just using an empty list, whose type is truly polymorphic. utop[11]> let z () : t1 list =3D let t =3D [] in ignore (List.map ~f t); t;; val z : unit -> t1 list =3D On the other hand, if we constraint t at the definition time, we get a type error, because that makes the type not polymorphic. utop[13]> let z () : t1 list =3D let t =3D ([] : t2 list) in t;; Error: This expression has type t2 list but an expression was expected of t= ype t1 list Type t2 is not compatible with type t1 In the end, Daniel's advice of annotating the value at its creation point is sound, but it's worth understanding why. y On Sun, Mar 23, 2014 at 7:40 AM, Daniel B=FCnzli wrote: > Le samedi, 22 mars 2014 =E0 21:02, Misha Aizatulin a =E9crit : >> type t1 =3D T1 >> type t2 =3D T2 >> >> let f T2 =3D () >> >> let input (c : in_channel) : t1 =3D >> let t =3D input_value c in >> f t; >> t > > Unmarshaling is not type-safe, you always need to add a type annotation w= hen you input_value. See the warning in the documentation here [1]. Your pr= ogram should read: > > type t1 =3D T1 > type t2 =3D T2 > > let f T2 =3D () > > let input (c : in_channel) : t1 =3D > let t =3D (input_value c : t1) in > f t; > t > > > > Which the compiler rejects. > > Best, > > Daniel > > [1] http://caml.inria.fr/pub/docs/manual-ocaml-4.01/libref/Marshal.html > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs