Types versus sets in math and programming languages
The slogan is that types are intensional, whereas sets are extensional. (...) That is:
- Sets are characterized by the
relation: we can ask which items are elements of a set and which are not.
- Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.
That seems an important distinction, especially since TTM allowed types of infinite cardinality. Any relation schema (type?) whose heading includes an attribute type of infinite cardinality, is thereby also of infinite cardinality. So we can think of constructing relation values from the values constructed for each attribute type.
Quote from AntC on June 30, 2021, 5:00 amhttps://byorgey.wordpress.com/2021/06/24/types-versus-sets-in-math-and-programming-languages/
Thanks. Have you thought about leaving a comment?
The article is interesting, but too much preamble and not enough substance. Maybe in the next post...
The slogan is that types are intensional, whereas sets are extensional. (...) That is:
- Sets are characterized by the
- Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.
That seems an important distinction, especially since TTM allowed types of infinite cardinality. Any relation schema (type?) whose heading includes an attribute type of infinite cardinality, is thereby also of infinite cardinality. So we can think of constructing relation values from the values constructed for each attribute type.
I agree it's important, but I found the treatment problematic: too much left unsaid. A type is a set of values, known at compile time. Sets (in a computer language) are values of a type, which may or many not be known at compile time. Values are not constructed, but memory is allocated to hold a value.
Pascal had sets, and very useful they were too (as part of the language, not just in the library).
At the end of the day he's having fund creating a language -- don't we all relate to that?
Quote from dandl on June 30, 2021, 7:16 amQuote from AntC on June 30, 2021, 5:00 amhttps://byorgey.wordpress.com/2021/06/24/types-versus-sets-in-math-and-programming-languages/
Thanks. Have you thought about leaving a comment?
The article is interesting, but too much preamble and not enough substance. Maybe in the next post...
He's on sabbatical next semester. I guess there's (a lot) more to come. Brent is/was one of the superstars of the Haskell world. I guess he went and got a teaching position, and that put an end to his major contributions.
The slogan is that types are intensional, whereas sets are extensional. (...) That is:
- Sets are characterized by the
- Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.
That seems an important distinction, especially since TTM allowed types of infinite cardinality. Any relation schema (type?) whose heading includes an attribute type of infinite cardinality, is thereby also of infinite cardinality. So we can think of constructing relation values from the values constructed for each attribute type.
I agree it's important, but I found the treatment problematic: too much left unsaid. A type is a set of values, known at compile time. Sets (in a computer language) are values of a type, which may or many not be known at compile time. Values are not constructed, but memory is allocated to hold a value.
Pascal had sets, and very useful they were too (as part of the language, not just in the library).
Hmm hmm. Sets were implemented as a bit-vector. Good luck trying to code a set of Int's. Or of some structured/product type with sub-fields.
At the end of the day he's having fund creating a language -- don't we all relate to that?
Interesting typo. I'd be pretty sure he's getting no funding for this beyond his salary; so yes it's for fun only.
BTW re "We could try to completely get rid of the distinction, but this seems like it would lead directly to a dependent type system and refinement types. " Haskell has decided to support dependent types -- not only is this a great deal of complexity, the language will IMO have long periods of 'down time' while they try to figure out how to achieve it, and then to fix what they broke, and then to make it performant again. Re 'refinement types' that Brent links to, there's a small group working outside Haskell HQ (I'd almost say against Haskell HQ), but 'Liquid Haskell' looks a whole heap more useful. (For Haskell HQ being 'useful' is not a motivation.) HQ has already implemented something called type-in-type, which is on a path to conflate types and values: what seems to be a value (like True) can appear as a type -- in which case its type-of-type is Bool.
None of this abstraction-gymnastics has delivered anything looking a like a record system.