Conversation

Patrick Walton
@pcwalton
Reminder: the way to remember the difference between sum and product types is to count the number of possible values. enum { A(int), B(int) } is a sum type because there are INT_MAX+INT_MAX possible values. (int, int) is a product type because there are INT_MAX*INT_MAX values.
6
116
Paul Bone
@Paul_Bone
Initially I was confused when I read TAPL and saw that it went to set theory almost right away. Then I started thinking about types as describing the "set of values a variable may take". And now this, and sum/product types makes sense.
1
8
Brendan Zabarauskas
@brendanzab
I think so long as you keep it as a loose analogy it's fine, but there's a bit of subtlety when it comes to comparing types to sets. IIRC, TAPL goes into set theory as a basis for some of the proofs, but it's not required as part of foundation used to define type systems.
1
3
Brendan Zabarauskas
@brendanzab
I get a bit confused with the distinctions though, to be honest. I've seen people say that set membership is a semantic property, where as type membership is syntactic, but I'm not sure I'm convinced?
3
1
Jon Purdy
@evincarofautumn
Sets: • Use a logic + axioms (e.g. ZFC) • Membership: described as proposition x∈S • Equality: extensional Types: • Write a logic—no axioms, only rules • Membership: defined as judgement x:T • Equality: defined, intensionally or on extension of type to set of values
3
1
Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
@evincarofautumn
and 2 others
Might help me understand this more: twitter.com/evincarofautum Is the idea that unlike saying “types _are_ a set of values”, we are instead saying “types can be _modeled_ as sets of values”? And in some (extensional) type systems we use this as a way of defining equality?
Quote Tweet
Jon Purdy
@evincarofautumn
·
Replying to @evincarofautumn
So the number of types in a sum type |A + B| is more precisely the cardinality of the disjoint union of their extensions |εA + εB|, which is the union of those sets paired with tags |{1} × εA ∪ {2} × εB|; for finite types this just works out to the sum of the sizes |εA| + |εB|.
Twitter Web App