# Course on functional languages and dependently typed languages

## Summary

The course consists of 11 regular lectures and 2 extra lectures. The regular lectures consist of three main parts:

1. an introduction motivating the use of formal methods from theoretical computer science in climate science,

2. an introduction to mathematical specification, functional and dependently typed programming, and computer-verified proofs,

3. an introduction to the Botta et al. framework for decision-making under uncertainty in the context of climate science, including an example application of the framework as in [2].

4. The extra lectures provide some theoretical background to the topics covered in the main lectures:

- an introduction to formal logic and the correspondence between proofs in constructive logic and programs in dependently typed programming languages,

- an introduction to the notions of functor and monad from the perspective of category theory.These play an important role in the Botta et al. framework.

Part 1 of the regular lectures and the two extra lectures are provided as presentation slides. Parts 2 and 3 of the regular lectures are included in this document as lecture notes, but they are also available as “literate” Idris [5] source code files which can be machine-checked (“type-checked”) and compiled, and from which the lecture notes can be generated automatically using the tool lhs2tex [6].

## Type-Checking

To use the Literate Idris files of the lectures, you need an installation of Idris 1 (the files are tested with version 1.3.2). For instructions on how to get started, see the [Idris tutorial](https://idris.readthedocs.io/en/latest/tutorial/starting.html).

Once Idris is up and running (and `idris` in your path),

- download IdrisLibs [3].

- enter `idris -i $IDRISLIBS --sourcepath $IDRISLIBS --build lectures.ipkg` to build the files

- or enter `idris -i $IDRISLIBS --sourcepath $IDRISLIBS --allow-capitalized-pattern-variables --checkpkg lectures.ipkg` to just type-check the files

- or type-check individual `.lidr` files and load them into the interactive Idris REPL (Read-Eal-Print-Loop) by typing

where `IDRISLIBS` is the path of `IdrisLibs` on your machine.

To remove the generated code, you can use

`idris --clean lectures.ipkg`.

## References

[1] Botta, N., Jansson, P., Ionescu, C. (2017). Contributions to a computational theory of policy advice and avoidability. J. Funct. Program., 27, e23.

[2] Botta, N., Jansson, P., Ionescu, C.(2018). The impact of uncertainty on optimal emission policies. Earth Syst. Dynam., 9, 525-542.

[3] Botta, N. et al.(2016-2021). IdrisLibs, https://gitlab.pik-potsdam.de/botta/IdrisLibs

[4] Botta, Nicola, Brede, Nuria, Crucifix, Michel, & Martı́nez Montero, Marina. (2020). Course on functional languages and dependently typed languages.

[Zenodo](https://doi.org/10.5281/zenodo.4543579).

[5] Brady,E. (2013). Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23(9):552–593.

[6] Löh, A., [lhs2texPreprocessor](https://github.com/kosmikus/lhs2tex)