> While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.
I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y".
It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.
> I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program...
chriswarbo's point is: That's one way to think about types. It's not the only way, or even the only valid way. If you're going to disagree with chriswarbo, simply ignoring his/her point and reiterating your own isn't a good way to do it.
Can you demonstrate that your definition is the only valid way to think about types? Can you demonstrate that all other ways are subsets of your way? Those would be useful replies that would actually answer chriswarbo.
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.
"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.
It's also simple enough to direct readers to note that types refer to expressions, not values. It's only through later evaluation relations do those expressions and their values end up sharing types.
Types can be seen both as collections of values and as collections of expressions. (I'm defining a “value” as “something the operational semantics of the language lets you substitute a variable with”.) In a call-by-value language, the former is embeddable in the latter. In a call-by-name or call-by-need language, the two coincide.
I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.
If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.
> If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound.
Just because induction on some types is sound, does not entail that induction on all types is sound. Indeed it's not in general, even though it may be in specific languages.
(1) Induction on datatypes is a powerful tool for reasoning about programs in strict languages, and it's only possible when you regard datatypes as collections of values.
All types in a call-by-value language are two collections: one of values and another of expressions, the former embeddable in the latter. This is plain obvious when you see its operational semantics.
> An introduction like I just gave seems simple enough
Simple enough for what?
And I don't see why a bit of pedantry about Haskell's type system requires rewriting an introduction that's expressive and actually simple, not just "simple enough" from a certain point of view.
It's not pedantry, it's a basic definition. There are plenty of languages with stronger type properties that can't be captured by types-as-sets. While the current introduction may be simple, it's also wrong.
And of what consquence is this purported "error" to the reader of this article? Would you edit a children's book about zoo animals from "This is a lion" to "This is a photograph of a lion printed onto paper?" What pedagogic purpose does your correction serve?
We teach Newton's physics to children (and even many adults) even though they've been supplanted by later theories, not because we don't know what the correct answer is, but because Newtonian physics are much easier to grasp and because they still give a useful view of the world around us, even if they break down in the extremes. Why is this any different?
> And of what consquence is this purported "error" to the reader of this article?
Did you even read my comments? I already listed one falsehood that pervades our industry because types are misunderstand in exactly this way: "It's important not to perpetuate the false notion that sets of simple values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language."
This is blatantly, perniciously false, no doubt leading many people to choose dynamically typed languages to their detriment, yet this is what a reasonable person could conclude from the definitions in this article.
Finally, Newtonian physics governs every interaction an average person will have in their lifetime. The analogy that types-as-sets will suffice for nearly every interaction with types that a programmer will have in their lifetime is simply false. The fact that some programmers don't go beyond their first introduction to types makes a wrong definition almost dangerously false, given how much of our society is run by software.
I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y".
It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.