PhD course on “Functional Programming and Climate Impact Research”, spring term 2024, study period 4.
Abstract: This is a course aimed at PhD students or MSc students interested in the application of functional programming, domain-specific languages, and dependent types to climate impact research.
Note. This course is run as a seminar / reading course. Therefore, you must have the motivation and capacity to digest material with limited teacher presence.
The course is based on material from the following research papers:
- Week 15: read 2010: Vulnerability modelling with functional programming and dependent types
- Week 16: read 2011: Testing versus proving in climate impact research
- Week 17: read 2012: Dependently-Typed Programming in Scientific Computing - Examples from Economic Modelling
- Week 18: read 2014: Towards a Computational Theory of GSS: a Case for Domain-Specific Languages
- Week 19: read 2017: Sequential decision problems, dependent types and generic solutions
- Week 20: read 2017: Contributions to a computational theory of policy advice and avoidability
- Week 21: read 2018: The impact of uncertainty on optimal emission policies
- Week 22: read 2023: Responsibility Under Uncertainty: Which Climate Decisions Matter Most?
Good background reading is provided by the 2023 book ”Computing the Climate” by Steve M. Easterbrook and the 2022 book ”Domain-Specific Languages of Mathematics” by Jansson, Ionescu, Bernardy.
The course is examined through
- a sequence of graded hand-ins (solutions to exercises to be further specified during the course)
- active participation in most of the weekly seminars
The plan is to award 7.5 higher education credits (ECTS) upon successful completion of the course.
- BSc degree in Computer Science and Engineering or equivalent.
- Functional programming (ideally in Haskell, but other languages are also OK)
- Formal methods (ideally using dependent types, but other methods are also OK)
- Use functional programming specification / implementation / formalisation as a way of understanding new domains
- Understand a selection of topics in Climate Impact Research
- Effectively use Haskell and Agda for formalisation
- Master the terminology, concepts and theories associated with the selected area;
- Demonstrate deep knowledge and understanding in the area of the course, and insight into current research and development;
- Demonstrate deep methodological knowledge in the area of the course;
- Demonstrate the ability to critically and systematically integrate knowledge and to analyse, assess, and deal with complex issues in the area of the course;
- Search for, and extract, necessary information from scientific publications in the selected area of the course, with the purpose of identifying strengths and weakness of solutions, approaches and methodologies.
- The course will start in March (2024-03-25) and end in May or June.
- The schedule is available below:
| Week | Date | Time | Event | Room |
|---|---|---|---|---|
| 13 | Mon 2024-03-25 | 15.15-17.00 | FPClimate seminar 1 | EDIT 6128 |
| 13 | Tue 2024-03-26 | 14.15-15.15 | Talk by Anil Madhavapeddy | HB2 |
| 14 | (Patrik away) | |||
| 15 | Mon 2024-04-08 | 15.15-17.00 | FPClimate seminar 2 (Cezar Ionescu) | EDIT 6128 |
| 16 | Mon 2024-04-15 | 15.15-17.00 | FPClimate seminar 3 | EDIT 6128 |
| 17 | Mon 2024-04-22 | 15.15-17.00 | FPClimate seminar 4 | EDIT 6128 |
| 18 | Mon 2024-04-29 | 15.15-17.00 | FPClimate seminar 5 (Nicola Botta) | EDIT 6128 |
| 19 | Mon 2024-05-06 | 15.15-17.00 | FPClimate seminar 6 | EDIT 6128 |
| 20 | Mon 2024-05-13 | 15.15-17.00 | FPClimate seminar 7 | EDIT 6128 |
| 21 | Mon 2024-05-20 | 15.15-17.00 | FPClimate seminar 8 (Nicola Botta) | EDIT 5128 |
| 22 | Mon 2024-05-27 | 15.15-17.00 | FPClimate seminar 9 | EDIT 6128 |
- Time zone: CET (UTC+1) in week 13 (until 2024-03-30), then CEST (UTC+2) from week 14 onwards.
- For local participants, the room is EDIT 6128 (at Chalmers campus Johanneberg) for most seminars.
- For remote participants, the zoom link is almost https://chalmers.zoom.us/my/CUTpatrikja but without the upper case letters.
- Introduction slides (Patrik Jansson) including exercises
- We did a round of introductions, followed by an introduction by Patrik to the course (prerequisites, contents, examination, learning outcomes, schedule, first few weeks).
- Then Patrik presented some introductory material (see the slides) about equations, problems, solutions, specifications, domain-specific languages, etc.
- In the course we use logic and functional programming notation (mostly Haskell and Agda) to specify, implement, and test concepts from Climate Impact Research.
- Brief introduction to some relevant domain-specific notions: prisoner’s dilemma, strategy profile, Nash equilibrium, policies, optimality, agent-based models, green growth, equational reasoning.
- Homework for next seminar:
- solve the exercises and
- actively read Vulnerability modelling with functional programming and dependent types in preparation for the seminar by Cezar Ionescu.
- Next up is an invited talk:
Talk by Prof. Anil Madhavapeddy
- Announced separately [will be in room HB2]
- Title: (Functional) Programming for the Planet
- Abstract: As simultaneous crises in emissions and biodiversity sweep the planet, computer systems that analyse the complex interplay of our globe’s health are ever more crucial to guiding policy decisions about how to get out of the mess we’re in. In this talk, we examine how functional programming can contribute to building systems that are more resilient, predictable and reproducible in the face of huge amounts of input data (such as from satellites and ground sensing) that demands precise access control (or else poachers and malicious actors go straight to the source) and requires interactive exploration from non-CS-experts at different levels of the software stack (to do climate science). We will also highlight how our ongoing cross-disciplinary research is having a real impact on conservation projects that are sorely underserved by current systems/PL infrastructure, and also how we went about forging these links. We hope to encourage some of you to form your own local collaborations with your colleagues working on the climate crisis!
- For those who missed it, there is a closely related recorded keynote from ICFP 2023.
solve W13 exercises (FPClimate_seminar_1.pdf) and W15 preparation exercises (ref/seminar_2_exercises.pdf)
read and prepare questions for ”Vulnerability modelling …” paper
- 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” [Ionescu, 2016] doi:10.1017/S0960129514000139
- Definitions
- There were many attempts at defining “vulnerability” around 2000 [Thywissen 2006 lists 36!]
- The Structure of Vulnerability (according to [Ionescu, 2016])
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.
FPClimate seminar 3: Discussion about the current paper: Testing versus proving in climate impact research
- Exercises: (informally: “re-implement the paper”)
F = Vec 3 (a vector of length 3);
V = Rational; and
x1, x2 : F V
x1 = [1, 1, 1];
x2 = [1, 2, 1];
- Q1a: What does Def. 1 say about m x1 in relation to m x2?
- Q1b: What do you think it should say?
- Q1c: Can you suggest another Def 1’ (which is stronger / stricter than Def. 1) and captures this case?
- Q2a: Find counterexamples to sumList and to supList being vulnerability measures.
- Q2b: Re-implement with Rational instead of Float. Are they correct now?
- (starting from the paper or from the subdirectory file:ref/test-vs-proof/).
- Q3a: To get started with Agda, implement a self-contained version of the code up to FunctorList (with minimal imports).
- Q3b: Make the definition of VulnMeas work (type check) for a recent version of Agda and its standard library.
- Q3c: Implement foldMeas based on a suitable number of postulates for the properties you need.
- Lecture by Nicola Botta
- implement Backwards induction in different languages (one per person)
- Prel. plan: Agda (Oskar), Haskell (Janek), Python (Adrian), Purescript (Nicolas), Rust (Tobias), Julia (Jayson)
- and apply it to 2-3 simple examples [generation problem, random walk, your favourite!]
- More concretely:
- compute an optimal policy sequence (for, say, n=3 steps)
- compute all trajectories (or a sample)
- sort them by probability
- show the first few examples
- say something about the computational cost (complexity)
- You don’t need to prove correctness, or implement the dependent types, but you need to have a “generic” (polymorphic / parametric) solver so that a user can supply a sequential decision problem (X, Y, next, reward, …) and get a solution (a sequence of optimal policies).
- You can assume that the state and action types are finite, so that the solution space also is finite.
- Make sure to provide some test cases and expected outputs.
- Lecture by Nicola Botta
- Thu 2024-06-13, 13:00-15:00, in room EDIT-5128
- If you do not need formal credits, you can just contact Patrik Jansson.
- If you want credits for your local MSc degree, contact the examiner for (DAT235/DIT577): [Ana Bove](https://www.cse.chalmers.se/~bove/)
- If you want credits for your local PhD degree, obtain the approval of your supervisor and examiner, then contact Patrik Jansson.
- TODO add links to talks, etc. online