umbral 5 init

This commit is contained in:
Alexander 2025-08-16 09:52:26 -04:00
parent 6808af8471
commit b48dc428ee
10 changed files with 235 additions and 7 deletions

View file

@ -43,7 +43,7 @@ module FunctorOfMonad (M : Monad) :
end
```
Each of these functors accepts an instance of a less general structure and uses only the elements that module provides to implement an instance of the more general structure. `FunctorOfMonad` is boring, being just the composition of the others, but those themselves are a bit neat. Looking at the implementation of `map` in terms of `pure` and `apply`, you can see that we have the function `f` put into an empty context and then applied to `x`. Since there's no information about the given functor other than that it _is_ a functor, this implementation is the only way to obtain a new instance of the applicative's backing type `('a -> 'b) t`; there aren't any real options here in the way of implementation[^unique-functor]. The meaning in terms of monads and/or effects is still worth contemplating, though: applicatives tell us what application looks like in a context while monads do the same for composition[^makes-sense].
Each of these functors accepts an instance of a less general structure and uses only the elements that module provides to produce an instance of a more general structure. `FunctorOfMonad` is boring, being just the composition of the others, but those themselves are a bit neat. Looking at the implementation of `map` in terms of `pure` and `apply`, you can see that we have the function `f` put into an empty context and then applied to `x`. Since there's no information about the given functor other than that it _is_ a functor, this implementation is the only way to obtain a new instance of the applicative's backing type `('a -> 'b) t`; there aren't any real options here in the way of implementation[^unique-functor]. The meaning in terms of monads and/or effects is still worth contemplating, though: applicatives tell us what application looks like in a context while monads do the same for composition[^makes-sense].
The more involved implementation in `ApplicativeOfMonad` is where we get some options in terms of implementation and also, not unrelatedly, where potential problems crop up. Because it turns out that there are multiple ways to implement `ApplicativeOfMonad`--- also multiple ways to implement a particular monad or applicative--- it becomes hard to predict whether a derived implementation matches the expected implementation without resorting to _ad hoc_ testing, which would sort of defeat the point of deriving implementations (i.e. less work).