''Predicate types'' is a typing system where the "instance of" property of an object is defined by a ''predicate'' (a function returning true or false) rather than be details of the object's construction.  One way of implementing SetsAndPolymorphism.  

CecilLanguage has such a typing system; with the property that as an object's state changes, so can its type (the set of allowable predicates is not restricted to object invariants).

----------

''How does it deal with the "mutually-exclusive" issue? What keeps the answer to "what type am I" from being multiple? If it doesn't, then perhaps it's attributes and not types.''

PredicateTypes aren't mutually exclusive. There are many forms of types in the literature that aren't mutually exclusive (DependentTyping, PredicateTypes, static duck typing, higher level 'kinds' (as reflected in Haskell type-classes and C++ concepts), interfaces, effect typing, etc.). 

It seems that you're favoring some personal definitions for "attributes" and "types", and that in your mind "type" implies "mutually exclusive" whereas whatever you're calling "attributes" are not. That's a practitioner's view, I guess. Language designers have been working to integrate higher level and more flexible types into languages (and they've succeeded in a few languages - ScalaLanguage being an especially fine example of a new such "practitioner's language", using static duck typing for flexibility). However, several of the early designs for integrating types into programming were rather rigid and 'mutually exclusive'. 

But now you've been informed. Try in the future to not mistake the clumsy nature of the early implementations as defining 'types'. CeeIsNotThePinnacleOfProcedural, and mutual exclusion is not the pinnacle of typing. It'd be more productive for you to adopt the language people already use to describe types (such as PredicateTypes and DependentTyping) than for you to walk around trying to tell people that they really should be calling these things "attributes" based on your personal definition of the terms.

''Without a solid definition of "types", such is hard to avoid. And none of that subjective fuzzy "intention to classify" stuff, please.''

The only reason you find it "hard to avoid" your particular brand of sophistry is that you're taking an illogical and incorrect position to start with: you're insisting that "type" must be defined prior to definition of PredicateTypes. Perhaps you should learn about various forms of definitions (http://en.wikipedia.org/wiki/Ostensive_definition, http://en.wikipedia.org/wiki/Extensional_definition, http://en.wikipedia.org/wiki/Enumerative_definition, http://en.wikipedia.org/wiki/Intensional_definition). It seems what you're trying to say is that "if there is no intensional definition for type, then it's okay to say ridiculous things about PredicateTypes". But it's the other way around. "Type" is defined on a per-TypeSystem basis, and is on the broader scale of TypeTheory understood ostensively by examples such as PredicateTypes.

[''An interesting question is: does math have a type system that can be changed/swapped? Or are types in math not a type system, but just widely accepted types?'']
-----------

See also PredicateClasses, PredicateDispatching.