From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p667iOuL021588 for ; Wed, 6 Jul 2011 09:44:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuoEACMRFE7RVda2kGdsb2JhbAA9AQMSnF+LHwgUAQEBAQkJDQcUBCGIeqcsjnWEaokhAgMGhjAEh0SKfIYYhg88gT+CKQ X-IronPort-AV: E=Sophos;i="4.65,484,1304287200"; d="scan'208";a="102601471" Received: from mail-iw0-f182.google.com ([209.85.214.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 06 Jul 2011 09:44:18 +0200 Received: by iwr19 with SMTP id 19so10461625iwr.27 for ; Wed, 06 Jul 2011 00:44:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; bh=UQkZ67RY120nHigpjCnXbPbrHYBh6xcTGWygkBn/OdU=; b=Uw4SerRw0EHfiKBYoC4GgTsFXepQGtzCPP72chO6DKaXXGysY00AO1yQ3+3CwA87zp LMrtr62KLpepU+G9rzVQs8mA5cORb+iBpIQ/d1wVswM1vCPU6ySL8EIM4gVTdRcTN8Lo Kjh5AqnjMdWFWmiCzbGoASK5hNSJXtJUzpA7k= Received: by 10.42.147.137 with SMTP id n9mr8353287icv.383.1309938257100; Wed, 06 Jul 2011 00:44:17 -0700 (PDT) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id d8sm8492075icy.21.2011.07.06.00.44.14 (version=TLSv1/SSLv3 cipher=OTHER); Wed, 06 Jul 2011 00:44:15 -0700 (PDT) Sender: Jacques Garrigue Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Wed, 6 Jul 2011 16:44:12 +0900 Cc: caml-list@inria.fr Message-Id: <0E8CCD89-8740-4462-97AD-8555FDA4EBE6@math.nagoya-u.ac.jp> References: <098226D8-77AA-4F80-97A5-F72F47C6A98E@math.nagoya-u.ac.jp> To: malc X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p667iOuL021588 Subject: Re: [Caml-list] Type inference and marshalling On 2011/07/06, at 14:11, malc wrote: > On Wed, 6 Jul 2011, Jacques Garrigue wrote: > >> On 2011/07/05, at 22:59, malc wrote: >> >>> Perhaps someone could explain why following behaves the way it does: >>> >>> ~$ ocaml >>> Objective Caml version 3.11.2 >>> >>> # let f ic = let i = input_value ic in let j = i + 1 in LargeFile.seek_in ic i;; >>> Warning Y: unused variable j. >>> val f : in_channel -> unit = >> >> The return type of input_value being 'a, which gets generalized by the >> relaxed value restriction, i gets the polymorphic type "forall 'a. 'a". >> So you can use it both as an int and an int64. >> ==> input_value is an unsafe function, you should always write a type >> annotation on its return type. > > Sure i'm well aware of that, but to me "let j = i + 1" means that i has > type int and after that "LargeFile.seek ic i" makes no sense yet is > accepted by the type checker. But this is just the definition of let polymorphism... If the type of a let-bound value contains variables, they can be generalized (with some restriction for soundness). So i can perfectly have several types. What makes no sense here is the return type of input_value, yet this cannot be avoided since there is currently no mechanism in ocaml to actually check the type of the value received. I have no simple solution for this with the current standard library. A potential way to avoid this problem would be to force the user to provide a monomorphic type: module type T = sig type t end let input_value ic (type a) (t : (module T with type t = a)) : a = Pervasives.input_value ic let f ic = let i = input_value ic (module struct type t = int end : T with type t = int) in let _ = i + 1 in seek_in ic i;; This is verbose, but some syntactic sugar could be easily provided. In the long term, safe input primitives are the solution. Jacques Garrigue