-
-
Save awonnacott/483fadf59abdbf5e51bd75c5b86347a7 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
the following is my preferred defintion of monad | |
a monad M requires the following three functions, along with their names (programmers, mathematicians): | |
a -> M a ("singleton" or "unit") | |
M M a -> M a ("flatten" or "multiplication") | |
(a -> b) -> (M a -> M b) ("map", no name its deifnition is given by the definition of unit) | |
such that, where m : M a and mmm : M M M a: | |
flatten (map singleton m) = m = flatten (singleton m) | |
flatten (flatten mmm) = flatten (map flatten mmm) | |
and calling them map, flatten, and singleton makes it easy to see how a lot of data structures are monads | |
the following is my preferred defintion of comonad, for you to read at the same time | |
a comonad W (becuase W is an upside down M) requires the following three functions, along with their names: | |
M a -> a ("extract") | |
M M a -> M a ("duplicate") | |
(a -> b) -> (M a -> M b) ("map", no name its deifnition is given by the definition of extract) | |
such that, where w : W a: | |
extract (map duplicate w) = w = extract (duplicate m) | |
duplicate (duplicate w) = duplicate (map duplicate w) | |
and you can see how | |
-in the defintiions, all the arrows point the other way | |
-in the axioms, the corresponding words were filled in, and then the order of the functions was flipped |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment