Conversation

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.

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.

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

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.

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.

gwillen

@gwillen

Yeah that all seems very true. (I hear that if you want to really split hairs about sameness, Homotopy Type Theory might be for you.)