Abstract
Simplicity is a Turing-incomplete typed combinator language for smart contracts with a formal semantics. The design of Simplicity makes it possible to statically estimate the resources (e.g., memory) required to execute contracts. Such a feature is highly relevant in blockchain applications to efficiently determine fees to run smart contracts. Despite being Turing incomplete, the language is capable of expressing non-trivial contracts. Often, Simplicity programs contain lots of code repetition that could otherwise be avoided if it had common programming languages features, such as local definitions, functions, and bounded loops. In this work, we provide the foundations to make Simplicity a richer language. To achieve that, we connect Simplicity’s primitives with a categorical model. By doing so, we lift the language to a more abstract representation that will allow us to extend it by leveraging category theory models for computations. This methodology facilitates the addition of local definitions, functions, and bounded loops. We provide an implementation of Simplicity and its virtual machine in the functional programming language Haskell.
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.
Our implementation and accompanying material are available at https://bitbucket.org/russo/isola-additional-material/overview.
- 2.
In category theory, copair is commonly used without the product with E: if \(f' : A \rightarrow C\) and \(g' : B \rightarrow C\), then \([ f', g' ] : A + B \rightarrow C\). However, using the morphism containing E will ease the equivalence between morphisms and Simplicity terms.
- 3.
The encoding of a category using the eDSL for BCCs\(_\text {Hask}\) does not ensure that the category is indeed a BCC. It is the programmers responsibility to ensure this by verifying the existence of constructed morphisms and proving the corresponding laws. The eDSL is simply the “language of BCCs where objects are Haskell types.”
References
Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013)
Cousineau, G., Curien, P., Mauny, M.: The categorical abstract machine. Sci. Comput. Program. 8(2), 173–202 (1987)
Elliott, C.: Compiling to categories. In: Proceedings of the ACM on Programming Languages (ICFP) (2017). http://conal.net/papers/compiling-to-categories
Marlow, S.: Haskell 2010 language report (2010). http://www.haskell.org/
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)
O’Connor, R.: Simplicity: a new language for blockchains. In: Proceedings of the Workshop on Programming Languages and Analysis for Security, PLAS 2017. ACM (2017)
O’Connor, R.: Simplicity: a new language for blockchains. CoRR abs/1711.03028 (2017). http://arxiv.org/abs/1711.03028
Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for gadts. In: ACM SIGPLAN Notices, vol. 41, pp. 50–61. ACM (2006)
Schwartz, D., Youngs, N., Britto, A., et al.: The ripple protocol consensus algorithm. Ripple Labs Inc White Paper 5 (2014)
Swan, M.: Blockchain: Blueprint for a New Economy. O’Reilly Media Inc., Newton (2015)
Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-59451-5_2
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1–32 (2014)
Acknowledgments
This work was funded by the Swedish Foundation for Strategic Research (SSF) under the project Octopi (Ref. RIT17-0023) and the Swedish research agency Vetenskapsrådet.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Valliappan, N., Mirliaz, S., Lobo Vesga, E., Russo, A. (2018). Towards Adding Variety to Simplicity. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_31
Download citation
DOI: https://doi.org/10.1007/978-3-030-03427-6_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03426-9
Online ISBN: 978-3-030-03427-6
eBook Packages: Computer ScienceComputer Science (R0)