On coherence in computer algebra
Modern computer algebra systems (e. g. AXIOM) support a rich type system including parameterized data types and the possibility of implicit coercions between types. In such a type system it will be frequently the case that there are different ways of building coercions between types. An important requirement is that all coercions between two types coincide, a property which is called coherence.
We will prove a coherence theorem for a formal type system having several possibilities of coercions covering many important examples. Moreover, we will give some informal reasoning why the formally defined restrictions can be satisfied by an actual system.
KeywordsType System Computer Algebra Category Theory Computer Algebra System Type Inference
Unable to display preview. Download preview PDF.
- 1.Association for Computing Machinery. Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Francisco, CA, June 1992.Google Scholar
- 2.H. P. Barendregt. The Lambda Calculus — Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, second edition, 1984.Google Scholar
- 4.R. Bündgen. Reduce the redex → ReDuX. In C. Kirchner, editor, Fifth International Conference on Rewriting Techniques and Applications (RTA '93), Lecture Notes in Computer Science, Montréal, Canada, June 1993. Springer-Verlag. To appear.Google Scholar
- 6.K. Chen, P. Hudak, and M. Odersky. Parametric type classes. In LFP '92 , pages 170–181.Google Scholar
- 7.H. Comon, D. Lugiez, and P. Schnoebelen. A rewrite-based type discipline for a subset of computer algebra. Journal of Symbolic Computation, 11:349–368, 1991.Google Scholar
- 8.A. Fortenbacher. Efficient type inference and coercion in computer algebra. In A. Miola, editor, Design and Implementation of Symbolic Computation Systems (DISCO '90), volume 429 of Lecture Notes in Computer Science, pages 56–60, Capri, Italy, Apr. 1990. Springer-Verlag.Google Scholar
- 11.P. Hudak, S. Peyton Jones, P. Wadler, et al. Report on the programming language Haskell — a non-strict, purely functional language, version 1.2. ACM SIGPLAN Notices, 27(5), May 1992.Google Scholar
- 12.R. D. Jenks and R. S. Sutor. AXIOM: The Scientific Computation System. Springer-Verlag, New York, 1992.Google Scholar
- 13.S. Kaes. Type inference in the presence of overloading, subtyping, and recursive types. In LFP '92 , pages 193–205.Google Scholar
- 14.S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971.Google Scholar
- 15.J. C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245–285, July 1991.Google Scholar
- 16.D. L. Rector. Semantics in algebraic computation. In E. Kaltofen and S. M. Watt, editors, Computers and Mathematics, pages 299–307, Massachusetts Institute of Technology, June 1989. Springer-Verlag.Google Scholar
- 17.J. C. Reynolds. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Semantics-Directed Compiler Generation, Workshop, volume 94 of Lecture Notes in Computer Science, pages 211–258, Aarhus, Denmark, Jan. 1980. Springer-Verlag.Google Scholar
- 18.J. C. Reynolds. The coherence of languages with intersection types. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software — International Conference TACS '91, volume 526 of Lecture Notes in Computer Science, pages 675–700, Sendai, Japan, Sept. 1991. Springer-Verlag.Google Scholar
- 19.G. Smolka, W. Nutt, J. A. Goguen, and J. Meseguer. Order-sorted equational computation. In H. AÏt-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, chapter 10, pages 297–367. Academic Press, 1989.Google Scholar