Comment by zanzibar7 on Basic building blocks of dependent type theory · 2023-06-21T16:16:16.918Z · LW · GW

Thanks for these posts.  I've just started working through them, but great so far.

I became curious recently if some concept of homogenous sets should be serving foundation for applied mathematics, and that's lead me to a deeper curiousity about type theory.  Types are already been a core concept in programming and databases for decades.  Working on sympy, it was distressing how much work had to go on under the hood to make sure objects were really of right type to do a calculation, and how dis-organized, bug-prone, and inefficient this became.  How many engineering mistakes could be avoided if physics and chemistry variables used in compuations had types accounted for their units automatically, or mismatched units could raise a warning?  Or the conceptual difference between a date and a duration?  It seems like something that should be a core part of university math sometimes.

But type theory has always felt like a rabbit hole when it comes to doing stuff.  Your specification above reminded me of this.

>There are three basic building  blocks in type theory: values, functions, and types. (And then you  can additionally construct ordered pairs out of any combination of these.) Values could also be seen as constant functions that don’t accept any arguments, so, in a sense there are only functions and types, but we will talk about “values” as separate things nevertheless.

If we define everything in terms of functions, than we don't need values.  For the same reason, its just useful to think of many undergraduate calculations as taking place over ℂ rather than ℚ or ℝ.  But that means you need to understand ℂ before you should really be doing anything.  But then we've got vectors, and matrices, and tensors ...  With python's numpy, it's extra cognitive load to have to worry about whether a returned value's type is a float or a 1x1 array, or maybe even some other equivalent type.

And that's where I start to get turned off from type theory.  Instead of giving me the foundation to express the ideas I'm really interested it, it is getting in the way.