4 ms·

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 syn

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.
- colanderman 5y ago
  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.
- gowld 5y ago
  Andrej Bauer is a great resource twitter.com/andrejbauer/status/1212737159217762304 http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ 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.)
- jerf 5y ago
  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.
gowld 5y ago
> "types are syntax, not semantics". 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
- colanderman 5y ago
  FWIW, it is the article's author's paraphrase, not mine.
kazinator 5y ago
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.)

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.

colanderman 5y ago
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.
gowld 5y ago
Andrej Bauer is a great resource twitter.com/andrejbauer/status/1212737159217762304 http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ 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.)
jerf 5y ago
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.

gowld 5y ago

> "types are syntax, not semantics". 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

colanderman 5y ago
FWIW, it is the article's author's paraphrase, not mine.

kazinator 5y ago

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.)