Saturday, October 2, 2010

Types are sets and sets are types

The essential property of a type is whether a value belongs to it. So too with sets. So let a ∈ S be the same as a instanceof S.
Subtypes are subsets.
Function types are special subsets of set tuples.
(Disjoint) set union is the sum type
The Cartesian product of two sets is the product type of the two types.
Set equality is type equality
The power set is the type of subtypes.
The universe set is the set of all bit patterns.
Set intersection is interesting and does not appear in any language I know of, other than subtyping.

I am not certain what the axiom of choice says when applied to types; it is probably rather profound.

No comments:

Post a Comment