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.

Replying to

and

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.

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

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?

gwillen

@gwillen

Nov 16, 2021

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.

Show replies