Type Inference For Linear Algebra With Units Of Measurement

P. R. Griffioen 1
1 ATEAMS - Analysis and Transformation based on rEliAble tool coMpositionS
Inria Lille - Nord Europe, CWI - Centrum Wiskunde & Informatica
Abstract : Refining types of numerical data with units of measurement has the potential to increase safety of programming languages but is restricted to homogeneous units when checked statically with parametric polymorphism. We lift units to vectors and show how type inference of linear algebra expressions can statically determine safety for data with heterogeneous units. The typing is based on the dyadic product of units that is found in linear transformations and the corresponding vector spaces. Since it is a refinement of Kennedy's types for units we automatically obtain a unification algorithm, which gives principal types for linear algebra. The extension of unit-unification to numerical data with heterogeneous units makes the safety of statically checked numerical expressions available to a significantly larger set of use-cases.
Type de document :
[Technical Report] SwAT-1302, 2013, pp.1 - 32
Liste complète des métadonnées

Contributeur : Tijs Van Der Storm <>
Soumis le : jeudi 2 janvier 2014 - 17:05:34
Dernière modification le : samedi 17 septembre 2016 - 01:35:06


  • HAL Id : hal-00923380, version 1



P. R. Griffioen. Type Inference For Linear Algebra With Units Of Measurement. [Technical Report] SwAT-1302, 2013, pp.1 - 32. 〈hal-00923380〉



Consultations de la notice