Contents

### Context

#### Computation

intuitionistic mathematics

### Computability

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

# Contents

## Idea

In purely functional programming languages (such as Haskell) all would-be side effects are data typed in terms of monads in computer science which make the side effects look like and hence be formally treated like verifiable deterministic pure functions. If the actual side effect operations of reading input from or writing output to actual physical devices is typed in this monadic way, one speaks of an I/O-monad.

So to the programming language an IO-monad looks just like a state monad or similar, but when run on an actual computer the bind operation does cause actual physical effects.