| 
|
Topic: type retract
topics >
computer science >
data >
data type as a set of values
Topic:
lattice theory of types
Topic:
type algebras, typed lambda calculus, and type-complete 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 32-bit type retract on bit strings, maps all bit strings into 32-bit values while 32-bit 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: universal domain
Quote: complete language <=> fixed points of a semantic function are the values of its expressions [»backJ_1973, OK]
Subtopic: type retract
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: meaning of 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]
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 32-bit values
[»demeA_1978]
Topic: data type as a set of values (20 items)
Topic: lattice theory of types (15 items)
Topic: type algebras, typed lambda calculus, and type-complete languages (28 items)
Topic: universal data type
(18 items)