Richard Bird (1943-2022) (image from Wikipedia)
Ideas:
- 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.
At PIK researchers in the natural and social sciences work together to study global change and its impacts on ecological, economic and social systems. They examine the Earth system’s capacity for withstanding human interventions and devise strategies for a sustainable development of humankind and nature.
PIK research projects are interdisciplinary and undertaken by scientists from the following Research Domains: Earth System Analysis, Climate Impacts and Vulnerabilities, Sustainable Solutions and Transdisciplinary Concepts and Methods.
(PIK home page, cca 2010)
At PIK researchers in the natural and social sciences work together to study global change and its impacts on ecological, economic and social systems. They examine the Earth system’s capacity for withstanding human interventions and devise strategies for a sustainable development of humankind and nature.
PIK research projects are interdisciplinary and undertaken by scientists from the following Research Domains: Earth System Analysis, Climate Impacts and Vulnerabilities, Sustainable Solutions and Transdisciplinary Concepts and Methods.
(PIK home page, cca 2010)
A first attempt to apply the AoP ideas:
\ldots The complexity of the climate, ecological, social and economic systems that researchers are modelling means that the validity of scenario results will inevitably be subject to ongoing criticism.
\ldots What this criticism does, however, is emphasize the need for a strong foundation upon which scenarios (\emph{i.e., modelling}) can be applied, a foundation that provides a basis for managing risk despite uncertainties associated with future climate changes.
\emph{This foundation lies in the concept of vulnerability.}
(from “Climate Change Impacts and Adaptation: A Canadian Perspective”, 2004)
The paper was drafted for DTP10 Dependently-Typed Programming, Edinburgh.
The first version was submitted in December 2010, the final version was published online in …December 2014, and the paper journal version came out January 2016.
- UNDP Annual Report, 2004:
\ldots a human condition or process resulting from physical, social and environmental factors which determine the likelihood and damage from the impact of a given hazard
- Cannon et al. 2004
Vulnerability [\ldots] is a way of conceptualizing what may happen to an identifiable population under conditions of particular risk and hazards.
- The Intergovernmental Panel on Climate Change, 1995
\emph{vulnerability}: the extent to which climate change may damage or harm a system.”
- Institute for Environment and Security (United Nations University),
2004
Vulnerability is the intrinsic and dynamic feature of an element at risk (community, region, state, infrastructure, environment, etc.) that determines the expected damage or harm resulting from a given hazardous event, and is often affected by the harmful event itself. Vulnerability changes continuously over time and is driven by physical, social, economic and environmental factors.
\ldots many, many others (Thywissen 2006 lists 32 more)
vulnerable (adj.):
- exposed to the possibility of being attacked or harmed, either physically or emotionally: we were in a vulnerable position | small fish are *vulnerable* to predators
- Bridge (of a partnership) liable to higher penalties, either by convention or through having won one game towards a rubber.
(Oxford Dictionary of English, 2010)
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 . possibleCalvo and Dercon (2005):
\begin{itemize} \item Vulnerability measures a set of outcomes across possible states of the world. These states of the world are assumed to be in finite number and come with associated probabilities. \item Poverty is defined in terms of a threshold, which has the same value in all states of the world. \item The states of the world in which the outcomes are above the threshold do not enter in the vulnerability measurement (this is called the “axiom of focus”). \item Monotonicity requirements: the likelier the outcomes below the threshold, and the greater their distance to the threshold, the greater the vulnerability. \end{itemize}
> V = sum [p i * v (x i) | i <- [1 .. n]]
where
> n :: Nat -- the number of possible states of the world
> p :: Nat -> [0, 1] -- p i is the probability of state i
> v :: Real -> Real -- a monotonically decreasing and convex function
> x i = (y i) / z -- relative distance to threshold of outcome i
> y :: Nat -> Real -- y i is the outcome in state i if below the
> -- threshold, 0 otherwise
> z :: Real -- the thresholdExercise: Does this fit the structure of vulnerability? How / why not?
“Small fish are vulnerable to predators.”
possible :: State -> [Evolution]
predators :: Evolution -> Bool
wounded :: Evolution -> Bool
harm :: Evolution -> Bool
harm = wounded ∧ predators- Vulnerability is here a predicate on states (transferred epithtet)
- Factors of interest (predators) and impacts to assess (wounded) play a symmetric role
Vulnerability measures should be “monotonous”. If every harm value in the structure increases, the structure remaining the same, then the aggregated value should also increase (“increasing” is non-strict).
For all inc : V -> V increasing (inc v ⊒ v), we have for all v ∈
F V
measure (fmap inc v) ⊒ measure v“Most common harm value” does not fulfil this condition!
E.g., [1, 2, 3, 10, 10] worse than [4, 4, 4, 11, 11]!
- natural transformation between representations of possibility
τ :: F1 a -> F2 a
- vulnerability measures of the “same kind”
m1 :: F1 V -> W m2 :: F2 V -> W
- compatibility w.r.t.
τm1 v1 ⊒ m1 v2 ⇒ m2 (τ v1) ⊒ m2 (τ v2)
- reuse:
m2 . τis compatible withm2
Exercise: What are the “minimal” categories involved?
Enter dependent types (under the influence of Patrik Jansson).
We started moving the categorical machinery to the new framework, leading to many developments (see the rest of the FPClimate papers).
There is still a certain “friction” between categorical frameworks and the depedently typed ones which have largely superseded them, as illustrated by Richard Bird’s last book (together with Jeremy Gibbons).
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.
Meta-exercise: find and correct all the errors in the article.