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?

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

Ah yeah, I think that makes sense! Could you elaborate a bit on what you mean by ‘extension of type’ here?

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.