Semantic Subtyping

The distinguishing feature of a type system using SemanticSubtyping is that it has a set-theoretic model, in which types correspond directly to sets of values.

Start with: Guiseppe Castagna and Alain Frisch, "A Gentle Introduction to Semantic Subtyping", Second workshop on Programmable Structured Documents (Hakone).

From the introduction to that paper:

Many recent type systems rely on a subtyping relation. Its definition generally depends on the type algebra, and on its intended use. We can distinguish two main approaches for defining subtyping: the syntactic approach and the semantic one. The syntactic approach -- by far the most widespread -- consists in defining the subtyping relation by axiomatising it in a formal system (a set of inductive or coinductive rules); in the semantic approach [...], instead, one starts with a model of the language and an interpretation of types as subsets of the model, then defines the subtyping relation as the inclusion of denoted sets, and, finally, when the relation is decidable, derives a subtyping algorithm from the semantic definition.

[In short, "syntactic" type systems are those in which types are "constructed" out of more primitive types using various type operations (Cartesian product, union, join, meet, etc.). Which is how all class-based and prototype-based languages work.]

Semantic subtyping is most useful for expressing types of tree-structured data, such as XML, EssExpressions and TermTrees?.

SemanticSubtyping is powerful; on the other hand it has some interesting issues. (Not insurmountable, but interesting nonetheless):

One possibility is to use HyperSetTheory?. This theory (original ZF + Anti-Foundation Axiom) allows a hyperset to include itself as a member. In particular, there can be a "Hyperset" or "Type" type that includes itself, and a UniversalSet type that includes everything [this is wrong, see below]. A system of hypersets can be visualised as a directed graph that specifies the membership relation.

My mistake, HyperSetTheory? does not allow a UniversalSet type, because it would lead to a contradiction via Cantor's Theorem. To have a UniversalSet type, you would need to use a set theory with a restricted version of the axiom of separation (so that Cantor's Theorem does not hold), such as NewFoundations or NFU. See SetOfAllSets.

In CeDuce, "arrow" (function) types are treated as sets of sets of pairs, and have contravariant argument and covariant result types. CeDuce is not object-oriented, but since ClosuresAndObjectsAreEquivalent (yes really, despite the skepticism on that page), this induces the correct subtyping relations for object types. For example extending an object type with additional methods automatically results in a subtype, because this is equivalent to changing the closure argument type contravariantly. (See, contravariance is useful.)

Many of the above issues can cause syntactic typing to creep into the semantic model.

See also CeDuce, CeeOmega.


View edit of January 8, 2005 or FindPage with title or text search