Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: de Bruijn indices
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-10-12 (16:50)
From: Chet Murthy <chet@w...>
Subject: Re: de Bruijn indices

>>>>> "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.