Tic tac types: a gentle introduction to dependently typed programming (functional pearl)
Authors: 
Sean Innes, 
Nicolas WuAuthors Info & Claims
Pages 40 - 51
Abstract
Tic-Tac-Toe is a simple, familiar, classic game enjoyed by many. This pearl is designed to give a flavour of the world of dependent types to the uninitiated functional programmer. We cover a journey from Tic-Tac-Terrible implementations in the harsh world of virtually untyped |Strings|, through the safe haven of vectors that know their own length, and into a Tic-Tac-Titanium version that is too strongly typed for its own good. Along the way we discover something we knew all along; types are great, but in moderation. This lesson is quickly put to use in a more complex recursive version.
Supplementary Material
Video Presentation
- Download
- 28.14 MB
References
[1]
F. Bancilhon and N. Spyratos. 1981. Update Semantics of Relational Views. ACM Trans. Database Syst. 6, 4 (Dec. 1981), 557–575.
[2]
Richard Bird, Jeremy Gibbons, Stefan Mehner, Janis Voigtländer, and Tom Schrijvers. 2013. Understanding Idiomatic Traversals Backwards and Forwards. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell (Haskell ’13). ACM, New York, NY, USA, 25–36.
[3]
Richard Bird and Lambert Meertens. 1998. Nested datatypes. In Mathematics of Program Construction, Johan Jeuring (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 52–67.
[4]
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.
[5]
Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs/1610.07978 (2016). arXiv: 1610.07978
[6]
Richard A Eisenberg and Jan Stolarek. 2015. Promoting functions to type families in Haskell. ACM SIGPLAN Notices 49, 12 (2015), 95–106.
[7]
Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In Proceedings of the 2012 Haskell Symposium (Haskell ’12). ACM, New York, NY, USA, 117–130.
[8]
J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. 2005. Combinators for Bi-directional Tree Transformations: A Linguistic Approach to the View Update Problem. SIGPLAN Not. 40, 1 (Jan. 2005), 233–246.
[9]
Jeremy Gibbons and Bruno C. D. S. Oliveira. 2009. The essence of the Iterator pattern. Journal of Functional Programming 19, 3-4 (2009), 377–402.
[10]
Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2015. Conjugate Hylomorphisms–Or: The Mother of All Structured Recursion Schemes. In ACM SIGPLAN Notices, Vol. 50. ACM, 527–538.
[11]
Mauro Jaskelioff and Russell O’Connor. 2015. A representation theorem for second-order functionals. Journal of Functional Programming 25 (2015), e13.
[12]
Sam Lindley and Conor McBride. 2013. Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell (Haskell ’13). ACM, New York, NY, USA, 81–92.
[13]
Conor McBride. 2011. Functional pearl: Kleisli arrows of outrageous fortune. Journal of Functional Programming (to appear) (2011).
[14]
Conor McBride and James McKinna. 2004. The view from the left. Journal of Functional Programming 14, 1 (2004), 69–111.
[15]
Conor McBride and Ross Paterson. 2008. Applicative programming with effects. Journal of Functional Programming 18, 1 (2008), 1–13.
[16]
Erik Meijer, Maarten Fokkinga, and Ross Paterson. 1991. Functional programming with bananas, lenses, envelopes and barbed wire. In Functional Programming Languages and Computer Architecture, John Hughes (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 124–144.
[17]
Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.
[18]
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple Unification-based Type Inference for GADTs. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, New York, NY, USA, 50–61.
[19]
Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. 2017. Profunctor Optics: Modular Data Accessors. CoRR abs/1703.10857 (2017). arXiv: 1703.10857
[20]
Maciej Piróg, Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff. 2018. Syntax and Semantics for Operations with Scopes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). ACM, New York, NY, USA, 809–818.
[21]
Robert Pollack. 1992. Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks. pages.
[22]
Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89). ACM, New York, NY, USA, 347–359.
[23]
Philip Wadler. 1995. Monads for Functional Programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text. SpringerVerlag, Berlin, Heidelberg, 24–52.
Index Terms
- Tic tac types: a gentle introduction to dependently typed programming (functional pearl)
Recommendations
Dependently typed programming in Agda
TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementationDependently typed languages have for a long time been used to describe proofs about programs. Traditionally, dependent types are used mostly for stating and proving the properties of the programs and not in defining the programs themselves. An ...
Bidirectional Elaboration of Dependently Typed Programs
PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative ProgrammingDependently typed programming languages allow programmers to express a rich set of invariants and verify them statically via type checking. To make programming with dependent types practical, dependently typed systems provide a compact language for ...
Dependently typed programming with singletons
Haskell '12: Proceedings of the 2012 Haskell SymposiumHaskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 August 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICFP '19
Sponsor:
ICFP '19: ACM SIGPLAN International Conference on Functional Programming
August 18, 2019
Berlin, Germany
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 734Total Downloads
- Downloads (Last 12 months)11
- Downloads (Last 6 weeks)1
Reflects downloads up to 29 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in