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. Manyof these topics, such as coercions, are relevant. The thesis abstract reads: 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 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 |
Free forum by Nabble | Edit this page |