Re: de Bruijn indices

[Chet Murthy <chet@watson.ibm.com>]

>>>>> "GM" == Greg Morrisett <jgm@cs.cornell.edu> 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--