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
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
