Conversation

William J. Bowman @ ICFP
@wilbowma
You are reading a complicated type theory paper, and find a comment “aren’t these telescopes?”. Your mind is full of images of lenses, mirror, parabola, stars. You stare, dumbfounded, at a page of Greek symbols and inference rules. 🧵
5
37
William J. Bowman @ ICFP
@wilbowma
What possible connection between these two worlds could there be? What dark sorcery is this mad man trying to communicate to me? How could a tool of astronomical observations be at all related to type theory? WHAT ISGOINGO 🧵
1
11
Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
and
@wilbowma
Did you check out the source? 🔭
Quote Tweet
🥢 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.
2
2