In functional programming, side effects are a common problem (dealing with the outside world). In math functions are often thought of as "pure". Elm is a programming language that handles side effects to make it seem like you're in a pure functional environment, shielding you from the impurities. Haskell handles side effects using monads (I don't have a lot of experience with Haskell).
- Side Effects in Elm (Intro documentation)
- Why are side-effects modeled as monads in Haskell? (StackOverflow)
- Understanding Side Effects in Elm (Reddit)
- https://github.com/CoqHott/coq-effects (I think this is Coq library for algebraic effects)
What I'm wondering is, a brief intro to the concept of side effects from an algebraic standpoint. Something that will allow one to understand:
- How things like errors/exceptions can be accounted for.
- How unknown changes to the external world's state can be accounted for. (Such as making a search query in the browser, it modifies all kinds of stuff).
So for example, say you have a function that returns a boolean value:
$$ f : X \rightarrow B $$
where $X = \{a, b, c\}$ and $B = \{1, 0\}$.
But say that the function makes an HTTP request and so it modifies the external world, wondering how that would be accounted for in the equation to make the function "pure" again. Wondering if it's just as simple as:
$$ f(w): X \rightarrow B $$
where $w$ is the external world.
Or maybe there is more to it so that it follows along with the material in the fields algebraic/computational effects.
Then the second case is handling errors. Maybe the function occasionally has an error. So wondering how that would be mathematically modeled according to this area of work.
$$ f(w) : X \rightarrow B \lor e $$
where $e \in E$ is an error/exception.
For someone with an interest in understanding Algebraic Effects / Monads, but with little or no prior experience, how to go about modeling them mathematically. Specifically, how to account for world state changes (known or unknown) and errors or unexpected behavior, using mathematical notation.
Reading a paper such as Computational lambda-calculus and monads (1988) is a bit over my head. Other papers such as Algebraic Effects for Functional Programming just jump straight into the programming source code and skip the math.
One place to start might be Plotkin and Pretnar's "A Logic for Algebraic Effects" [PDF]. More generally, you might be interested in perusing this bibliography.