[TYPES] "Type systems for programs respecting dimensions" Re: Types for Units-of-Measure

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

For people who are interested :-

McBride, Conor; Nordvall-Forsberg, Fredrik (2022). "Type systems for 
programs respecting dimensions" (PDF). Advanced Mathematical and 
Computational Tools in Metrology and Testing XII. Advances in 
Mathematics for Applied Sciences. World Scientific. pp. 331–345. 
doi:10.1142/9789811242380_0020. ISBN 9789811242380.

https://urldefense.com/v3/__https://pureportal.strath.ac.uk/files/121022760/McBride_etal_amctmtxii2021_type_systems_for_programs_respecting_dimensions.pdf__;!!IBzWLUs!UX9RGwE5FC7pDxN47lDwNSXSAGRQyL5BgEzF1Jh82ctFk29TRks-axesIRwfnSzjWQsnkE7KCbhahp8xI9WTIixy-7kG5YI$ 

 From the Conclusion:

Following Hart, we have shown how to use dependent types to extend type
systems for units of measure from scalars to matrices. ...

On 9/11/20 22:42, Rodney Brown wrote:
> 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.