/FPClimate

PhD course on Functional Programming and Climate Impact Research

Primary LanguageAgda

FPClimate

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.

Lecture / seminar / reading plan

The course is based on material from the following research papers:

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.

Examination

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.

Prerequisites

  • 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)

Learning outcomes (after completion of the course the student should be able to)

  • 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

Knowledge and understanding

  • 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;

Skills and abilities

  • Demonstrate the ability to critically and systematically integrate knowledge and to analyse, assess, and deal with complex issues in the area of the course;

Judgement and approach

  • 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.

Scheduling

  • The course will start in March (2024-03-25) and end in May or June.
  • The schedule is available below:
WeekDateTimeEventRoom
13Mon 2024-03-2515.15-17.00FPClimate seminar 1EDIT 6128
13Tue 2024-03-2614.15-15.15Talk by Anil MadhavapeddyHB2
14(Patrik away)
15Mon 2024-04-0815.15-17.00FPClimate seminar 2 (Cezar Ionescu)EDIT 6128
16Mon 2024-04-1515.15-17.00FPClimate seminar 3EDIT 6128
17Mon 2024-04-2215.15-17.00FPClimate seminar 4EDIT 6128
18Mon 2024-04-2915.15-17.00FPClimate seminar 5 (Nicola Botta)EDIT 6128
19Mon 2024-05-0615.15-17.00FPClimate seminar 6EDIT 6128
20Mon 2024-05-1315.15-17.00FPClimate seminar 7EDIT 6128
21Mon 2024-05-2015.15-17.00FPClimate seminar 8 (Nicola Botta)EDIT 5128
22Mon 2024-05-2715.15-17.00FPClimate seminar 9EDIT 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.

Week 13:

FPClimate seminar 1

  • 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:
  • 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.

Week 14:

solve W13 exercises (FPClimate_seminar_1.pdf) and W15 preparation exercises (ref/seminar_2_exercises.pdf)

read and prepare questions for ”Vulnerability modelling …” paper

Week 15:

FPClimate seminar 2

Present and discuss solutions to exercises from the previous seminar

(after the seminar) solve W15 exercises

Week 16:

FPClimate seminar 3: Discussion about the current paper: Testing versus proving in climate impact research

  • Exercises: (informally: “re-implement the paper”)

Q1 (About definition 1): Consider the case

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?

Q2: Implement some of the Haskell code in section 3 to get a feeling for what can go wrong.

  • Q2a: Find counterexamples to sumList and to supList being vulnerability measures.
  • Q2b: Re-implement with Rational instead of Float. Are they correct now?

Q3: Implement (part of) the code for section 4

  • (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.

Week 17:

FPClimate seminar 4

Week 18:

FPClimate seminar 5

  • Lecture by Nicola Botta

Week 19:

FPClimate seminar 6

Week 20:

FPClimate seminar 7

Week 21:

FPClimate seminar 8

new exercises for S8 / paper 8

  • 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 favorite!]
  • 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.

Week 22:

FPClimate seminar 9

  • Lecture by Nicola Botta

Week 24:

FPClimate seminar 10 (wrap-up)

  • Thu 2024-06-13, 13:00-15:00, in room EDIT-5128

How to register

  • 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.

Other resources

  • TODO add links to talks, etc. online