RE: de Bruijn indices

[Greg Morrisett <jgm@cs.cornell.edu>]

> 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