Department of Computer Science and Technology

Technical reports

Programming languages and dimensions

Andrew John Kennedy

April 1996, 149 pages

This technical report is based on a dissertation submitted November 1995 by the author for the degree of Doctor of Philosophy to the University of Cambridge, St Catherine’s College.

DOI: 10.48456/tr-391

Abstract

Scientists and engineers must ensure that the equations and formulae which they use are dimensionally consistent, but existing programming languages treat all numeric values as dimensionless. This thesis investigates the extension of programming languages to support the notion of physical dimension.

A type system is presented similar to that of the programming language ML but extended with polymorphic dimension types. An algorithm which infers most general dimension types automatically is then described and proved correct.

The semantics of the language is given by a translation into an explicitlytyped language in which dimensions are passed as arguments to functions. The operational semantics of this language is specified in the usual way by an evaluation relation defined by a set of rules. This is used to show that if a program is well-typed then no dimension errors can occur during its evaluation.

More abstract properties of the language are investigated using a denotational semantics: these include a notion of invariance under changes in the units of measure used, analogous to parametricity in the polymorphic lambda calculus. Finally the dissertation is summarised and many possible directions for future research in dimension types and related type systems are described.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-391,
  author =	 {Kennedy, Andrew John},
  title = 	 {{Programming languages and dimensions}},
  year = 	 1996,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-391},
  number = 	 {UCAM-CL-TR-391}
}