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 8F51A7F890 for ; Sun, 23 Mar 2014 13:59:22 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Au4BAGfZLlOFBoIFdGdsb2JhbABYg0HDRYEkDgEMFQg8giUBAQEDAScTCQEoDQIDCws0ElcGExuHVgeqVIRbApdThi4QB456B4MkgRSJVI56gTKUOw X-IPAS-Result: Au4BAGfZLlOFBoIFdGdsb2JhbABYg0HDRYEkDgEMFQg8giUBAQEDAScTCQEoDQIDCws0ElcGExuHVgeqVIRbApdThi4QB456B4MkgRSJVI56gTKUOw X-IronPort-AV: E=Sophos;i="4.97,714,1389740400"; d="scan'208";a="53763110" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 23 Mar 2014 13:59:19 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id EEC3563B1; Sun, 23 Mar 2014 21:59:15 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B46F1411F; Sun, 23 Mar 2014 21:59:15 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 13CF2410E; Sun, 23 Mar 2014 21:59:14 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.2 \(1874\)) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <20140323044133.99286.qmail@www1.g3.pair.com> Date: Sun, 23 Mar 2014 21:59:12 +0900 Cc: avatar@hot.ee, jonathan.protzenko@gmail.com, OCaml Mailing List Content-Transfer-Encoding: 7bit Message-Id: References: <20140323044133.99286.qmail@www1.g3.pair.com> To: Kiselyov Oleg X-Mailer: Apple Mail (2.1874) Subject: Re: [Caml-list] typechecking On 2014/03/23 13:41, oleg@okmij.org wrote: > The complete solution is to update the function > generalize_expansive in typing/ctype.ml > which is responsible for implementing the relaxed value restriction. > The type 'a should not be considered co-variant in 'a. Alas, such a > modification is a bit cumbersome since generalize_expansive is called > recursively. One have to split cases. It is not clear how much benefit > can be gained -- complicating type checker for the sake of a rare > error. I don't think it would make sense anyway. I suppose your rationale is that since 'a is empty in the sound part of the language, if you actually get a value of this type it must be unsound, and should not be generalized. However, this would just be a hack, and would not catch all such errors. For instance 'a list contains the empty list, so we have no reason not to generalize it, but an unsound function might still return a non empty list with this type. Moreover, there are also useful applications of the generalization of 'a. For instance, the following idiom allows you to give an arbitrary polymorphic type to a non-value, which you cannot under the strict value restriction. let y = Obj.magic (f x) let z : ('a -> 'a) t = y So well, unsound functions are unsound, and you have to live with that. In particular _always_ annotate with ground types. Jacques Garrigue