[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Reading ACM SigPlan Notices in the 80s, the papers on adding
Units-of-Measure to programming
languages for type-checking seemed sensible - especially after reading
Comp.risks in
Software Engineering Notes.
More recently I read George Hart's 1995 book "Multidimensional Analysis:
..." which provided
the abstract algebra behind my vague intuitive understanding of
Dimensional correctness,
sketched an implementation and described the suprising (to me) result
that some problems in
science and engineering need matrices that aren't simply dimensionally
uniform.
Using google scholar for literature searches on the subject, led to
Kennedy's 1996 Thesis
which describes adding Units of Measure to Standard ML. His later work
adds this in F#.
His thesis doesn't reference Hart though.
Last year Griffioen's thesis extended Kennedy's Hindley–Milner type
system to support
Hart's matrices.
I hope drawing attention to this may help bring Unit-of-Measure type
checking to languages
commonly used.
en.wikipedia.org/wiki/User:RDBrown/Prog_Lang_Dimensions (has the links)
Kennedy, Andrew J. (April 1996). Programming languages and
dimensions (Phd). 391. University of Cambridge. ISSN 1476-2986.
UCAM-CL-TR-391.
Kennedy, A. (2010). "Types for Units-of-Measure: Theory and
Practice". In Horváth, Z.; Plasmeijer, R.; Zsók, V. (eds.). Central
European Functional Programming School. CEFP 2009. Lecture Notes in
Computer Science. 6299. Springer. doi:10.1007/978-3-642-17685-2_8. ISBN
978-3-642-17684-5. F# implementation usage tutorial
Hart, G. (1994). "The Theory of Dimensioned Matrices". In Lewis,
John G. (ed.). Proceedings of Fifth SIAM Conference on Applied Linear
Algebra, Snowbird, Utah, June 1994. Society for Industrial and Applied
Mathematics. pp. 186–190. ISBN 9780898713367.
Hart, George W. "Multidimensional Analysis". — links to the above
paper and the book of the same name, showing examples of the
multidimensional linear algebra theorems.
Hart, George W. (1995), Multidimensional Analysis: Algebras and
Systems for Science and Engineering, Springer-Verlag, ISBN 978-0-387-94417-3
ISBN 9781461286974 reprint at Springer
Griffioen, P. R. (September 2015). "Type inference for array
programming with dimensioned vector spaces". IFL '15: Proceedings of the
27th Symposium on the Implementation and Application of Functional
Programming Languages. pp. 1–12. doi:10.1145/2897336.2897341. ISBN
978-1-4503-4273-5. "... We extend arrays with units of measurement, and
Hindley-Milner typing with a matrix type based on the algebraic
structure of units of measurement in matrices that allows type inference
up to dimensioned vector spaces. The inference is sound and complete and
gives the most general type of any linear algebra expression.
Experiments show that the explicit support for linear algebra increases
type safety, and that it leads to a more functional and index-free style
of programming. It refines the types for linear algebra operators
significantly, while the use of arrays as general containers has to be
replaced by other data structures. As validation the matrix type system
is implemented in the functional matrix language Pacioli."
Griffioen, P. (2019). A unit-aware matrix language and its
application in control and auditing (PDF) (Thesis). University of
Amsterdam. hdl:11245.1/fd7be191-700f-4468-a329-4c8ecd9007ba.
github.com/pgriffel/pacioli
