From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 38BCA7F89E for ; Sat, 22 Mar 2014 23:24:29 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of jonathan.protzenko@gmail.com) identity=pra; client-ip=74.125.82.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="jonathan.protzenko@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of jonathan.protzenko@gmail.com designates 74.125.82.47 as permitted sender) identity=mailfrom; client-ip=74.125.82.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="jonathan.protzenko@gmail.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@mail-wg0-f47.google.com) identity=helo; client-ip=74.125.82.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="postmaster@mail-wg0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYBAJ4MLlNKfVIvlGdsb2JhbABYgmVcg16oe5ZrgRUWDgEBAQEHCwsJEiqCJQEBAQQjBAsBDQEbEgoCAwwGBQsNAgIFBBILAgIJAwIBAgEREQEFAQoSEwYCAQEOh1IBAxEBBAifUIwOUYMOllQKGScDCmSGKBEBBQyBHY0eOoJvgUkEmEqBMo8QQYRc X-IPAS-Result: AqYBAJ4MLlNKfVIvlGdsb2JhbABYgmVcg16oe5ZrgRUWDgEBAQEHCwsJEiqCJQEBAQQjBAsBDQEbEgoCAwwGBQsNAgIFBBILAgIJAwIBAgEREQEFAQoSEwYCAQEOh1IBAxEBBAifUIwOUYMOllQKGScDCmSGKBEBBQyBHY0eOoJvgUkEmEqBMo8QQYRc X-IronPort-AV: E=Sophos;i="4.97,711,1389740400"; d="scan'208";a="53721794" Received: from mail-wg0-f47.google.com ([74.125.82.47]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Mar 2014 23:24:28 +0100 Received: by mail-wg0-f47.google.com with SMTP id x12so2480092wgg.6 for ; Sat, 22 Mar 2014 15:24:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:content-type:content-transfer-encoding; bh=mQs5m6iAMn67dkX47eGYdPCb2O4dZ9/20XtuQzbWLmA=; b=vJJmg/SxGEUqYuuKGLfNi11a5tNME3tjvicP9lmryQqvIIEb37V6CnIyjZZtdt34XR aQmOwubm2e0W09OVaGQsriv5WKLDOcpxQ86N/PFY5mXyQ/WwDsbXRlpJuRa5my5RJWtZ 5nuxCSs4tQ1mCdmmxrnqarjogCNmV1XUrLDA1Abqkaw9x5o/Q89ReFAdCijxo7WJaCf6 TXtUMdZ4L9e1aeSSuLieV1t1zv2oeqvs+rsVKvzUOZP/pPuSlFC4n3Bkxh2fZbC8edai PykuJluLXI0T9YPbSnrRXVNQNNLXR+ul+4GLhsZooGjHHuEZ+0a9VY1zVBMwmyVd80Jv sVtQ== X-Received: by 10.180.98.71 with SMTP id eg7mr5454792wib.31.1395527067942; Sat, 22 Mar 2014 15:24:27 -0700 (PDT) Received: from ?IPv6:2a01:e35:2f37:f210:5e26:aff:fe0c:c1d8? ([2a01:e35:2f37:f210:5e26:aff:fe0c:c1d8]) by mx.google.com with ESMTPSA id t6sm20217516wix.4.2014.03.22.15.24.26 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 22 Mar 2014 15:24:27 -0700 (PDT) Message-ID: <532E0D98.1030207@gmail.com> Date: Sat, 22 Mar 2014 23:24:24 +0100 From: Jonathan Protzenko User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Firefox/31.0 Thunderbird/31.0a1 MIME-Version: 1.0 To: caml-list@inria.fr References: <532DEC4E.6040505@hot.ee> <2E564C20A45F40FFA6BDB6946F088F03@erratique.ch> In-Reply-To: Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] typechecking I was also surprised by this example, and I kind of expected input_value to have type in_channel -> '_a. However, input_value is defined as follows: stdlib/pervasives.ml 365:external input_value : in_channel -> 'a = "caml_input_value" Since writing '_a is not allowed, I guess there's not much we can do here. Cheers, ~ jonathan On Sat 22 Mar 2014 11:12:10 PM CET, Yaron Minsky wrote: > 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 = let t = Obj.magic () in f t; t;; > val z : unit -> t1 = > > If [t] comes in as an argument, we get the expected error: > > utop[10]> let z t : t1 = 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 = let t = [] in ignore (List.map ~f t); t;; > val z : unit -> t1 list = > > 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 = let t = ([] : t2 list) in t;; > Error: This expression has type t2 list but an expression was expected of type > 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ünzli > wrote: >> Le samedi, 22 mars 2014 à 21:02, Misha Aizatulin a écrit : >>> type t1 = T1 >>> type t2 = T2 >>> >>> let f T2 = () >>> >>> let input (c : in_channel) : t1 = >>> let t = input_value c in >>> f t; >>> t >> >> Unmarshaling is not type-safe, you always need to add a type annotation when you input_value. See the warning in the documentation here [1]. Your program should read: >> >> type t1 = T1 >> type t2 = T2 >> >> let f T2 = () >> >> let input (c : in_channel) : t1 = >> let t = (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 >