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 NAA21269 for caml-red; Fri, 13 Oct 2000 13:48:49 +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 TAA12789 for ; Thu, 12 Oct 2000 19:33:25 +0200 (MET DST) Received: from opus.cs.cornell.edu (exchange.cs.cornell.edu [128.84.97.8]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9CHXOf24637 for ; Thu, 12 Oct 2000 19:33:24 +0200 (MET DST) Received: by opus.cs.cornell.edu with Internet Mail Service (5.5.2650.21) id ; Thu, 12 Oct 2000 13:33:23 -0400 Message-ID: <706871B20764CD449DB0E8E3D81C4D43BFCA51@opus.cs.cornell.edu> From: Greg Morrisett To: "'Chet Murthy'" Cc: caml-list@inria.fr Subject: RE: de Bruijn indices Date: Thu, 12 Oct 2000 13:33:23 -0400 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2650.21) Content-Type: text/plain; charset="iso-8859-1" Sender: weis@pauillac.inria.fr > It wasn't the substitution that was killing me, but the > alpha-conversion, and checks for alpa-conversion. But alpha-conversion is a form of substitution... > 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. > > Of course, it would result in uggggggly names -- uglier than deBruijn > numbers, unless similar tricks were played in pretty-printing. This is essentially what we did in TAL -- each variable had a string-based name and a number field. Numbers defaulted to zero (and weren't printed). When we needed to alpha-convert something, we incremented a global counter and used this for the new number (keeping the string the same.) You do end up with foo_12349 this way, but only if something has to be alpha-converted -- and that turned out to be pretty rare. Again, I haven't re-implemented things with De Bruijn, and would like too. It may be that TAL would run faster with a well-implemented scheme. Two side notes: 1. The reason I can't easily re-implement TAL using de Bruijn instead of explicit names, is that I exposed my term datatypes to make pattern matching easy. If I'd been coding in something like Java, I suspect I would've abstracted terms enough that re-writing the code would've been easier. One problem with ML is that the convenience of pattern matching tends to direct you (or at least me) to expose too much representation information. Abstract patterns would help a lot... 2. I seem to recall that there are subtle issues with typed calculi (especially dependently-typed calculi) and de Bruijn? Certainly explicit substitutions are tricky in this setting... -Greg