[HN Gopher] Types versus sets (and what about categories?)
___________________________________________________________________
Types versus sets (and what about categories?)
Author : carnitine
Score : 66 points
Date : 2022-03-16 11:13 UTC (1 days ago)
(HTM) web link (lawrencecpaulson.github.io)
(TXT) w3m dump (lawrencecpaulson.github.io)
| arjvik wrote:
| Where can I get a good, intuitive explanation of what Type Theory
| really is?
| stepchowfun wrote:
| 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/Tutor...
| auggierose wrote:
| 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.
| pmoriarty wrote:
| _" category theorists are happy to tell you how much they despise
| ZF set theory"_
|
| Why do they despise ZF set theory?
| joe_the_user wrote:
| 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.
| auggierose wrote:
| 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/E8...
| AnimalMuppet wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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?
| danidiaz wrote:
| A related answer in the CS Stack Exchange:
| 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.
| bsedlm wrote:
| 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 wrote:
| 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 wrote:
| Pull this thread far enough and it turns out the Y-combinator
| is a lambda encoding of Russell's paradox.
| carnitine wrote:
| 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 wrote:
| because of the y-combinator|russell paradox? correct??
|
| better question: any references to a type-based construction
| of set theory?
| anchpop wrote:
| 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
| layer8 wrote:
| > 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 wrote:
| I think it's referring to this definition from a 2018 paper:
|
| 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.
| colanderman wrote:
| 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_s...
| kazinator wrote:
| 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 wrote:
| > _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.
| gowld wrote:
| Andrej Bauer is a great resource
|
| 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.)
| jerf wrote:
| 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.
| colanderman wrote:
| 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.
| colanderman wrote:
| 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.
| tshaddox wrote:
| 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?"
| gowld wrote:
| > "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 l-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 wrote:
| FWIW, it is the article's author's paraphrase, not mine.
___________________________________________________________________
(page generated 2022-03-17 23:01 UTC)