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
Jon Purdy
@evincarofautumn
The collection of values that inhabit a type or a set is called its “extension”—in the sense of “extent”, not “to extend”. Equality of sets is defined by equality of those collections—∀x(x ∈ A ↔ x ∈ B) ↔ A = B—while equality of types is whatever the type system’s rules say.
1
2
Jon Purdy
@evincarofautumn
Replying to
@brendanzab
It holds regardless, but in practice TT papers tend to leave the assumption of intensionality unstated because it’s so common. Extensionality, or weaker stuff with the same flavour like structural typing, shows up in rules for stuff like unification (e.g. of rows) and subtyping.
1