Topic: data type as a set of values
Topic: lattice theory of types
Topic: type algebras, typed lambda calculus, and typecomplete languages
Topic: universal data type
 
Summary
For data types on a universal type domain, Scott defines retracts which are continuous functions whose ranges are fixed points. For instance the 32bit type retract on bit strings, maps all bit strings into 32bit values while 32bit values (the retract's range) are mapped into the themselves. The range is the type's value space; it is shared by other retracts with different mappings from the universal value space. A value space with retracts is at once typeless yet rich in data types. The retracts are also members of Scott's universal domain which contains both functions and values.
In reduction languages the semantic function on expressions forms a retract; the corresponding type is the set of 'values' for the language. In programming languages, value access composed with assignment is a type retract. (cbb 5/80)
Subtopic: complete language
Quote: complete language <=> fixed points of a semantic function are the values of its expressions [»backJ_1973, OK]
 Subtopic: universal domain
Quote: Scott's universal domain is both typeless and contains an infinite hierarchy of types [»demeA_1978]
 Quote: type retracts are themselves values of the universal domain [»demeA_1978]
 Subtopic: type retract
Quote: a type retract f is the identity on its range (its set of values over the universal domain) [»demeA_1978]
 Quote: a type retract is a continuous function which is the identity over its range (a proper subspace of D)
 Quote: a type retract is a function which is the identity on its range
 Quote: the identity function on functions is a retract for all functions [»scotD9_1976]
 Subtopic: meaning of type retract
Quote: a data type of the universal domain is the type retract for a proper subdomain of the universal domain
 Quote: a type retract defines the interpretation (value) of each element in the universal domain [»demeA_1978]
 Quote: in Russell, the meaning of a data type is the meaning of its operations over the universal domain of bit strings [»demeA_1978]
 Quote: composing functions for assign and access yields a type retract whose range is all legal values for that type [»demeA_1978]
 Quote: can convert a type retract for a set of operations into one for a set of values; e.g., integers as 32bit values [»demeA_1978]

Related Topics
Topic: data type as a set of values (20 items)
Topic: lattice theory of types (15 items)
Topic: type algebras, typed lambda calculus, and typecomplete languages (28 items)
Topic: universal data type (18 items)
