Conversation

🥢 Jon 🧄
@ionathanch
tbh chasing down references for weird type theory terminology is kinda fun. TIL that these things (x: A)(y: B y)(z: C x y) are called telescopes (probably?) due to de Bruijn, from "Telescopic mappings in typed lambda calculus" (over an unfortunate page break):
these abstractors are [x:real][y:P(x)]. If, for example, the function is complex-values, then its type becomes [x:real][y:P(x)]compl. In such a sequence of two or more abstractors the type of the second may depend on the variable in the first, the type of the third may depend on the variables of the first two, etc. It reminds of a old-fashioned telescope consisting of a sequence of segments of decreasing width, where each segment can be shifted into the
previous one. That is why these abstractor strings are called telescopes.
1
25