3 ms·

The types of data

23 points by tel 12y ago

colanderman 12y ago
You told me only about algebraic types of data. There exist other type systems that are equally valid. For example, one can imagine a relational type system which describes values (which are finite sets of tuples having named, unordered fields) by their cardinality (0, 1, >1, 0 or 1, >0, or any) the field names they contain, and the types of the values of those fields. You can extend this system in several ways as well; the type can include keys (sets of fields for which each tuple in the set contain distinct values) and dependent field specifications (denoting fields which are present/have a given type only if some other given field has a certain value).
- tel 12y ago
  That's a fair critique and I hope my post suggested an understanding that I wrote from a rather exposed position. The reason I chose to call these "the" types of data is not because there exist no other reasonable mechanisms for defining things like types and data but instead because there's such a strong relationship between this presentation of types and the foundations of intuitionistic logic. You can also find these types in category theory (given a sufficiently nice category) which further cements their conceptual power. Further, you can refine this presentation to make a dependent type theory and end up with a really wonderful place to express something like your relational type system.
  - tel 12y ago
    (To go a little further on this I'd want to dive into what "validity" means in terms of a type system. Frankly, I'm not sure I can do a good job at defining that at all. I'm not even totally certain anyone can, though I imagine that's not true. Some things I would point toward are consistency, existence of many models, Gentzen Inversion if you're defining things in a natural deduction format, etc.)
    - colanderman 12y ago
      I used "valid" very loosely – I mean roughly, useful for describing typical data in a way that helps catch bugs without impeding usability. One of my issues with algebraic types is the awkwardness of describing enumerable arrays and sets. Both end up being represented as some kind of binary tree. (I say "enumerable" because obviously functions can easily represent non-enumerable arrays and sets.) Relational types can describe both trivially. I'm sure relational types have weaknesses likewise (though I can't think of any off the top of my head). A non-parametric relational type system – which doesn't permit field values to themselves be relations, such as in SQL – has obvious difficulties specifying recurrent structures. (You can of course flatten these using pointers, but without dependent constraints you can't catch bugs.)
      - tel 12y ago
        I think we're discussing slightly different things. I'd like to eventually get this line of reasoning closer to where you are, but right now my interest in describing ADTs has less to do with representation of useful things and more to do with "these types form a basis for thinking about computation". Effectively, products are the quintessential "grouping" notion, sums the quintessential "choice" notion, and implications the quintessential "hypothetical" notion. So those are pretty important for describing any computation. All that said, I really like relational types and wish they were more commonly used. I do think it takes some effort to model them in ADTs and that a system which provided them more directly would be fun.
felixgallo 12y ago
Coming from a formal symbolic logic background and 30 years of software development in typed and typeless imperative and functional languages, it's incredibly interesting, pleasurable, and more than a little frustrating to not understand this blog post in the slightest. Not only do the words not really make sense to me in the order they're presented; and not only do the assertions seem alien and foreign in nearly every respect; but I can't fathom a pragmatic path by which even if I accepted everything here as given, it would give me an intuition I could use to do anything different or better than I do now. And that's neat, because there's apparently (given the footnotes) a bunch of people for whom that is not true, so I have to be missing something somewhere, and that's a learning opportunity. And certainly I've enjoyed your other blog posts, tel, for their clarity and brevity and informational content. Nevertheless this is problematic, because I'm probably your target audience, and I couldn't be any more baffled or concerned by the idea that you'd be blithely mapping "+" (sum, addition) to "\/" (logical-or, disjunction) across fields and asserting conceptual equivalence like it's a given, much less a foundational building block of an argument. Now off to bounce harmlessly off that blog post a few more times.

23 points by tel 12y ago

You told me only about algebraic types of data. There exist other type systems that are equally valid. For example, one can imagine a relational type system which describes values (which are finite sets of tuples having named, unordered fields) by their cardinality (0, 1, >1, 0 or 1, >0, or any) the field names they contain, and the types of the values of those fields. You can extend this system in several ways as well; the type can include keys (sets of fields for which each tuple in the set contain distinct values) and dependent field specifications (denoting fields which are present/have a given type only if some other given field has a certain value).

tel 12y ago
That's a fair critique and I hope my post suggested an understanding that I wrote from a rather exposed position. The reason I chose to call these "the" types of data is not because there exist no other reasonable mechanisms for defining things like types and data but instead because there's such a strong relationship between this presentation of types and the foundations of intuitionistic logic. You can also find these types in category theory (given a sufficiently nice category) which further cements their conceptual power. Further, you can refine this presentation to make a dependent type theory and end up with a really wonderful place to express something like your relational type system.
- tel 12y ago
  (To go a little further on this I'd want to dive into what "validity" means in terms of a type system. Frankly, I'm not sure I can do a good job at defining that at all. I'm not even totally certain anyone can, though I imagine that's not true. Some things I would point toward are consistency, existence of many models, Gentzen Inversion if you're defining things in a natural deduction format, etc.)
  - colanderman 12y ago
    I used "valid" very loosely – I mean roughly, useful for describing typical data in a way that helps catch bugs without impeding usability. One of my issues with algebraic types is the awkwardness of describing enumerable arrays and sets. Both end up being represented as some kind of binary tree. (I say "enumerable" because obviously functions can easily represent non-enumerable arrays and sets.) Relational types can describe both trivially. I'm sure relational types have weaknesses likewise (though I can't think of any off the top of my head). A non-parametric relational type system – which doesn't permit field values to themselves be relations, such as in SQL – has obvious difficulties specifying recurrent structures. (You can of course flatten these using pointers, but without dependent constraints you can't catch bugs.)
    - tel 12y ago
      I think we're discussing slightly different things. I'd like to eventually get this line of reasoning closer to where you are, but right now my interest in describing ADTs has less to do with representation of useful things and more to do with "these types form a basis for thinking about computation". Effectively, products are the quintessential "grouping" notion, sums the quintessential "choice" notion, and implications the quintessential "hypothetical" notion. So those are pretty important for describing any computation. All that said, I really like relational types and wish they were more commonly used. I do think it takes some effort to model them in ADTs and that a system which provided them more directly would be fun.

felixgallo 12y ago

Coming from a formal symbolic logic background and 30 years of software development in typed and typeless imperative and functional languages, it's incredibly interesting, pleasurable, and more than a little frustrating to not understand this blog post in the slightest. Not only do the words not really make sense to me in the order they're presented; and not only do the assertions seem alien and foreign in nearly every respect; but I can't fathom a pragmatic path by which even if I accepted everything here as given, it would give me an intuition I could use to do anything different or better than I do now. And that's neat, because there's apparently (given the footnotes) a bunch of people for whom that is not true, so I have to be missing something somewhere, and that's a learning opportunity. And certainly I've enjoyed your other blog posts, tel, for their clarity and brevity and informational content. Nevertheless this is problematic, because I'm probably your target audience, and I couldn't be any more baffled or concerned by the idea that you'd be blithely mapping "+" (sum, addition) to "\/" (logical-or, disjunction) across fields and asserting conceptual equivalence like it's a given, much less a foundational building block of an argument. Now off to bounce harmlessly off that blog post a few more times.