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 q2M9mfKp026542 for ; Thu, 22 Mar 2012 10:48:41 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag4BACX1ak9KfVK2kGdsb2JhbABCtyYIIgEBAQEJCQ0HFAQjgiICExMGARQlAw0FXyABBQEBNAkZh2gLnhmCXQqPBIUXgU0BBQsIilCCX4I/YwSVXoszgxc9gVeCM4Fb X-IronPort-AV: E=Sophos;i="4.73,629,1325458800"; d="scan'208";a="137226845" Received: from mail-we0-f182.google.com ([74.125.82.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Mar 2012 10:48:27 +0100 Received: by wern13 with SMTP id n13so2816507wer.27 for ; Thu, 22 Mar 2012 02:48:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:subject:message-id:mime-version:content-type :content-disposition:user-agent; bh=ovfQ4TstTHXylBKRw/icWoT0VARfqkK91IHFm0+LGL0=; b=uD1Num+nnUeyKGgWtQtH3hCgsaxtLXrOQloSMQtveun0WW20Nl+R+sMeOn/Xpb8nHg SP1Knm/abqcU/GSRwhzSSuSfr2tEE2ouczjRPNH1xitBnCi7eAJJj8ZnAtAh4v5xDnrl ch8nq/h0rQ/y4TyiIOBmmL/bE1mtgAFJ/OZRezvySbyZP5vwa/TMOMVSC9wgZRsAlHP4 mB7V9wB+P2r09B6NHPlVH25j8RWYpdfzVPzdyulwT0X4yGxwsxfxrbVWym25eqTFnu+n +JJxZ7MeQfQxB0/a5M6aRtWTVF55RKDPcRY8bZtmhKn6OqUZH+RxPMvlDefHKE7nceTa mBHQ== Received: by 10.180.102.129 with SMTP id fo1mr3565374wib.6.1332409707604; Thu, 22 Mar 2012 02:48:27 -0700 (PDT) Received: from voyager (knopper.inria.fr. [128.93.60.80]) by mx.google.com with ESMTPS id fn2sm6860059wib.0.2012.03.22.02.48.26 (version=TLSv1/SSLv3 cipher=OTHER); Thu, 22 Mar 2012 02:48:26 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by voyager with local (Exim 4.72) (envelope-from ) id 1SAegJ-0007rG-Kn for caml-list@inria.fr; Thu, 22 Mar 2012 10:51:43 +0100 Date: Thu, 22 Mar 2012 10:51:43 +0100 From: Roberto Di Cosmo To: caml-list@inria.fr Message-ID: <20120322095143.GA30016@voyager> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Subject: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? I was playing around some more with GADTs, preparing my next course on functional programming, and came across an example on which the type checker outputs a type containing a funny name for a type variable. I do not know if this qualifies as a bug, so before filing it, I'd love some feedback. Here we are: I am writing an example to show how one can code a well typed length function for empty/nonempty list; we start with the type definition type empty type nonempty type ('a, 'b) l = Nil : (empty, 'b) l | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;; then we move on to the length function let rec length : type a b. (a,b) l -> 'a = function | Nil -> 0 | (Cons (_,r)) -> 1+ (length r);; Hey, you say, the natural type to declare for length should be type a b. (a,b) l -> int but as you see, for some mysterious reason I ended up writing something silly (dont ask why, I am just very well known to step on strange bugs as easily as I breath) type a b. (a,b) l -> 'a The type checker is happy anyway: 'a will be instantiated to int, and the declaration of length is accepted... but now look at the output type val length : ('a1, 'b) l -> int = Why do we get 'a1, and not 'a, in the type? Well, probably, since 'a is instantiated to int during type checking, it may be the case that 'a, as type name, is still marked as taken during the type output, so we get ('a1,'b) The type is perfectly sound... it is just 'surprising' for a regular user... do you think this should be considered a bug? --Roberto ------------------------------------------------------------------ Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo FRANCE. Twitter: http://twitter.com/rdicosmo ------------------------------------------------------------------ Attachments: MIME accepted, Word deprecated http://www.gnu.org/philosophy/no-word-attachments.html ------------------------------------------------------------------ Office location: Bureau 6C08 (6th floor) 175, rue du Chevaleret, XIII Metro Chevaleret, ligne 6 ------------------------------------------------------------------