Abstract
Types describe a program’s meaning. Dependent types, which allow types to be predicated on values, allow a program to be given a more precise type, and thus a more precise meaning. Typechecking amounts to verifying that the implementation of a program matches its intended meaning. In this tutorial, I will describe Idris, a pure functional programming language with dependent types, and show how it may be used to develop verified embedded domain specific languages (EDSLs). Idris has several features intended to support EDSL development, including syntax extensions, overloadable binders and implicit conversions. I will describe how these features, along with dependent types, can be used to capture important functional and extra-functional properties of programs, how resources such as file handles and network protocols may be managed through EDSLs, and finally describe a general framework for programming and reasoning about side-effects, implemented as an embedded DSL.
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
Similar content being viewed by others
Notes
- 1.
Typically, and perhaps confusingly, referred to in the dependently typed programming literature as “vectors”.
- 2.
- 3.
- 4.
Named instances are also available, but beyond the scope of this tutorial.
- 5.
- 6.
- 7.
Reading a line may fail, but for the purposes of this example, we consider this harmless and return an empty string.
- 8.
In practice, ’name simply introduces a new empty type.
References
Bauer, A., Pretnar, M.: Programming with Algebraic Effects and Handlers (2012). http://arxiv.org/abs/1203.1539
Brady, E.: Idris - systems programming meets full dependent types. In: Programming Languages Meets Program Verification (PLPV 2011), pp. 43–54 (2011)
Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552–593 (2013)
Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: ICFP 2013: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ACM (2013)
Brady, E.: Programming in Idris : a tutorial (2013)
Brady, E., Hammond, K.: Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocols. Fundamenta Informaticae 102(2), 145–176 (2010)
Brady, E., Hammond, K.: Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation. In: ICFP 2010: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, pp. 297–308. ACM, New York (2010)
Brady, E., Hammond, K.: Resource-safe systems programming with embedded domain specific languages. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 242–257. Springer, Heidelberg (2012)
Christiansen, D.: Dependent type providers. In: WGP 2013: Proceedings of the 9th ACM SIGPLAN Workshop on Generic Programming. ACM (2013)
Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York (1980). A reprint of an unpublished manuscript from 1969
McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69–111 (2004)
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18, 1–13 (2008)
Peyton Jones, S., et al.: Haskell 98 language and libraries - the revised report (2002). http://www.haskell.org/
Acknowledgements
I am grateful to the Scottish Informatics and Computer Science Alliance (SICSA) for funding this research. I would also like to thank the many contributors to the Idris system and libraries, as well as the reviewers for their helpful and constructive suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Brady, E. (2015). The Idris Programming Language. In: Zsók, V., Horváth, Z., Csató, L. (eds) Central European Functional Programming School. CEFP 2013. Lecture Notes in Computer Science(), vol 8606. Springer, Cham. https://doi.org/10.1007/978-3-319-15940-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-15940-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15939-3
Online ISBN: 978-3-319-15940-9
eBook Packages: Computer ScienceComputer Science (R0)