A short description of the second seminar of the FPClimate course. The first seminar has its own blog post.
Lecture (slides, source) by Prof. Cezar Ionescu
about Vulnerability Modelling with Functional Programming and Dependent Types
- (Prof. Ionescu very sadly passed away after severe illness in October 2024.)
Background: Algebra of Programming (the book, by Richard Bird and Ooge de Moor)
- Category theory is an extensible language for precisely formulating mathematical theories (concepts, models, etc.).
- One such extension is particularly well-suited for formulating functional programs.
- Further extensions allow us to formulate specifications.
- There are other frameworks with similar properties: higher-order logics (dependent types), Hoare logics, etc.
- The categorical framework is good for equational reasoning.
Potsdam Institute for Climate Impact Research (PIK)
- The work described in this lecture (and this course) started at PIK, around 2010.
- Relation-based computations in a monadic BSP model [Botta, Ionescu, 2007] <doi:10.1016/j.parco.2007.08.002>, PIK page
Vulnerability modelling [the paper this seminar is about]
- Motivated by a surge in "Vulnerability assessment" work in the climate change community.
- Cezar's paper first submitted in 2010, published 2014, Journal version 2016!
- ["Vulnerability Modelling with Functional Programming and Dependent Types"(doi:10.1017/S0960129514000139) [Ionescu, 2016] <doi:10.1017/S0960129514000139>
Definitions of Vulnerability
- There were many attempts at defining "vulnerability" around 2000
- [Thywissen 2006]lists 36 definitions!
The Structure of Vulnerability (according to [Ionescu, 2016]) Illustrated by the following Haskell code:
possible :: Functor f => State -> f Evolution
harm :: Preorder v => Evolution -> v
measure :: Functor f, Preorder v, Preorder w => f v -> w
vulnerability :: Preorder w => State -> w
vulnerability = measure . fmap harm . possible
- The paper presents a few examples which fit this structure.
Vulnerability measures
- should be monotonic
- can be related by natural transformations between representations of possibility
- should be "compatible\"
Next stage: dependent types
- (under the influence of Patrik Jansson)
- moving the categorical machinery to the new framework
Conclusions
- Main idea: formulate problems as programming correctness problems!
- This can be useful in contexts where simulation is used to replace experiments (climate science, social science, political theory, etc.).
- Type theory can formulate both correctness conditions and the programs themselves.
- Moreover, the correctness proofs are then mechanically checked.