[Axiom-developer] Type Theory and Axiom

[Tim Daly]

Weber's Thesis
http://cg.cs.uni-bonn.de/personal-pages/weber/publications/pdf/WeberA/Weber93b.pdf

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