3 ms·

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

by 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.

by tel 12y ago

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.