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.

http://www.cduce.org/papers.html

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):

Which SetTheory? There are quite a few to choose from.
RusselsParadox? issues. Are the set of "types" themselves objects which may or may not be in the set encoding types; and if so, do paradoxes arise as a result?

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.

How are objects (in particular, primitive types) included in the type system? Do we assume that any possible object springs forth from the ether, and completely ignore/abstract away the details of construction? Or do we let construction details creep in?
Associating behavior with types/objects. In the purely semantic view, a type is a subset of some universal type (containing everything). Most programming languages find it useful, however, to associate behavior (methods/messages/etc.) with types or individual objects; how is this accomplished within the semantic framework?

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.)

Decideability. The text above includes the disclaimer "when the relationship is decideable"; frequently it isn't. (Determiniation of whether or not two arbitrary, infinite sets have a subtype of relationship is generally NOT decideable).

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