Andreas Weber
ABSTRACT
This paper presents algorithms that perform a type inference for a type system occurring in the context of computer algebra. The type system permits various classes of coercions between types and the algorithms are complete for the precisely defined system, which can be seen as a formal description of an important subset of the type system supported by the computer algebra program AXIOM.
Previously only algorithms for much more restricted cases of coercions have been described or the frameworks used have been so general that the corresponding type inference problems were known to be undecidable.
- 1.CARDELLI, L. A semantics of multiple inheritance. Information and Computation 76 (1988), 138-164. Google Scholar
Digital Library
- 2.COMON, H., LUGIEZ, D., AND SCHNOEBELEN, P. A rewritebased type discipline for a subset of computer algebra. Journal of Symbolic Computation 11 (1991), 349-368. Google ScholarDigital Library
- 3.DALMAS, S. A polymorphic functional language applied to symbolic computation. In Proc. Symposium on Symbolic and Algebraic Computation (ISSA C '92) (Berkeley, CA, July 1992), P. S. Wang, Ed., Association for Computing Machinery, pp. 369-375. Google ScholarDigital Library
- 4.FORTENBACHER, A. Efficient type inference and coercion in computer algebra. In Design and Implementation of Symbolic Computation Systems (DISCO '90) (Capri, Italy, Apr. 1990), A. Miola, Ed., vol. 429 of Lecture Notes in Computer Science, Springer-Verlag, pp. 56-60. rage Google ScholarCross Ref
- 5.FUH, Y.-C., AND MISHRA, P. Type inference with subtypes. Theoretical Computer Science 73 (1990), 155-175. Google ScholarDigital Library
- 6.HEARN, A. C., AND SCHR(3FER, E. An order-sorted approach to algebraic computation. In Miola { 12}, pp. 134--144. Google Scholar
- 7.JENKS, R. D., AND SUTOR, R. S. AXIOM: The Scientific Computation System. Springer-Verlag, New York, 1992. Google ScholarDigital Library
- 8.KAES, S. Type inference in the presence of overloading, subtyping, and recursive types. In Proceedings of the 1992 A CM Conference on Lisp and Functional Programming (San Francisco, CA, June 1992), Association for Computing Machinery, pp. 193-205. Google ScholarDigital Library
- 9.LANG, S. Algebra. Addison-Wesley, Reading, MA, 1971.Google Scholar
- 10.LINCOLN, P., AND MITCHEL, J. C. Algorithmic aspects of type inference with subtypes, in Conference Record of the Nineteenth Annual A CM Symposium on Principles of Programming Languages (Albuquerque, New Mexico, Jan. 1992), Association for Computing Machinery, pp. 293-304. Google ScholarDigital Library
- 11.MARZINKEWITSCH, R. Operating computer algebra systems by handprinted input. In Proc. Symposium on Symbolic and Algebraic Computation (ISSAC '91) (Bonn, Germany, July 1991), S. M. Watt, Ed., Association for Computing Machinery, pp. 411--413. Google ScholarDigital Library
- 12.MIOLA, A., Ed. Design and implementation of Symbolic Computation Systems ~ International Symposium DISCO '93 (Gmunden, Austria, Sept. 1993), vol. 722 of Lecture Notes in Computer Science, Springer-Verlag. Google ScholarDigital Library
- 13.MISSURA, S. A. Extending AlgBench with a type system. In Google ScholarDigital Library
- 14.MITCHELL, J. C. Type inference with simple subtypes. Journal of Functional Programming 1, 3 (July 1991), 245-285.Google ScholarCross Ref
- 15.MONAGAN, M. B. Gauss: a parameterized domain of computation system with support for signature functions. In Miola {12}, pp. 81-94. Google Scholar
- 16.RECTOR, D. L. Semantics in algebraic computation. In Computers and Mathematics (Massachusetts Institute of Technology, June 1989), E. Kaltofen and S. M. Watt, Eds., Springer- Verlag, pp. 299-307. Google ScholarDigital Library
- 17.ShNTAS, P. S. A type system for computer algebra. In Miola {12}, pp. 177-191. Google Scholar
- 18.SCHONERT, M., BESCHE, H. U., BREUER, T., CELLER, F., MNICH, J., PFEIFFER, G., POLLS, U., AND NIEMEYER, A. GAP- Groups Algorithm, and Programming. Lehrstuhl D ftir Mathematik, RWTH Aachen, Apr. 1992. Available via anonymous ftp at samson.math, rwth-aachen, de in pub/gap.Google Scholar
- 19.SMOLKA, G., Ntn'r, W., GOGUEN, J. A., AND MESEGUER, J. Order-sorted equational computation. In Resolution of Equations in Algebraic Structures, Volume 2, H. Ait-Kaci and M. Nivat, Eds. Academic Press, 1989, chapter 10, pp. 297- 367.Google Scholar
- 20.SUTOR, R. S., AND JENKS, R. D. The type inference and coercion facilities in the Scratchpad Ii interpreter. ACM SIGPLAN Notices 22, 7 (1987), 56-63. SIGPLAN '87 Symposium on Interpreters and interpretive Techniques. Google ScholarDigital Library
- 21.WEBER, A. A type-coercion problem in computer algebra. In Artifical Intelligence and Symbolic Mathematical Computation -- International Conference AISMC-1 (Karlsruhe, Germany, Aug. 1992), J. Calmet and J. A. Campbell, Eds., vol. 737 of Lecture Notes in Computer Science, Springer- Verlag, pp. 188-194. Google Scholar
- 22.WEBER, A. On coherence in computer algebra. In Miola { 12}, pp. 95-106. Google Scholar
- 23.WEBER, A. Type Systems for Computer Algebra. Dissertation, Fakult~it ftlr Informatik, Universit~it Ttibingen, July 1993.Google Scholar
- 24.ZIPPEL, R. The Weyl computer algebra substrate. In Miola {12}, pp. 303-318. Google Scholar
Index Terms
- Algorithms for type inference with coercions
Recommendations
Coercions in a polymorphic type system
We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument ...
Polymorphic type inference
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesThe benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central ...
Comments