Domain specific extensions and their framework
This topic is about extensions of Type Theory by a language modelled
by the structure central to a specific application domain. The
language provides a higher level of abstractions for reasoning with
the type theoretic representation of the structure, encapsulating
``implementation details'' of the representation. We aim to have a unified
framework for such an extension: an inherent, hierarchical description
of the target structures independent of their possible
representations, a method to derive a language for a given structure, and
semantics that guarantees correct interaction between extensions and
base systems. The framework is to lead to systematic machine
implementations of extensions and further to a single, extensible
system.
For example, Szasz's theory of specifications can be
seen as such an extension for the structure of specifications
represented by (data type, predicate) pairs. Each natural step of
inference in her theory (e.g., formation of higher-order
specification) corresponds to several steps of inference on the
pair-representations in the base Type Theory; so, the pairs models the
theory. Note that representing the pairs by dependent sums and then
manipulating them as plain types (e.g., applying function type
formation) cannot give desired results.
Similar developments can be expected for
setoids , setoids with algebraic
structure , domains ,
categories , etc.; study of various
calculus encodings of objects ,
processes , etc., should
also benefit from mixing machine-assisted reasoning at their original
calculi level. Development of their theories will enjoy the usual
advantages of modular programming; e.g., we can start experimenting
with the use of new abstraction, even if its representation is not in
place yet; we can change representation to support more abstractions
without affecting a prior development.
For the framework, we will unify and extend the correspondences
between various categorical structures and their internal languages,
e.g., cartesian closed categories and simply typed
lambda-calculi . We continue development and
implementation of the framework for categories with extra structure
based on universal properties . Compared to the more
established one for categories with (essentially) algebraic
structure , it gives rise to internal languages
suited for more logical, rather than equational, reasoning with the
familiar pattern of introduction and elimination rules. Further
theoretical issues are: adaptation of sketches
(e.g. ) for description of specific instances;
generalisation to fibred categories for a clear semantics of
interactions between the base and extensions; and iterations and other
ways to combine extensions for a hierarchical, modular development of
abstractions. The framework itself, which talks about Type Theory
extensions, will be studied in the ordinary mathematical context, but
constructive aspects in each instance, e.g. issues of equality, will
be a part of investigation.
Last modified: Wed May 27 13:49:13 MET DST 1998