8 ms·

Types versus sets (and what about categories?)

79 points by carnitine 5y ago

bsedlm 5y ago
As I understand this (which arguably I don't), what sets bring to the table (so to say) is a notion of unique identification That said, I wonder if it's at all possible to replace sets (to do all which is founded on sets) with a simple untyped lambda calculus (which I think is "functions at their most abstract") and then re-build mathematics on top of that? I suppose the idea would be to define sets in terms of lambdas and then show all the set axioms etc... This occured to me when I noticed that 'standard' set theory defines functions in terms of sets. If sets can be constructed (defined) in terms of lambdas (and types?), then yes to my own question.
- arjvik 5y ago
  I have no authority to write on this topic, but I think it's most definitely possible. After all, untyped Lambda Calculus is Turing Complete, so it clearly can represent sets somehow.
  - carnitine 5y ago
    Pull this thread far enough and it turns out the Y-combinator is a lambda encoding of Russell’s paradox.
- carnitine 5y ago
  The untyped lambda calculus is inconsistent as a logic, hence you need some notion of types. Type theory is indeed building mathematics from lambdas, though.
  - bsedlm 5y ago
    because of the y-combinator|russell paradox? correct?? better question: any references to a type-based construction of set theory?
    - anchpop 5y ago
      You should read the homotopy type theory book if you’re interesting in things like this :p But to answer your question, there’s one here: https://arxiv.org/abs/1305.3835 https://arxiv.org/abs/1305.3835
colanderman 5y ago
This is an interesting article, but doesn't give a good definition which distinguishes sets from (mathematical) types, though it hints at it with "types are syntax, not semantics". I suppose the main difference (paraphrasing Wikipedia [1]) is: sets are descriptive; types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. (Sets can be uncountably infinite, and whether the axiom of choice holds for such sets is debatable.) Regarding the computer-science flavor of types, which usually (not always) overlay a value system which looks more like set theory, I suppose the difference is: sets describe concrete values, whereas types describe the je-ne-sais-quoi a syntactic element may require or guarantee, such that the program is well-formed. These qualities include such ephemera as object ownership and lifetime, which can distinguish two syntactic elements in a way that sets cannot, and exclude details such as how a value of a type is represented. TLA+ is an example of a language which is based on set-theory, but overlaid with a notion of types closer to this second definition. All values in the language are sets in the set-theory sense -- TRUE, 5, "Hello" are all sets -- but it's considered "silly" (Lamport's term) to mix these values in a way which would belie this underlying representation. Some tools thus perform type-checking, despite that the value language itself is untyped. Similarly, there are different "levels" of expressions and rules regarding how such expressions are linked in terms of these levels, which are not captured by either syntax or values, but rather by a type system of sorts. [1] https://en.wikipedia.org/wiki/Type_theory#Differences_from_set_theory https://en.wikipedia.org/wiki/Type_theory#Differences_from_s...
- whatshisface 5y ago
  >types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. Sequences of rational numbers are the usual way of constructing reals, and f(n): N -> Q is a both a sequence of rational numbers and a valid type in almost any language. Does that type include every sequence of rationals or only those that could be produced by a program in that programming language? I guess there is a third option, that it would represent all computable sequences, but is the computability of a sequence decidable? The question of whether or not the function will ever return if asked for the nth value certainly isn't.
arjvik 5y ago
Where can I get a good, intuitive explanation of what Type Theory really is?
- auggierose 5y ago
  View it as a particular opinion of how collections should be formed. Now take this particular opinion and enforce it by mechanical rules, so that valid collections are exactly those that can be formed by these rules. Voila, you got your type theory. If you want to be really bold, start infusing a notion of construction and proof into your collections. Good luck with finding a good and intuitive explanation for that process.
- stepchowfun 5y ago
  I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use. I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it! If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
layer8 5y ago
> lambda-typed lambda calculus That’s the first time I (consciously) come across the term "lambda-typed" (as opposed to generic "typed lambda calculus"), and a quick Google search didn’t turn up any easily digestible description. Could someone provide more insight on what is meant by "lambda-typed" and how it works?
- stingraycharles 5y ago
  I think it’s referring to this definition from a 2018 paper: https://arxiv.org/abs/1803.10143 https://arxiv.org/abs/1803.10143 “An extended type system with lambda-typed lambda-expressions” If I understand it correctly, it implies that a type itself may be a function.
AnimalMuppet 5y ago
Like bsedlm, I'm not sure that I understand this. But: People keep trying to make types in mathematics be the same thing as types in programming. I think that's wrong. It seems to me that types in mathematics (at least Russell types, and maybe all types) are different from types in programming. They are somewhat connected, but they are different. A type in programming is a set of values, plus a set of valid operations on those values. This is a semantic thing (or at least can be), not merely a syntax thing. Types in math may be interesting, but programmers aren't really writing math papers. They're trying to write programs that work. Programmers therefore care about types as used in programming, not types as used in math.
- zozbot234 5y ago
  A type in programming languages is a property of program expressions, not values, which is used to syntactically verify certain properties of the program. This is what makes them work similarly to types in mathematics.
- carnitine 5y ago
  I’m not sure when they were ever distinct things? The history of types in mathematics and programming is incredibly interwoven. Also, it has been shown time and time again that in an expressive enough type system in a programming context, types are not sets and cannot be modelled by them.
  - auggierose 5y ago
    Of course types can be modelled by sets, just not in the straight forward way you might envision. After all, if you cannot model it in ZFC, how do you prove correctness of your type system?
pmoriarty 5y ago
"category theorists are happy to tell you how much they despise ZF set theory" Why do they despise ZF set theory?
- auggierose 5y ago
  There is for example the book "Sets for Mathematics" [0] by Lawvere, one of the inventors of category theory. Those sets he talks about in his book are category-theoretic sets. Which kind of implies that ZFC sets are NOT for Mathematics :-) [0]: https://www.cambridge.org/core/books/sets-for-mathematics/E899F592AD8FBA9A550B1ED3E1E61EC3 https://www.cambridge.org/core/books/sets-for-mathematics/E8...
- joe_the_user 5y ago
  The article describes several ways that various seemingly simple mathematical objects like integer are defined in set theory using complex combinations of sets and I believe the inelegance of such constructions is the main motivation. The thing is, any constructive definition of (almost)all mathematical objects is likely to share this kind of inelegance imo. But I don't think anyone has come up with an alternative to this.
- IngoBlechschmid 5y ago
  Working category theorist here. I wouldn't subscribe to that statement in this strong form, even though I am convinced that various flavors of type theory are a better foundation for mathematics. But this feature doesn't make me despise ZF set theory. In fact, ZF set theory is a beautifully elegant theory. I love it for studying sets. It's just not my favorite foundation. Additionally to the reasons listed by my siblings, many important results in category theory cannot be adequately formalized in ZF for size reasons. Too often, we have to or want to deal with results concerning categories which are too big to fit into sets (these collections are called "proper classes"). In ZF, we can often only formalize specific instances of our theorems but not the general theorem itself. This is explained in more detail by Mike Shulman here: https://arxiv.org/abs/0810.1279 https://arxiv.org/abs/0810.1279 Among other partial solutions, one is to extend ZF to a theory called ZFC/S where S is a very useful mathematical fiction came to live.
danidiaz 5y ago
A related answer in the CS Stack Exchange: https://cs.stackexchange.com/a/91345/5296 https://cs.stackexchange.com/a/91345/5296 > type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case.

79 points by carnitine 5y ago

As I understand this (which arguably I don't), what sets bring to the table (so to say) is a notion of unique identification That said, I wonder if it's at all possible to replace sets (to do all which is founded on sets) with a simple untyped lambda calculus (which I think is "functions at their most abstract") and then re-build mathematics on top of that? I suppose the idea would be to define sets in terms of lambdas and then show all the set axioms etc... This occured to me when I noticed that 'standard' set theory defines functions in terms of sets. If sets can be constructed (defined) in terms of lambdas (and types?), then yes to my own question.

arjvik 5y ago
I have no authority to write on this topic, but I think it's most definitely possible. After all, untyped Lambda Calculus is Turing Complete, so it clearly can represent sets somehow.
- carnitine 5y ago
  Pull this thread far enough and it turns out the Y-combinator is a lambda encoding of Russell’s paradox.
carnitine 5y ago
The untyped lambda calculus is inconsistent as a logic, hence you need some notion of types. Type theory is indeed building mathematics from lambdas, though.
- bsedlm 5y ago
  because of the y-combinator|russell paradox? correct?? better question: any references to a type-based construction of set theory?
  - anchpop 5y ago
    You should read the homotopy type theory book if you’re interesting in things like this :p But to answer your question, there’s one here: https://arxiv.org/abs/1305.3835 https://arxiv.org/abs/1305.3835

colanderman 5y ago

This is an interesting article, but doesn't give a good definition which distinguishes sets from (mathematical) types, though it hints at it with "types are syntax, not semantics". I suppose the main difference (paraphrasing Wikipedia [1]) is: sets are descriptive; types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. (Sets can be uncountably infinite, and whether the axiom of choice holds for such sets is debatable.) Regarding the computer-science flavor of types, which usually (not always) overlay a value system which looks more like set theory, I suppose the difference is: sets describe concrete values, whereas types describe the je-ne-sais-quoi a syntactic element may require or guarantee, such that the program is well-formed. These qualities include such ephemera as object ownership and lifetime, which can distinguish two syntactic elements in a way that sets cannot, and exclude details such as how a value of a type is represented. TLA+ is an example of a language which is based on set-theory, but overlaid with a notion of types closer to this second definition. All values in the language are sets in the set-theory sense -- TRUE, 5, "Hello" are all sets -- but it's considered "silly" (Lamport's term) to mix these values in a way which would belie this underlying representation. Some tools thus perform type-checking, despite that the value language itself is untyped. Similarly, there are different "levels" of expressions and rules regarding how such expressions are linked in terms of these levels, which are not captured by either syntax or values, but rather by a type system of sorts. [1] https://en.wikipedia.org/wiki/Type_theory#Differences_from_set_theory https://en.wikipedia.org/wiki/Type_theory#Differences_from_s...

whatshisface 5y ago
>types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. Sequences of rational numbers are the usual way of constructing reals, and f(n): N -> Q is a both a sequence of rational numbers and a valid type in almost any language. Does that type include every sequence of rationals or only those that could be produced by a program in that programming language? I guess there is a third option, that it would represent all computable sequences, but is the computability of a sequence decidable? The question of whether or not the function will ever return if asked for the nth value certainly isn't.

arjvik 5y ago

Where can I get a good, intuitive explanation of what Type Theory really is?

auggierose 5y ago
View it as a particular opinion of how collections should be formed. Now take this particular opinion and enforce it by mechanical rules, so that valid collections are exactly those that can be formed by these rules. Voila, you got your type theory. If you want to be really bold, start infusing a notion of construction and proof into your collections. Good luck with finding a good and intuitive explanation for that process.
stepchowfun 5y ago
I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use. I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it! If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

layer8 5y ago

> lambda-typed lambda calculus That’s the first time I (consciously) come across the term "lambda-typed" (as opposed to generic "typed lambda calculus"), and a quick Google search didn’t turn up any easily digestible description. Could someone provide more insight on what is meant by "lambda-typed" and how it works?

stingraycharles 5y ago
I think it’s referring to this definition from a 2018 paper: https://arxiv.org/abs/1803.10143 https://arxiv.org/abs/1803.10143 “An extended type system with lambda-typed lambda-expressions” If I understand it correctly, it implies that a type itself may be a function.

AnimalMuppet 5y ago

Like bsedlm, I'm not sure that I understand this. But: People keep trying to make types in mathematics be the same thing as types in programming. I think that's wrong. It seems to me that types in mathematics (at least Russell types, and maybe all types) are different from types in programming. They are somewhat connected, but they are different. A type in programming is a set of values, plus a set of valid operations on those values. This is a semantic thing (or at least can be), not merely a syntax thing. Types in math may be interesting, but programmers aren't really writing math papers. They're trying to write programs that work. Programmers therefore care about types as used in programming, not types as used in math.

zozbot234 5y ago
A type in programming languages is a property of program expressions, not values, which is used to syntactically verify certain properties of the program. This is what makes them work similarly to types in mathematics.
carnitine 5y ago
I’m not sure when they were ever distinct things? The history of types in mathematics and programming is incredibly interwoven. Also, it has been shown time and time again that in an expressive enough type system in a programming context, types are not sets and cannot be modelled by them.
- auggierose 5y ago
  Of course types can be modelled by sets, just not in the straight forward way you might envision. After all, if you cannot model it in ZFC, how do you prove correctness of your type system?

pmoriarty 5y ago

"category theorists are happy to tell you how much they despise ZF set theory" Why do they despise ZF set theory?

auggierose 5y ago
There is for example the book "Sets for Mathematics" [0] by Lawvere, one of the inventors of category theory. Those sets he talks about in his book are category-theoretic sets. Which kind of implies that ZFC sets are NOT for Mathematics :-) [0]: https://www.cambridge.org/core/books/sets-for-mathematics/E899F592AD8FBA9A550B1ED3E1E61EC3 https://www.cambridge.org/core/books/sets-for-mathematics/E8...
joe_the_user 5y ago
The article describes several ways that various seemingly simple mathematical objects like integer are defined in set theory using complex combinations of sets and I believe the inelegance of such constructions is the main motivation. The thing is, any constructive definition of (almost)all mathematical objects is likely to share this kind of inelegance imo. But I don't think anyone has come up with an alternative to this.
IngoBlechschmid 5y ago
Working category theorist here. I wouldn't subscribe to that statement in this strong form, even though I am convinced that various flavors of type theory are a better foundation for mathematics. But this feature doesn't make me despise ZF set theory. In fact, ZF set theory is a beautifully elegant theory. I love it for studying sets. It's just not my favorite foundation. Additionally to the reasons listed by my siblings, many important results in category theory cannot be adequately formalized in ZF for size reasons. Too often, we have to or want to deal with results concerning categories which are too big to fit into sets (these collections are called "proper classes"). In ZF, we can often only formalize specific instances of our theorems but not the general theorem itself. This is explained in more detail by Mike Shulman here: https://arxiv.org/abs/0810.1279 https://arxiv.org/abs/0810.1279 Among other partial solutions, one is to extend ZF to a theory called ZFC/S where S is a very useful mathematical fiction came to live.

danidiaz 5y ago

A related answer in the CS Stack Exchange: https://cs.stackexchange.com/a/91345/5296 https://cs.stackexchange.com/a/91345/5296 > type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case.