Models for Polymorphism over Physical Dimension

Reference. Models for Polymorphism over Physical Dimension

Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton · TLCA · 2015 · dimension-types · DOI

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

Cite as @atkey-2015-models (helia, typst) · \cite{atkey-2015-models} (LaTeX)

BibTeX

bibtex · 14 lines

@inproceedings{atkey-2015-models,
  doi = {10.4230/LIPICS.TLCA.2015.45},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.45},
  author = {Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam},
  keywords = {Category Theory, Units of Measure, Dimension Types, Type Theory},
  language = {en},
  title = {Models for Polymorphism over Physical Dimension},
  volume = {38},
  pages = {45-59},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2015},
  copyright = {Creative Commons Attribution 3.0 Unported license},
  booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}
}

hayagriva YAML (typst)

yaml · 19 lines

atkey-2015-models:
  type: article
  title: Models for Polymorphism over Physical Dimension
  author:
  - Atkey, Robert
  - Ghani, Neil
  - Nordvall Forsberg, Fredrik
  - Revell, Timothy
  - Staton, Sam
  date: 2015
  page-range: 45-59
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.45
  serial-number:
    doi: 10.4230/LIPICS.TLCA.2015.45
  parent:
    type: proceedings
    title: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 38

Download: atkey-2015-models.bib · atkey-2015-models.yml

Cites 17 works (4 here)

With notes (4)

Functors are type refinement systems mellies_zeilberger_2015POPL · 2015

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds’ paper on “The Meaning of Types” (2000), showing how the paper’s main results may be reconstructed along these lines.

PDF · DOI · pldb

From parametricity to conservation laws, via Noether’s theorem atkey-2014-fromPOPL · 2014

PDF · DOI · pldb

Categorical Logic and Type Theory jacobs-19991999

This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.

Adjointness in Foundations lawvere_1969Dialectica · 1969

DOI

External (13)

Revisiting the categorical interpretation of dependent type theory (2014)
Categorical models for Abadi and Plotkin’s logic for parametricity (2005)
Adding apples and oranges (2002)
The physical basis of dimensional analysis (2001)
Some properties of Fib as a fibred 2-category (1999)
Phase I report (1999)
Relational parametricity and units of measure (1997)
Automatic dimensional inference (1991)
Strong typing and physical units (1986)
A proposal for an extended form of type checking of expressions (1983)
Types, abstraction and parametric polymorphism (1983)
G-groupoids, crossed modules and the fundamental groupoid of a topological group (1976)
On physically similar systems; illustrations of the use of dimensional equations (1914)