Topic: type algebras, typed lambda calculus, and type-complete languages

topics > computer science > data > Group: data type

derived data types
procedure and type-valued variables

formal methods and languages
function signature
function syntax definition
functional programming
lambda calculus
lattice theory of types
type retract


A type system assigns a type to every expression of a language. It does this by building up types from the expression's constituents. For example, the type of a function call is a cross-product of the types of its arguments yielding its result type. Many of these intermediate types will not have a name.

ML derives its type automatically. Type expressions are built with cross-product and function.

If the type of an expression is independent of its context, then any free variable can be parameterized. The typed lambda calculus is an example of a type-complete language. (cbb 1/90)

Subtopic: data type as meaning up

Quote: to understand an expression must know the data type of each variable in the expression [»browRE7_1976]
Quote: a type system is a set of rules for associating a type with every meaningful subexpression [»wegnP10_1986]
Quote: type-checking sees types as syntactic constraints that guarantees compatibility of composite expressions

Subtopic: safe type system up

Quote: Capability Language (CL) propagates capabilities for region-based memory operations; provably safe type system; lexical scope not required; e.g., extensible systems and continuation-passing style [»walkD7_2000]
Quote: Capability Language (CL), provably safe intermediate language for region-based memory management; supports aliasing and extensible OS; best for continuation-passing languages [»walkD7_2000]
Quote: associate capability and type with each object; guarantees exclusive ownership for deallocation or reuse; extends linear type systems [»walkD7_2000]

Subtopic: type schema up

Quote: datatypes in ML by type constructors which represent the type and construct new instances of the type [»readC_1989]
Quote: every type in ML, including list constructors, can be defined in terms of tuple and function types; predefined types for efficiency [»readC_1989]
Quote: formalization of XML Schema using tree grammars; named types and structural types; matching and validation [»simeJ1_2003]
Quote: formalization of XML Schema used for XQuery and XPath specifications; one of the first
Quote: validation theorem -- validates iff matches and erases; roundtripping if unambiguous [»simeJ1_2003]
Quote: Kleisli and its self-describing data exchange use parametric polymorphism and type inference; from functional programming [»wongL9_2000]
Quote: define object types by arbitrarily nested records (f:t), sets {t}, bags {|t|}, lists [t], and variants ; natural mappings for bioinformatics databases [»wongL9_2000]
Quote: Kleisli uses the nested relational calculus (NRC); lambda calculus plus records, and sets [»wongL9_2000]

Subtopic: function type up

Quote: a function type is a cross product of its argument types to its result type [»kiebRB9_1973, OK]
Quote: many types do not have explicit names; e.g., operator or function types [»kiebRB9_1973]

Subtopic: type algebra up

Quote: a type algebra is intrinsically first-order; needs homeomorphisms from functions to relations [»reynJC9_1983]
Quote: in modern type theory, types are values in a suitable semantic domain; type constructors are maps from this domain into itself [»nelsG_1991]
Quote: in the theory of dependent types, Modula-3's generic interface is a function from module-values to module-types and a generic module is a function from module-values to module-values [»nelsG_1991]
Quote: an algebraic specification of an abstract type consists of its syntax (names, domains, ranges) and the relations of its operations [»guttJV6_1977]

Subtopic: type-complete up

Quote: type completeness--all data types enjoy equal status; e.g., Pascal functions cannot return arrays or functions [»atkiMP6_1987]
Quote: in a type-complete language, type of a name or expression can not depend on context
Quote: in a type-complete language, any expression can be parameterized with respect to any free name
Quote: type-complete language if type for every name, every expression or composite, independent of context, allowable types exist, parameterized expressions [»demeA_1980]
Quote: simplest type-complete language is the typed lambda calculus [»demeA_1980]
Quote: in a type-complete language, parameterization and application are universally applicable [»demeA_1980]
Quote: with type-completeness, any name that can be declared can also be a parameter [»demeA_1980]

Subtopic: examples up

QuoteRef: demeAJ_1980 ;; presentation of data types in Russell

Related Topics up

Group: derived data types   (9 topics, 119 quotes)
Group: procedure and type-valued variables   (4 topics, 95 quotes)

Topic: formal methods and languages (53 items)
Topic: function signature (21 items)
Topic: function syntax definition (17 items)
Topic: functional programming (45 items)
Topic: lambda calculus (16 items)
Topic: lattice theory of types (15 items)
Topic: type retract
(12 items)

Updated barberCB 3/06
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.