Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-25T07:21:18.309Z Has data issue: false hasContentIssue false
  • English
  • Français

Homotopical patch theory*

Published online by Cambridge University Press:  13 September 2016

CARLO ANGIULI ,
EDWARD MOREHOUSE ,
DANIEL R. LICATA  and
ROBERT HARPER
CARLO ANGIULI
Affiliation:
Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA (e-mails: [email protected], [email protected])
EDWARD MOREHOUSE
Affiliation:
Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA (e-mails: [email protected], [email protected])
DANIEL R. LICATA
Affiliation:
Department of Mathematics and Computer Science, Wesleyan University, Middletown, Connecticut, USA (e-mail: [email protected])
ROBERT HARPER
Affiliation:
Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Homotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.

Type
Research Article
Information
Journal of Functional Programming , Volume 26 , 2016 , e18
Copyright
Copyright © Cambridge University Press 2016 

Footnotes

*

This research was sponsored in part by the National Science Foundation under grant number CCF-1116703. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity. This material is based on research sponsored in part by The United States Air Force Research Laboratory under agreement number FA9550-15-1-0053. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government or Carnegie Mellon University.

References

Abbott, M., Altenkirch, T. & Ghani, N. (2005) Containers: Constructing strictly positive types. Theor. Comput. Sci. 342 (1), 3–27.Google Scholar
Aczel, P. (1977) The strength of Martin-Löf's intuitionistic type theory with one universe. In Proceedings of the Symposium on Mathematical Logic, Oulu, 1974. Dept. of Philosophy, University of Helsinki, Helsinki, Finland. Report No. 2, pp. 1–32.Google Scholar
Altenkirch, T. (2014) Containers in Homotopy Type Theory. Lyon: Talk at Mathematical Structures of Computation.Google Scholar
Altenkirch, T. & Kaposi, A. (2015) Towards Cubical Type Theory. Preprint. Available at: http://akaposi.bitbucket.org/nominal.pdf. (last accessed date 25/08/2016)Google Scholar
Altenkirch, T., McBride, C. & Swierstra, W. (2007) Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (PLPV '07). New York, NY, USA: ACM, pp. 57–68.Google Scholar
Awodey, S. & Warren, M. A. (2009) Homotopy theoretic models of identity types. Math. Proc. Camb. Phil. Soc 146 (1), 45–55.Google Scholar
Barras, B., Coquand, T. & Huber, S. (2015) A generalization of the Takeuti–Gandy interpretation. Math. Struct. Comput. Sci. 25 (5), 1071–1099.Google Scholar
Bezem, M., Coquand, T. & Huber, S. (2014) A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), Matthes, R. & Schubert, A. (eds), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, vol. 26, pp. 107–128.Google Scholar
Camp Project. (2010) Available at: http://projects.haskell.org/camp/. (last accessed date 25/08/2016)Google Scholar
Cavallo, E. (2015) Synthetic Cohomology in Homotopy Type Theory. M.Phil. Thesis, Carnegie Mellon University.Google Scholar
Cohen, C., Coquand, T., Huber, S. & Mörtberg, A. (2016) Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. Preprint. Available at: http://www.cse.chalmers.se/~coquand/cubicaltt.pdf. (last accessed date 25/08/2016)Google Scholar
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe Douglas, J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki James, T. & Smith, S. F. (1986) Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall.Google Scholar
Coq Development Team. (2015) The Coq proof assistant reference manual, version 8.5. INRIA. Available at: http://coq.inria.fr/. (last accessed date 25/08/2016)Google Scholar
Dagit, J. (2009) Type-Correct Changes–-A Safe Approach to Version Control Implementation. MS Thesis. Corvallis, Oregon, USA: Oregon State University.Google Scholar
Darcs Project. (2013) Available at: http://darcs.net/. (last accessed date 25/08/2016)Google Scholar
Gambino, N. & Garner, R. (2008) The identity type weak factorisation system. Theor. Comput. Sci. 409 (3), 94–109.Google Scholar
Garner, R. (2009) Two-dimensional models of type theory. Math. Struct. Comput. Sci. 19 (4), 687–736.Google Scholar
Hofmann, M. & Streicher, T. (1998) The groupoid interpretation of type theory. Twenty-Five Years of Constructive Type Theory. Oxford University Press.CrossRefGoogle Scholar
Hou, K.-B. (Favonia) (2014) Covering spaces in homotopy type theory. Talk at TYPES 2014.Google Scholar
Houston, R. (2012) On editing text. Available at: http://bosker.wordpress.com/2012/05/10/on-editing-text/. (last accessed date 25/08/2016)Google Scholar
Jacobson, J. (2009) A formalization of Darcs patch theory using inverse semigroups. Available at: ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf. (last accessed date 25/08/2016)Google Scholar
Kapulkin, C., Lumsdaine, P. L. & Voevodsky, V. (2012) The Simplicial Model of Univalent Foundations. arXiv:1211.2851.Google Scholar
Kleene, S. C. (1945) On the interpretation of intuitionistic number theory. J. Symbol. Log. 10 (4), 109–124.Google Scholar
Kreisel, G. (1959) Interpretation of analysis by means of constructive functionals of finite types. In Constructivity in Mathematics, Heyting, A. (ed), Amsterdam: North-Holland Pub. Co, pp. 101–128.Google Scholar
Lawvere, F. W. (1963) Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. PhD Thesis, Columbia University.Google Scholar
Licata, D. R., & Brunerie, G. (2013) π n (Sn ) in homotopy type theory. In Proceedings of the Third International Conference on Certified Programs and Proofs. New York, NY, USA: Springer-Verlag New York, Inc., pp. 1–16.Google Scholar
Licata, D. R., & Brunerie, G. (2015) A Cubical Approach to Synthetic Homotopy Theory. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '15). Washington, DC, USA: IEEE Computer Society, pp. 92–103.Google Scholar
Licata, D. R. & Finster, E. (2014) Eilenberg–MacLane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '14). New York, NY, USA: ACM, pp. 66:1–66:9.Google Scholar
Licata, D. R., & Harper, R. (2011) 2-dimensional directed type theory. In Electron. Notes Theor. Comput. Sci. 276, 263–289.Google Scholar
Licata, D. R. & Harper, R. (2012) Canonicity for 2-dimensional type theory. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12). New York, NY, USA: ACM, pp. 337–348.CrossRefGoogle Scholar
Licata, D. R. & Shulman, M. (2013) Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '13). Washington, DC, USA: IEEE Computer Society, pp. 223–232.Google Scholar
Löh, A., Swierstra, W. & Leijen, D. (2007) A Principled Approach to Version Control. Preprint. Available at: http://www.andres-loeh.de/VersionControl.html. (last accessed date 25/08/2016)Google Scholar
Lumsdaine, P. L. (2009) Weak ω-categories from intensional type theory. In Typed Lambda Calculi and Applications: 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1–3, 2009. Proceedings. Curien, P.-L. (ed), Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 172–187.Google Scholar
Lumsdaine, P. L. (2011 April) Higher Inductive Types: A Tour of the Menagerie. Available at: http://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/. (last accessed date 25/08/2016)Google Scholar
Lumsdaine, P. L. & Shulman, M. (2013) Higher Inductive Types. In preparation.Google Scholar
Lynagh, I. (2012 January) Camp Patch Theory. Available at: http://projects.haskell.org/camp/files/theory.pdf. (last accessed date 25/08/2016)Google Scholar
McBride, C. (2000) Dependently Typed Functional Programs and Their Proofs. PhD Thesis, University of Edinburgh.Google Scholar
Mimram, S. & Di Giusto, C. (2013) A categorical theory of patches. Electron. Notes Theor. Comput. Sci. 298, 283–307.Google Scholar
Nordström, B., Peterson, K. & Smith, J. M. (1990) Programming in Martin-Löf's Type Theory, an Introduction. Clarendon Press.Google Scholar
Norell, U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology.Google Scholar
Pijul Project. (2015) Available at: https://pijul.org/. (last accessed date 25/08/2016)Google Scholar
Polonsky, A. (2015) Internalization of Extensional Equality. arXiv.1401.1148.Google Scholar
Reynolds, J. C. (2002) Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS '02). Washington, DC, USA: IEEE Computer Society, pp. 55–74.Google Scholar
Roundy, D. (2005) Darcs: Distributed version management in haskell. In Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell (Haskell '05). New York, NY, USA: ACM, pp. 1–4.Google Scholar
Roundy, D. (2009 April) Theory of Patches. Available at: http://www.cs.tufts.edu/comp/150GIT/archive/david-roundy/theory-patches-2009.pdf. (last accessed date 25/08/2016)Google Scholar
Shulman, M. (2011 April) Homotopy Type Theory VI: Higher Inductive Types. Available at: http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html. (last accessed date 25/08/2016)Google Scholar
Shulman, M. (2015) Univalence for inverse diagrams and homotopy canonicity. Math. Structures Comput. Sci. 25, 1203–1277.Google Scholar
Sittampalam, G. et al. (2005) Some Properties of Darcs Patch Theory. Available at: http://urchin.earth.li/darcs/ganesh/darcs-patch-theory/theory/formal.pdf. (last accessed date 25/08/2016)Google Scholar
Swierstra, W. & Löh, A. (2014) The semantics of version control. In Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward! 2014). New York, NY, USA: ACM, pp. 43–54.Google Scholar
Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Available at: http://homotopytypetheory.org/book. (last accessed date 25/08/2016)Google Scholar
van den Berg, B. & Garner, R. (2011) Types are weak ω-groupoids. Proc. London Math. Soc. 102 (2), 370–394.Google Scholar
Voevodsky, V. (2006) A very short note on homotopy λ-calculus. Unpublished, September, 1–7.Google Scholar
Warren, M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory. PhD Thesis, Carnegie Mellon University.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.