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.
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.
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.
>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.
I think most languages (implicitly) define `->` to include all such functions, not just those which could be defined by the language itself. Otherwise it would not be possible to describe the type of builtin or foreign-language library functions, which often exist explicitly to circumvent language restrictions.
Even constructive logic languages (e.g. Coq) adhere to this definition I believe, else it would be impossible to introduce axioms.
> constructive mathematics does not assume that all reals are computable or constructive. It is agnostic about which reals there are.
Basically, in a computer, the "set of all reals" is irrelevant, only the set of computable reals matters.
(And you can represent many reals without infinite sequenecs, even some exotic ones. You don't need "infinite precision rational approximation", you just need enough precision to disambiguate from all other reals in your program.)
It can be helpful in the computer-science (as considered as studying real machines, not infinite machines) context to very explicitly consider types as literally what they will be in the computer's memory.
For instance, an "int64" in languages that support that type is not "an integer" which may be of unbounded size. It is specifically 2*64 values, and no others.
Things like strings can be imagined as a family of types, one for each size, or as a new sort of thing that can be variable length, but still has a strongly-characterizable upper limit.
It is also valid to consider mathematical types, of course. My point here is not to confuse the two, though. You will make a big mess of things if you are switching back and forth between types that can be represented in real machines and math types without realizing it. Mathematical types turn out to be tricky ways of viewing real programs, because they're much simpler to work with [1] but will bite you when you least expect it if you're not careful when real machine limits affect you.
[1]: One of the things that a lot of people find counterintuitive is why it's simpler to have things like "infinite tapes" and other infinities in the math. The reason is, in a real machine when you reach for another byte in RAM, you have two cases to consider: 1. it's there and 2. it's not. If you have "infinite" RAM, you only have one case. Trying to do real proofs on real machines is a this never ending proliferation of cases to worry about that the infinities make go away. Personally I think of almost every "infinite" that shows up in computer science as the English word "unbounded" instead. It's not that there's literally infinite cells, it's just, you'll never reach for another one and be told it's not there, but at any given point, consumption of whatever resource is finite.
Not quite literally, I would argue -- in almost all modern languages, `int64` doesn't mean just "all 64-bit bit patterns", it means more specifically: "a 64-bit bit pattern in a context in which the program text interprets as an integer value". I.e., although any given `float` bit pattern (member of the set GF(2)^64) is also an `int64` bit pattern (member of the same set), a value of type `float` is not a value of type `int64`.
Alternatively -- the type `int64` is comprised of 2^64 discrete values, distinct from the 2^64 discrete values comprising `float`, which happen to have 64-bit representations which overlap.
I would certainly call that another useful and valid perspective.
Again, the real thing is to make sure you don't accidentally flipflop between them without realizing it, because that leads to confusion. The mathematical definition isn't too hard, the definition I laid out isn't too hard, the definition you give isn't too hard, but the amount of confusion you can get from unknowingly switching between them is almost unbounded.
Is your question similar to the question "there's a string type in almost any language, but does that include a string representation of the 100 states of the 100-state 2-symbol busy beaver winner?"
> One main theme of this work is the importance of notations in mathematics and computer science: new questions were asked and solved only because of the use of AUTOMATH notation, itself a variation of λ-notation introduced by A. Church for representing functions.
The notation is syntax, but types are the semantics (specifically, denotational semantics) that the notation is used for.
In particular, the notation is a syntax that can be mechanically maniplated, so that computers can make semantic computations.
en.wikipedia.org/wiki//Type_theory
> . Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory.
Types can only be reduced to syntax when they are static, because only then can we assign type to nodes in the syntax, and declare that every node must have exactly one type as a matter of syntactic correctness.
(But even then, such as thing as type would be formally regarded as a semantic attribute of the grammar. It's syntax in the sense of being a semantic attribute that can be calculated for a node in the syntax, not syntax in the sense of being part of the grammar.)
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.
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).
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?
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.
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.
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.
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?
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 :-)
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.
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.
> 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.
31 comments
[ 4.1 ms ] story [ 75.0 ms ] threadThat 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.
Type theory is indeed building mathematics from lambdas, though.
better question: any references to a type-based construction of set theory?
But to answer your question, there’s one here: https://arxiv.org/abs/1305.3835
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_s...
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.
Even constructive logic languages (e.g. Coq) adhere to this definition I believe, else it would be impossible to introduce axioms.
twitter.com/andrejbauer/status/1212737159217762304
http://math.andrej.com/2008/02/06/representations-of-uncompu...
> constructive mathematics does not assume that all reals are computable or constructive. It is agnostic about which reals there are.
Basically, in a computer, the "set of all reals" is irrelevant, only the set of computable reals matters.
(And you can represent many reals without infinite sequenecs, even some exotic ones. You don't need "infinite precision rational approximation", you just need enough precision to disambiguate from all other reals in your program.)
For instance, an "int64" in languages that support that type is not "an integer" which may be of unbounded size. It is specifically 2*64 values, and no others.
Things like strings can be imagined as a family of types, one for each size, or as a new sort of thing that can be variable length, but still has a strongly-characterizable upper limit.
It is also valid to consider mathematical types, of course. My point here is not to confuse the two, though. You will make a big mess of things if you are switching back and forth between types that can be represented in real machines and math types without realizing it. Mathematical types turn out to be tricky ways of viewing real programs, because they're much simpler to work with [1] but will bite you when you least expect it if you're not careful when real machine limits affect you.
[1]: One of the things that a lot of people find counterintuitive is why it's simpler to have things like "infinite tapes" and other infinities in the math. The reason is, in a real machine when you reach for another byte in RAM, you have two cases to consider: 1. it's there and 2. it's not. If you have "infinite" RAM, you only have one case. Trying to do real proofs on real machines is a this never ending proliferation of cases to worry about that the infinities make go away. Personally I think of almost every "infinite" that shows up in computer science as the English word "unbounded" instead. It's not that there's literally infinite cells, it's just, you'll never reach for another one and be told it's not there, but at any given point, consumption of whatever resource is finite.
Alternatively -- the type `int64` is comprised of 2^64 discrete values, distinct from the 2^64 discrete values comprising `float`, which happen to have 64-bit representations which overlap.
Again, the real thing is to make sure you don't accidentally flipflop between them without realizing it, because that leads to confusion. The mathematical definition isn't too hard, the definition I laid out isn't too hard, the definition you give isn't too hard, but the amount of confusion you can get from unknowingly switching between them is almost unbounded.
That's a bad paraphrase of the original:
> One main theme of this work is the importance of notations in mathematics and computer science: new questions were asked and solved only because of the use of AUTOMATH notation, itself a variation of λ-notation introduced by A. Church for representing functions.
The notation is syntax, but types are the semantics (specifically, denotational semantics) that the notation is used for. In particular, the notation is a syntax that can be mechanically maniplated, so that computers can make semantic computations.
en.wikipedia.org/wiki//Type_theory
> . Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory.
en.wikipedia.org/wiki/Denotational_semantics
(But even then, such as thing as type would be formally regarded as a semantic attribute of the grammar. It's syntax in the sense of being a semantic attribute that can be calculated for a node in the syntax, not syntax in the sense of being part of the grammar.)
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.
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/Tutor...
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?
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.
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.
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.
Why do they despise ZF set theory?
[0]: https://www.cambridge.org/core/books/sets-for-mathematics/E8...
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.
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
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.
> 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.