Conversation

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.

116

Paul Bone

@Paul_Bone

Nov 16, 2021

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.

Brendan Zabarauskas

@brendanzab

Nov 16, 2021

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.

Replying to

and

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?

4:34 AM · Nov 16, 2021Twitter Web App

Replying to

and

I feel like I have a decent grasp of type theory, but tbh I still find this specific issue kind of finicky. I often find that type theorists can be insistent that certain interpretations of things are Definitely Wrong, even though they appear isomorphic to the ones they prefer.

Brendan Zabarauskas

@brendanzab

Nov 16, 2021

I think it depends on the type theorist you talk to. Some are pretty plural about these things. But yeah, type theorists care a lot about notions of 'sameness' (it's a big part of the field), so it is something that they are probably more likely to want to be precise about.

Show replies

Replying to

and

I see it as the distinction between platonically assuming all objects exists, as is often the case with set theory, and having a criteria for recognizing an object as a "something", which I think is what type theory does.

Replying to

and

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

Jon Purdy

@evincarofautumn

Nov 16, 2021

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