Document Open Access Logo

Models for Polymorphism over Physical Dimension

Authors Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.45.pdf
  • Filesize: 446 kB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Category Theory
  • Units of Measure
  • Dimension Types
  • Type Theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Robert Atkey
Neil Ghani
Fredrik Nordvall Forsberg
Timothy Revell
Sam Staton

References

  1. Robert Atkey. From parametricity to conservation laws, via Noether’s theorem. In Proc. POPL 2014, pages 491-502, 2014. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. Edgar Buckingham. On physically similar systems; illustrations of the use of dimensional equations. Physical Review, 4(4):345-376, 1914. Google Scholar
  5. P-L Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. Theoret. Comput. Sci., 546:99-119, 2014. Google Scholar
  6. Martin Erwig and Margaret Burnett. Adding apples and oranges. In Practical Aspects of Declarative Languages, pages 173-191. Springer, 2002. Google Scholar
  7. Claudio Hermida. Some properties of Fib as a fibred 2-category. Journal of Pure and Applied Algebra, 134(1):83-109, 1999. Google Scholar
  8. Ronald T. House. A proposal for an extended form of type checking of expressions. The Computer Journal, 26(4):366-374, 1983. Google Scholar
  9. Bart Jacobs. Categorical logic and type theory, volume 141. Elsevier, 1999. Google Scholar
  10. Andrew J. Kennedy. Relational parametricity and units of measure. In POPL'97, 1997. Google Scholar
  11. F. William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281-296, 1969. Google Scholar
  12. R Männer. Strong typing and physical units. ACM Sigplan Notices, 21(3):11-20, 1986. Google Scholar
  13. Mars Climate Orbiter Mishap Investigation Board. Phase I report. NASA, 1999. Google Scholar
  14. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Proc. POPL 2015, pages 3-16, 2015. Google Scholar
  15. John Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983. Google Scholar
  16. Ain A Sonin. The physical basis of dimensional analysis. Department of Mechanical Engineering, MIT, 2001. Google Scholar
  17. Mitchell Wand and Patrick O'Keefe. Automatic dimensional inference. In Computational Logic - Essays in Honor of Alan Robinson, pages 479-483, 1991. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact