Type Theory and Axiom

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

Type Theory and Axiom

Tim Daly
is an excellent "cross-over" document between type theory and Axiom. In particular,
he talks about type classes, which we have been discussing, in Axiom terms. Many
of these topics, such as coercions, are relevant.

The thesis abstract reads:

We study type systems for computer algebra systems, which frequently correspond
to the "pragmatically developed" typing constructions used in Axiom.

A central concept is that of type classes which correspoind to Axiom categories. We
will show that types can be syntactically described as terms of a regular order-sorted
signature if no type parameters are allowed. Using results obtained for the functional
programming language Haskell we will show that the problem of type inference is
decidable. This result still holds if higher-order functions are present and parametric
polymorphism is used. These additional constructs are useful for further extensions
of existing computer algebra systems. These typing concepts can be used to implement
category theory and algebra.

On the one hand we will show that there are well known techniques to specify many
important type classes algebraically, and we will also show that a formal and
algorithmically Feasible treatment of the interactions of algebraically specified data
types and type classes is possible. On the other hand we will prove that there are
quite elementary examples arising in computer algebra which need very "strong"
formalisms to be specified and are thus hard to handle algorithmically.

We will show that it is necessary to distinguish between types and elements as
parameters of parametrized type classes. The type inference problem for the former
remains decidable whereas for the latter it becomes undecidable. We will also show
that such a distinction can be made quite naturally.

Type classes are second-order types. Although we will show that there are
constructions used in mathematics which imply that type classes have to become
first-order types in order to model the examples naturally, we will also argue that this
does not seem to be the case in areas currently accessible for an algebra system.
We will only sketch some systems that have been developed during the last years
in which the concept of type classes as first-order types can be expressed. For some
of these systems the type inference problem was proven to be undecidable.

Another fundamental concept for a type system of a computer algebra system --
at least for the purpose of a user interface -- are coercions. We will show that there
are cases which can be modeled by coercions but not by an "inheritance
mechanism", i.e. the concept of coercions is not only orthogonal to the one of
type classes but also to more general formalisms as are used in object-oriented
languages. We will define certain classes of coercions and impose conditions on
important classes of coercions which will imply that the meaning of an expression
is independent of the particular coercions that are used in order to type it.

We shall also impose some conditions on the interaction between polymorphic
operations defined in type classes and coercions that will yield a unique meaning
of an expression independent of the type which is assigned to it -- if coercions are
present there will very frequently be several possiblities to assign types to expressions.

Often it is not only possible to coerce one type into another but it will be the case
that two types are actually isomorphic. We will show that isomorphic types have
properties that cannot be deduced from the properties of coercions and will shortly
discuss other possibilities to model type isomorphisms. There are natural examples
of type isomorphisms occurring in the area of computer algebra that have a
"problematic" behavior. So we will prove for a certain example that the type
isomorphisms cannot be captured by a finite set of coercions by proving that
the naturally associated equational theory is not finitely axiomatizable.

Up to now few results are known that would give a clear dividing line between
classes of coercions which have a decidable type inference problem and
classes for which type inference becomes undecidable. We will give a type
inference algorithm for some important class of coercions.

Other typing constructs which are again quite orthogonal to the previous ones
are those of partial functions and of types depending on elements. We will link
the treatment of partial functions in Axiom to the one used in order-sorted algebras
and will show some problems which arise if a seemingly more expressive solution
were used. There are important cases in which types depending on elements arise
naturally. We will show that not only type inference but even type checking is
undecidable for relevant cases occurring in computer algebra.

Tim


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer