Abstract
Gentzen’s Hauptsatz – cut elimination theorem – in sequent calculi reveals a fundamental property on logic connectives in various logics such as classical logic and intuitionistic logic. In this paper, we implement a procedure in Haskell to perform cut elimination for intuitionistic sequent calculus, where we use types to guarantee that the procedure can only return a cut-free proof of the same sequent when given a proof of a sequent that may contain cuts. The contribution of the paper is two-fold. On the one hand, we present an interesting (and somewhat unexpected) application of the current type system of Haskell, illustrating through a concrete example how some typical use of dependent types can be simulated in Haskell. On the other hand, we identify several problematic issues with such a simulation technique and then suggest some approaches to addressing these issues in Haskell.
Partially supported by the NSF Grants No. CCR-0224244 and No. CCR-0229480
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
Baars, A.I., Swierstra, S.D.: Typing Dynamic Typing. In: Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP 2002), Pittsburgh, PA (October 2002)
Chen, C., Xi, H.: Implementing Typeful Program Transformations. In: Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics Based Program Manipulation, San Diego, CA, June 2003, pp. 20–28 (2003)
Chen, C., Zhu, D., Xi, H.: Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell (October 2003), Available at http://www.cs.bu.edu/~hwxi/academic/papers/CutElim
Cheney, J., Hinze, R.: A Lightweight Implementation of Generics and Dynamics. In: Proceedings of Haskell Workshop, Pittsburgh, PA, October 2002, pp. 90–104. ACM Press, New York (2002)
Cheney, J., Hinze, R.: Phantom Types. Technical Report CUCIS-TR2003-1901, Cornell University, Available as Dienst/UI/1.0/Display/cul.cis/TR2003-1901 (2003), http://techreports.library.cornell.edu:8081/
Fridlender, D., Indrika, M.: Do we need dependent types? Functional Pearl in the Journal of Functional Programming 10(4), 409–415 (2000)
Gentzen, G.: Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift 39, 176–210, 405–431 (1935)
Hall, C.V., Hammond, K., Jones, S.L.P., Wadler, P.L.: Type Classes in Haskell. ACM Transactions on Programming Languages and Systems 18(2), 109–138 (1996)
Harper, R.W., Honsell, F., Plotkin, G.D.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)
Hinze, R.: Manufacturing Datatypes. Journal of Functional Programming 11(5), 493–524 (2001); Also available as Technical Report IAI-TR-99-5, Institut für Informatik III, Universität Bonn
Jones, M.P.: Type Classes with Functional Dependencies. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 230–244. Springer, Heidelberg (2000)
McBride, C.: Faking It. Journal of Functional Programming 12(4&5), 375–392 (2002)
Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 348–375 (1978)
Okasaki, C.: From Fast Exponentiation to Square Matrices: An Adventure in Types. In: Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (September 1999)
Pfenning, F.: Computation and Deduction. Cambridge University Press, Cambridge (to appear)
Pfenning, F.: Logic programming in the LF logical framework. In: Huet, I.G., Plotkin, G. (eds.) Logical Frameworks, pp. 149–181. Cambridge University Press, Cambridge (1991)
Pfenning, F.: Structural Cut Elimination. In: Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, June 1995, pp. 156–166 (1995)
Pfenning, F.: Structural Cut Elimination I: intuitionistic and classical logic. Information and Computation 157(1/2), 84–141 (2000)
Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, LA, January 2003, pp. 224–235.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, C., Zhu, D., Xi, H. (2004). Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. In: Jayaraman, B. (eds) Practical Aspects of Declarative Languages. PADL 2004. Lecture Notes in Computer Science, vol 3057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24836-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-24836-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22253-8
Online ISBN: 978-3-540-24836-1
eBook Packages: Springer Book Archive