From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA20913 for caml-red; Fri, 13 Oct 2000 13:49:27 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA13470 for ; Thu, 12 Oct 2000 20:12:44 +0200 (MET DST) Received: from saul.cis.upenn.edu (SAUL.CIS.UPENN.EDU [158.130.12.4]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9CIChf25007 for ; Thu, 12 Oct 2000 20:12:43 +0200 (MET DST) Received: from localhost (localhost [127.0.0.1]) by saul.cis.upenn.edu (8.10.1/8.10.1) with SMTP id e9CI8u022681; Thu, 12 Oct 2000 14:08:56 -0400 (EDT) To: Chet Murthy cc: Greg Morrisett , caml-list@inria.fr Reply-to: bcpierce@cis.upenn.edu Subject: Re: de Bruijn indices In-reply-to: Your message of Thu, 12 Oct 2000 10:57:56 -0400. <200010121457.KAA04527@nautilus-chet.watson.ibm.com> Date: Thu, 12 Oct 2000 14:08:56 EDT Message-ID: <22679.971374136@saul.cis.upenn.edu> From: "Benjamin C. Pierce" Sender: weis@pauillac.inria.fr > Now, there _is_ possibly one way of doing explicit names that would be > fast enough to be a contender -- where the names are chosen uniquely, > using a global counter, so no capture check is required. I can > imagine that that would be fast. This is pretty much how the Pict front end works. We started out with a standard deBruijn representation, but later switched to a scheme where, during parsing, we choose a globally unique spelling for each bound name (they're not *that* ugly). We have to do a little work later to make sure that uniqueness is maintained, but it seems faster on the whole. B