Hacker News new | past | comments | ask | show | jobs | submit login

I never claimed it was the only valid definition, but the current set-theoretic definition is simply wrong. The propositional definition is at least right (and fairly common), and isomorphic to other definitions.

Is it set-theoretic though? The article states:

> A type is a collection of possible values.

"Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? Would you also complain if a Web page giving an informal introduction to topology said "a space is a collection of points"? Keep in mind that in HoTT, types are spaces and points are values, and hence those two statements have similar meanings.

I know when I'm writing about technical topics, I often look for words which don't have a widely-used technical definition, since that frees me up to focus on what I want to talk about, rather than getting bogged down in the particulars of this-or-that preconceived notion. I could certainly imagine myself wanting to get across the idea of types "containing" values, and carefully choosing the word "collection" specifically to avoid the baggage associated with the word "set". Maybe the author did the same?

In such cases, I would much rather someone point out an existing field which is the same as what I describe ("Your idea of types as 'collections of values' sounds a lot like HoTT's idea that types are spaces of points"), rather than an existing field which is not what I describe yet uses a similar word ("Your use of the word 'collection' sounds a lot like 'set', which is a different theory without much relevance here")

> "Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints?

I think it's still wrong, but let's get concrete in the more unusual type systems to check. What is the "collection of values" for a type in TyPiCal [1]?

What is the "collection of values" for substructural types, like linear types [2] or affine types [3]?

I don't think "collection", set-based or otherwise, can capture these types.

[1] http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/

[2] https://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf

[3] http://users.eecs.northwestern.edu/~jesse/pubs/alms/tovpucel...

Didn't know about Typical. Like the properties it can prove. Thanks for the link!

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact