al/pages
1
0
Fork 0
Code Issues 3 Pull requests Projects Releases Packages Wiki Activity Actions

fixed syntax highlighting, finally, I hope

Browse source
This commit is contained in:
Alexander 2025-06-16 22:00:54 -04:00
parent 808ebfdfa2
commit d568f6138a
3 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
acl.cool/site/draft/derive-appfun.dj
View file

@ -43,7 +43,7 @@ module FunctorOfMonad (M : Monad) :
end
```
Each of these accepts an instance of a less general structure and uses only the elements the module provides to implement an instance of the more general structure. The last one is boring, obviously, being just the composition of the former two.
Each of these accepts an instance of a less general structure and uses only the elements the module provides to implement an instance of the more general structure. The last one is boring, obviously, being just the composition of the former two, but those are a _little_ interesting.
It turns out that there are multiple ways to implement the derivation functors--- also multiple ways to implement a particular monad--- and they don't all behave the same. That makes it hard to predict whether the more-general, derived implementations are the "natural" ones that you expected to get without _ad hoc_ testing, which rather defeats the point of "gratis". On the other hand, the derivations here can be performed pretty mechanically, with little insight, by following the types in much the same way one might mechanically prove an easy proposition.