De Bruijn indices as first encounter - General

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Pedro Minicz

I image a bunch of people here have encountered the lambda calculus somewhere. Maybe for some, even before function programming languages. My question is: has anyone been introduced to or seen introductory material that jumps straight to De Bruijn indices, avoiding named variables all together? If so, how was the learning experience? Do you believe it was "harder" than it should have been or "equivalent" (I suppose its normal to struggle with lambda calculus a bit in the beginning, even without De Bruijn indices)?

Stuart Terrett

_Types and Programming Languages_ discusses lambda calculus with variables "up to renaming", then solves the problem by using DeBruijn indices. I'm not sure you could motivate them any faster than that, honestly. The only implementation given uses DeBruijn.