[TYPES] Types for Units-of-Measure

[Rodney Brown]

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