Document Open Access Logo

The Münchhausen Method in Type Theory

Authors Thorsten Altenkirch , Ambrus Kaposi , Artjoms Šinkarovs , Tamás Végh

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2022.10.pdf
  • Filesize: 0.68 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Type structures
Keywords
  • type theory
  • proof assistants
  • very dependent types

Metrics

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

Abstract

In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g. x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.

Cite As Get BibTex

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen Method in Type Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.TYPES.2022.10

Author Details

Thorsten Altenkirch
  • School of Computer Science, University of Nottingham, UK
Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Artjoms Šinkarovs
  • Heriot-Watt University, Edinburgh, Scotland, UK
Tamás Végh
  • Eötvös Loránd University, Budapest, Hungary

Funding

  • Kaposi, Ambrus: Supported by the "Application Domain Specific Highly Reliable IT Solutions" project which has been implemented with support from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme, and by Bolyai Scholarship BO/00659/19/3.
  • Šinkarovs, Artjoms: Supported by the Engineering and Physical Sciences Research Council through the grant EP/N028201/1.

References

  1. Agda Development Team. Agda 2.6.3 documentation, 2023. Accessed [2023/05/01]. URL: https://agda.readthedocs.io/en/v2.6.3/.
  2. Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. ΠΣ: Dependent types without the sugar. Functional and Logic Programming, pages 40-55, 2010. Google Scholar
  3. Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen method and combinatory type theory. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes, 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_8.pdf.
  4. Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, and Anton Setzer. A categorical semantics for inductive-inductive definitions. In CALCO, pages 70-84, 2011. URL: https://doi.org/10.1007/978-3-642-22944-2_6.
  5. Henk Barendregt. Introduction to generalized type systems. J. Funct. Program., 1(2):125-154, 1991. URL: https://doi.org/10.1017/s0956796800020025.
  6. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827, 2019. URL: https://arxiv.org/abs/1904.00827.
  7. Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:27, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.2.
  8. Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University (United Kingdom), 2013. Google Scholar
  9. J. I. Glasgow and M. A. Jenkins. Array theory, logic and the nial language. In Proceedings. 1988 International Conference on Computer Languages, pages 296-303, October 1988. URL: https://doi.org/10.1109/ICCL.1988.13077.
  10. Jason J. Hickey. Formal objects in type theory using very dependent types. In In Foundations of Object Oriented Languages 3, 1996. Google Scholar
  11. J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda-Calculus. Cambridge University Press, 1986. Google Scholar
  12. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 153-164, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  13. Kenneth E. Iverson. A Programming Language. John Wiley & Sons, Inc., New York, NY, USA, 1962. Google Scholar
  14. Ambrus Kaposi, András Kovács, and Nicolai Kraus. Shallow embedding of type theory is morally correct. In Graham Hutton, editor, Mathematics of Program Construction, pages 329-365, Cham, 2019. Springer International Publishing. Google Scholar
  15. András Kovács. Generalized universe hierarchies and first-class universe levels. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.28.
  16. Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith, editors, Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 127-172. Oxford University Press, 1998. Google Scholar
  17. Conor McBride. What is the combinatory logic equivalent of intuitionistic type theory? Answer to question on StackOverflow, 2012. URL: https://stackoverflow.com/questions/11406786/what-is-the-combinatory-logic-equivalent-of-intuitionistic-type-theory.
  18. Artjoms Šinkarovs. Multi-dimensional arrays with levels. In Max S. New and Sam Lindley, editors, Proceedings Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020, Dublin, Ireland, 25th April 2020, volume 317 of EPTCS, pages 57-71, 2020. URL: https://doi.org/10.4204/EPTCS.317.4.
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