Dependently-typed programming in scientific computing: Examples from economic modelling
Cezar Ionescu and Patrik Jansson
Abstract
Computer simulations are essential in virtually every scientific discipline, even more so in those such as economics or climate change where the ability to make laboratory experiments is limited. Therefore, it is important to ensure that the models are implemented correctly, that they can be re-implemented and that the results can be reproduced. Typically, though, the models are described by a mixture of prose and mathematics which is insufficient for these purposes. We argue that using dependent types allows us to gradually reduce the gap between the mathematical description and the implementation, and we give examples from economic modelling. We discuss the consequences that our incremental approach has on programming style and the requirements it imposes on the dependently-typed programming languages used.
Talk
Presented at IFL 2012 by Cezar Ionescu.
Video: http://www.youtube.com/watch?v=VDMkt9ND5Es
Paper
Accepted for the IFL 2012 post-proceedings, February 2013 (submitted November 2012).
Projects
This work was partially funded by the GSDP project.
2018-04-10: New grant application submitted SciDeR - Scientific Computing with Dependent Types for Reliability to VR
Related work
Earlier related papers by the same authors are
- Testing versus proving in climate impact research
- Computational Vulnerability Assessment (Generic Libraries in C++ with Concepts from High-Level Domain Descriptions in Haskell)