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 SAA12331 for caml-red; Thu, 12 Oct 2000 18:50:13 +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 RAA09597 for ; Thu, 12 Oct 2000 17:00:09 +0200 (MET DST) Received: from igw8.watson.ibm.com (igw8.watson.ibm.com [198.81.209.20]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9CF08f22312 for ; Thu, 12 Oct 2000 17:00:09 +0200 (MET DST) Received: from sp1n189at0.watson.ibm.com (sp1n189at0.watson.ibm.com [9.2.104.62]) by igw8.watson.ibm.com (8.9.3/8.9.3/05-14-1999) with ESMTP id LAA03300; Thu, 12 Oct 2000 11:00:06 -0400 Received: from nautilus-chet.watson.ibm.com (lig32-227-60-77.us.lig-dial.ibm.com [32.227.60.77]) by sp1n189at0.watson.ibm.com (8.9.3/Feb-20-98) with ESMTP id LAA34756; Thu, 12 Oct 2000 11:00:03 -0400 Received: from nautilus.chet.org (localhost [127.0.0.1]) by nautilus-chet.watson.ibm.com (8.9.3/8.9.3/Debian 8.9.3-21) with ESMTP id KAA04527; Thu, 12 Oct 2000 10:57:56 -0400 Message-Id: <200010121457.KAA04527@nautilus-chet.watson.ibm.com> X-Authentication-Warning: nautilus.chet.org: Host localhost [127.0.0.1] claimed to be nautilus.chet.org To: Greg Morrisett cc: caml-list@inria.fr Subject: Re: de Bruijn indices In-reply-to: Your message of Tue, 10 Oct 2000 14:09:44 EDT. <706871B20764CD449DB0E8E3D81C4D43BFCA25@opus.cs.cornell.edu> Date: Thu, 12 Oct 2000 10:57:56 -0400 From: Chet Murthy Sender: weis@pauillac.inria.fr >>>>> "GM" == Greg Morrisett writes: GM> Well, I can say from my own experience that de Bruijn isn't GM> always best. Neither NuPRL nor the TAL type-checker uses GM> indices, prefering named variables instead. For both, GM> preserving original names is really useful when debugging. I can't speak to TAL. I _can_ speak for Nuprl, having implemented a version of Nuprl in SML/NJ in 1990, and having re-implemented it, by a process of iterative migration, in Coq, in 1992-1994. Explicit names were *significantly* slower than deBruijn indices. The costs were there, even though I did the standard tricks of caching free-vars under binders, and even though I wrote the most careful code I could think of to make explicit names faster. It wasn't the substitution that was killing me, but the alpha-conversion, and checks for alpa-conversion. 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. --chet--