Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

So you want to learn type theory

purelytheoretical.com

Post reply on HN
Print view View original

31–40 of 51 posts

Re: So you want to learn type theory

#31

Post by psygnisfive »

bsaul wrote: post #30
psygnisfive wrote: post #22

Earlier quoted context omitted.

So I think you're right that you should have a good reason. Fashion isn't enough. Don't learn TT cause its "cool", that would be stupid. For FP, tho.. I would say that you'll be a better functional programmer by knowing TT, even if you don't have a typed language. And if you do have a typed language, you'll want to understand your type system, so learning TT gives you the tools to do that properly. But there's more t…

Reminds of how in basic physics, knowing the units of the result you're looking for helps you find the correct answer. Eg : if you're computing a speed ( m/s), then you'd better divide something that has a distance unit by something that has a time unit.

Yep, that's a perfect analogy. And people have actually used type systems to formalize the concept of units. :)

Re: So you want to learn type theory

#32

Post by psygnisfive »

tel wrote: post #28
psygnisfive wrote: post #19

Earlier quoted context omitted.

I want to disagree a little bit with chas here and just say that type theory as we know it today emerged out of a different, post-computer tradition than old-school Russellian type theory. Modern type theory comes arguably from Martin-Löf and the FP domain. As for what is type theory vs. set theory vs. category theory, I'd put it this way: type theory is a flavor of proof theory built on computational justification o…

How would you feel about something like type theory : "computing" :: FOL : set theory where I mean to say "computing" as generally as you like.

Thats also an appropriate analogy, I think. The main point is, type theory is a tool for reasoning, while set theory is a thing reasoned about. At least in the context of foundational questions. You can flip them, but then it becomes kind of silly, imo.

Re: So you want to learn type theory

#33

Post by JadeNB »

Chinjut wrote: post #26
JadeNB wrote: post #16

Earlier quoted context omitted.

> It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product. This sounds more like universal algebra ( http://www.e…

Category theory is about categories,. One notion which makes sense in the context of a category is the categorical product ( http://en.wikipedia.org/wiki/Product_%28category_theory%29 ). All the examples given are examples of categorical products within suitable categories [e.g., Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about…

Certainly, I didn't mean to imply that you (EDIT: I mean chas) were wrong, just that it didn't feel like the examples that you brought up were in the 'spirit' of category theory. As I mentioned in a sister comment (https://news.ycombinator.com/item?id=8780829), any sufficiently powerful formalisation can encode any other (proof: definition of 'sufficiently powerful'), so that there is no mathematical structure of which it can be said definitively that it is not an instance of category theory—but that doesn't mean that every structure should be so viewed!

For example, to pick on the lcm example (just because it's the one that caught my attention): as you mention, posets are automatically categories, but I don't think that the theory of posets is best viewed as a part of category theory; and, similarly, the product is just a special case of the limit over a discrete category, but I don't think that describing the least common multiple, say, as a limit will be educational to anyone! By contrast, viewing the lcm as part of an unusual algebraic structure on the natural numbers I think can be instructive.

Re: So you want to learn type theory

#35

Post by throwaway_99837 »

JadeNB wrote: post #33
Chinjut wrote: post #26

Earlier quoted context omitted.

Category theory is about categories,. One notion which makes sense in the context of a category is the categorical product ( http://en.wikipedia.org/wiki/Product_%28category_theory%29 ). All the examples given are examples of categorical products within suitable categories [e.g., Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about…

Certainly, I didn't mean to imply that you (EDIT: I mean chas) were wrong, just that it didn't feel like the examples that you brought up were in the 'spirit' of category theory. As I mentioned in a sister comment ( https://news.ycombinator.com/item?id=8780829 ), any sufficiently powerful formalisation can encode any other (proof: definition of 'sufficiently powerful'), so that there is no mathematical structure of w…

I think you should not attach yourself emotionally to whether a certain perspective is "educational" or "instructive" to anyone. Rather, look at both perspectives in a [detached] clinical manner as just things that are.

Re: So you want to learn type theory

#37

Post by Chinjut »

JadeNB wrote: post #33
Chinjut wrote: post #26

Earlier quoted context omitted.

Category theory is about categories,. One notion which makes sense in the context of a category is the categorical product ( http://en.wikipedia.org/wiki/Product_%28category_theory%29 ). All the examples given are examples of categorical products within suitable categories [e.g., Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about…

Certainly, I didn't mean to imply that you (EDIT: I mean chas) were wrong, just that it didn't feel like the examples that you brought up were in the 'spirit' of category theory. As I mentioned in a sister comment ( https://news.ycombinator.com/item?id=8780829 ), any sufficiently powerful formalisation can encode any other (proof: definition of 'sufficiently powerful'), so that there is no mathematical structure of w…

I absolutely think it's instructive to view the LCM as a specific case of meets in a semilattice, and in turn to view these as specialization of a general theory of categorical products. (Why wouldn't it be instructive? If you like, the "unusual algebraic structure" on the natural numbers which might be worth considering is that of a category with products). And I also think that recognition of such analogies and general patterns ubiquitous across mathematics is a large part of the spirit of category theory.

Re: So you want to learn type theory

#38

Post by mkehrt »

freyrs3 wrote: post #21
k__ wrote: post #4

Earlier quoted context omitted.

Well, of you want do implement a type system it could help too.

The academic type theory mentioned in this post is not really terribly important to implementing type systems for general purpose languages. There's this growing divide between the engineering discipline of type systems in general languages and the pure theory people who seem only interested in theorem provers and constructive math.

So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift?

It's all pretty much exactly the same as done in academic type theory for decades.

Re: So you want to learn type theory

#39

Post by tree_of_item »

mkehrt wrote: post #38
freyrs3 wrote: post #21

Earlier quoted context omitted.

The academic type theory mentioned in this post is not really terribly important to implementing type systems for general purpose languages. There's this growing divide between the engineering discipline of type systems in general languages and the pure theory people who seem only interested in theorem provers and constructive math.

So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift? It's all pretty much exactly the same as done in academic type theory for decades.

It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :]

More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having some mildly interesting type structures like sum types, and C++'s "lambdas" obviously have very little to do with type theory, unless you want to make the very weak claim of "anything that has anything to do with the lambda calculus = type theory".

Re: So you want to learn type theory

#40

Post by mkehrt »

tree_of_item wrote: post #39
mkehrt wrote: post #38

Earlier quoted context omitted.

So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift? It's all pretty much exactly the same as done in academic type theory for decades.

It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :] More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having…

Re Java generics: Nope. They came out of UPenn's featherweight java work, see here: http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf

Pierce literally wrote the book on type theory.

Swift is written by type theorists; large chunks of the people who worked on it has a PhD (or part of one) in PL theory.

Post reply on HN