Abstract
The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs.
To address these issues we introduce ΠΣ, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursion—used for types, functions and infinite objects—and an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of α-equality for recursive definitions. We show, by translating several high-level constructions, that ΠΣ is suitable as a core language for dependently typed programming.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Altenkirch, T., Oury, N.: ΠΣ: A core language for dependently typed programming. Draft (2008)
Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter. Draft (2005)
Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Proceedings of the 2007 workshop on Programming languages meets program verification, pp. 57–68 (2007)
Augustsson, L.: Cayenne — a language with dependent types. In: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp. 239–250 (1998)
Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: A standalone typechecker for ETT. In: Trends in Functional Programming, vol. 6. Intellect (2006)
The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009)
Coquand, T.: A calculus of definitions, Draft (2008), http://www.cs.chalmers.se/~coquand/def.pdf
Coquand, T., Kinoshita, Y., Nordström, B., Takeyama, M.: A simple type-theoretic language: Mini-TT. In: From Semantics to Computer Science; Essays in Honour of Gilles Kahn, pp. 139–164. Cambridge University Press, Cambridge (2009)
Cui, S., Donnelly, K., Xi, H.: ATS: A language that combines programming with theorem proving. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 310–320. Springer, Heidelberg (2005)
Danielsson, N.A., Altenkirch, T.: Mixing induction and coinduction. Draft (2009)
Dybjer, P., Setzer, A.: Indexed induction-recursion. Journal of Logic and Algebraic Programming 66(1), 1–49 (2006)
Giménez, E.: Un Calcul de Constructions Infinies et son Application à la Vérification de Systèmes Communicants. PhD thesis, Ecole Normale Supérieure de Lyon (1996)
Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 521–540. Springer, Heidelberg (2006)
Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science 5(3, 9) (2009)
McBride, C.: The Strathclyde Haskell Enhancement (2009), http://personal.cis.strath.ac.uk/~conor/pub/she/
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University (2007)
Sheard, T.: Putting Curry-Howard to work. In: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pp. 74–85 (2005)
Sozeau, M.: Un environnement pour la programmation avec types dépendants. PhD thesis, Université Paris 11 (2008)
Sulzmann, M., Chakravarty, M.M.T., Jones, S.P., Donnelly, K.: System F with type equality coercions. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 53–66 (2007)
Wadler, P., Taha, W., MacQueen, D.: How to add laziness to a strict language, without even being odd. In: The 1998 ACM SIGPLAN Workshop on ML (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N. (2010). ΠΣ: Dependent Types without the Sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-12251-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12250-7
Online ISBN: 978-3-642-12251-4
eBook Packages: Computer ScienceComputer Science (R0)
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.