LIPIcs.TLCA.2015.45.pdf
- Filesize: 446 kB
- 15 pages
Document
Models for Polymorphism over Physical Dimension
Authors
-
Part of:
Volume:
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Typed Lambda Calculi and Applications (TLCA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-06-15
Cite As Get BibTex
Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, and Sam Staton. Models for Polymorphism over Physical Dimension. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 45-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TLCA.2015.45
Abstract
We provide a categorical framework for models of a type theory that has special types for physical quantities. The types are indexed by the physical dimensions that they involve. Fibrations are used to organize this index structure in the models of the type theory. We develop some informative models of this type theory: firstly, a model based on group actions, which captures invariance under scaling, and secondly, a way of constructing new models using relational parametricity.
Subject Classification
Keywords
- Category Theory
- Units of Measure
- Dimension Types
- Type Theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Robert Atkey. From parametricity to conservation laws, via Noether’s theorem. In Proc. POPL 2014, pages 491-502, 2014.
-
Lars Birkedal and Rasmus E Møgelberg. Categorical models for Abadi and Plotkin’s logic for parametricity. Mathematical Structures in Computer Science, 15(04):709-772, 2005.
-
Ronald Brown and Christopher B Spencer. G-groupoids, crossed modules and the fundamental groupoid of a topological group. Proc. Indag. Math., 79(4):296-302, 1976.
-
Edgar Buckingham. On physically similar systems; illustrations of the use of dimensional equations. Physical Review, 4(4):345-376, 1914.
-
P-L Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. Theoret. Comput. Sci., 546:99-119, 2014.
-
Martin Erwig and Margaret Burnett. Adding apples and oranges. In Practical Aspects of Declarative Languages, pages 173-191. Springer, 2002.
-
Claudio Hermida. Some properties of Fib as a fibred 2-category. Journal of Pure and Applied Algebra, 134(1):83-109, 1999.
-
Ronald T. House. A proposal for an extended form of type checking of expressions. The Computer Journal, 26(4):366-374, 1983.
-
Bart Jacobs. Categorical logic and type theory, volume 141. Elsevier, 1999.
-
Andrew J. Kennedy. Relational parametricity and units of measure. In POPL'97, 1997.
-
F. William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281-296, 1969.
-
R Männer. Strong typing and physical units. ACM Sigplan Notices, 21(3):11-20, 1986.
-
Mars Climate Orbiter Mishap Investigation Board. Phase I report. NASA, 1999.
-
Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Proc. POPL 2015, pages 3-16, 2015.
-
John Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.
-
Ain A Sonin. The physical basis of dimensional analysis. Department of Mechanical Engineering, MIT, 2001.
-
Mitchell Wand and Patrick O'Keefe. Automatic dimensional inference. In Computational Logic - Essays in Honor of Alan Robinson, pages 479-483, 1991.