This paper extends a strongly-typed programming language with a notion of dimension type. Our approach improves on previous proposals in that dimension types may be polymorphic. Furthermore, any expression which is typable in the system has a most general type, and we describe an algorithm which infers this type automatically. The algorithm exploits equational unification over Abelian groups in addition to ordinary term unification.

PostScript file

In  ESOP '94: Proceedings of the 5th European Symposium on Programming

Publisher  Springer-Verlag

Details