initial math, and other things

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "cSpell.words": [
+        "nelist"
+    ]
+}

acl.cool/site/css-sample.dj

@@ -48,3 +48,5 @@ There are ten books in Iain M. Banks' _Culture_ series, possibly the greatest co
 8. Matter
 9. Surface Detail
 10. The Hydrogen Sonata
+
+Math is something I'm still working on; in more ways than one. Something like $$`\forall x \in \mathbb{N}, x \in \mathbb{N}` is easy enough, but other things are harder.

acl.cool/site/draft/derive-appfun.dj

@@ -1,11 +1,12 @@
 # Functors and Applicatives, Gratis[^falsehood]
 
-It's usually possible to derive implementations of general structures from those of more specific ones, e.g. `Applicative` from `Monad` and `Functor` from `Applicative`. Here's how to do it, and and why not to.
+It's usually possible to derive implementations of general structures from those of more specific ones; here, `Applicative` from `Monad` and `Functor` from `Applicative`. This is how to do it, and why not to.
 
 ```ocaml
-module type Functor = sig
+module type Monad = sig
   type 'a t
-  val map : ('a -> 'b) -> 'a t -> 'b t
+  val return : 'a -> 'a t
+  val bind : ('a -> 'b t) -> 'a t -> 'b t
 end
 
 module type Applicative = sig
@@ -14,14 +15,13 @@ module type Applicative = sig
   val apply : ('a -> 'b) t -> 'a t -> 'b t
 end
 
-module type Monad = sig
+module type Functor = sig
   type 'a t
-  val return : 'a -> 'a t
-  val bind : ('a -> 'b t) -> 'a t -> 'b t
+  val map : ('a -> 'b) -> 'a t -> 'b t
 end
 ```
 
-Above, we have the usual OCaml signatures for functors, applicative functors, and monads respectively. The only thing of note is that I've written the functions in pipe-last[^pipe-last] style. It's more common to see pipe-first style, which agrees with the usual infix operators, but I don't see any of those around to get offended; do you?
+Above, we have the usual OCaml signatures for functors[^other-functor], applicative functors, and monads respectively. The only thing of note is that I've written the functions in pipe-last[^pipe-last] style. It's more common to see pipe-first style, which agrees with the usual infix operators, but I don't see any of those around to get offended; do you?
 
 ```ocaml
 module ApplicativeOfMonad (M : Monad) :
@@ -43,18 +43,63 @@ 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, but those are a _little_ interesting.
+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 somewhat more interesting. Looking at the implementation of `map` in terms of `pure` and `apply`, we can see that we have the function `f` put into an empty context and then applied to `x`. Since we can't know more about the particular applicative functor given, this is the only way to obtain a new instance of its backing type `('a -> 'b) t`, so there aren't any real options here in the way of implementation[^unique-functor]. Still, the meaning in terms of monads and/or effects is worth contemplating; applicatives tell us what application looks like in a context while monads do the same for composition[^makes-sense].
 
-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.
+The more involved implementation in `ApplicativeOfMonad` is where we get some options in terms of implementation and also, not unrelatedly, where our problems arise. Because it turns out that there are multiple ways to implement the derivation functor--- also multiple ways to implement a particular monad or applicative--- it becomes hard to predict whether a derived implementation is the expected one without resorting to _ad hoc_ testing, testing that rather defeats the point of "gratis"[^low-effort]. The `apply` function, shown above, is derived from `bind` and `return` by threading `x` and `f` into the context through bind (as `y` and `g`, respectively), thus "stripping off" the context in the body of the lambda, then applying `g` to `y` to obtain a fresh `'b`, and finally passing that `'b` to `M.return`, thus producing a `'b M.t`, which of course is also an `'a t`, since `type 'a t = 'a M.t`[^with-type].
 
-***
+To explore concretely how deriving instances can go wrong, consider the following `BarMonad.
 
-The modules above that seem to have parameters, do; these modules are called "functors". A functor in OCaml parlance is distinct from anything called a "functor" elsewhere, being essentially a function from modules to modules. For practical reasons, modules and value-level programs are stratified from one another in OCaml[^1ml], so a functor does not literally have a function type, but the mental model is still basically correct.
+```ocaml
+module BarMonad : Monad with type 'a t = 'a bar = struct
+  ...
+end
+```
 
-A subtlety of the OCaml module system is that if a module is defined with a particular `module type` a.k.a. signature attached, e.g. `module M : S = struct...`, all the types that are abstract in the signature `S` will _also_ be abstract in the module itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal. This is because both types are abstract, meaning the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above, `Functor with type 'a t = 'a M.t`--- for example--- exposes the equality of the two types, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_.
+This has the following derived `Applicative`.
+
+```ocaml
+derived app for bar monad
+```
+
+And then, here's a lawful[^legis] implementation of `Applicative` for `bar` which is _not_ the one produced by `ApplicativeOfMonad (BarMonad)`.
+
+```ocaml
+lawful other bar
+```
+
+Just to be sure, let's check that this new instance satisfies the required properties, i.e. that
+
+1. `apply (pure Fun.id) x`                          = `x`
+1. `apply (apply (apply (pure Fun.compose) f) g) x` = `apply f (apply g x)`
+1. `apply (pure f) (pure x)`                        = `pure (f x)`
+1. `apply f (pure x)`                               = `apply (pure (fun g -> g x)) f`
+
+for `BarApplicative'` just as for `ApplicativeOfMonad (BarMonad)`.
+
+{% these are identity, composition, homomorphism, and interchange %}
+
+Monads have their own laws of course, but while a lawful monad is guaranteed to entail a lawful applicative, as we can see, it isn't guaranteed to produce the _desired_ applicative when given as input to a particular derivation functor. The alternate definition above may or may not be a useful one, but the point is that the arbitrary nature of what applicative implementation is considered "correct"[^correct] means you don't `per se` get the applicative you want when deriving an instance; rather, you get the version that accords with the monad, which is _probably_ what you want, but perhaps not. The nice thing about OCaml here, as opposed to Haskell with its typeclasses, is that there's no barrier to having multiple implementation of the `Applicative` signature, so it's easy to implement a different instance without ambiguity. Furthermore, because `ApplicativeOfMonad` operates on a generic applicative and thus cannot make use of any peculiar structure in its argument, even a result that does behave as desired may be less performant in code than a decent handwritten version--- compare such implementations for *FooMonad*.
+
+```ocaml
+foo monad stuff
+```
+
+[^with-type]: In regards to the `with type = ...` syntax, there is a subtlety of the OCaml module system that if a module is defined with a particular `module type` (a.k.a. signature) attached--- for example, `module M : S = struct ...`--- all the types that are abstract in the signature `S` will _also_ be abstract in the module `M` itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal, because both types are abstract, i.e. the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above example, `Functor with type 'a t = 'a M.t` exposes the equality of `'a t` and `'a M.t`, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_, etc.
 
 [^falsehood]: Unsurprisingly, that's a lie. Isn't it always? You have to buy a monad first.
 
 [^1ml]: See [1ML](https://people.mpi-sws.org/~rossberg/1ml/1ml-jfp-draft.pdf) for an OCaml-like language without this stratification.
 
-[^pipe-last]: This idea is that to synergize with the automatic currying of OCaml, parameters to which a function is more likely to be "partially applied" should be earlier in the argument list. This cuts down on syntactic noise; particularly, pipes which apply to the _last_ argument (see?) don't require shuffling-about of the parameter order, e.g. `xs |> List.map f` rather than `xs |> (fun xs -> List.map xs f)`. JaneStreet will tell you that labels address the issue best, but to my eyes, `:` and `~` were never meant to stand that close to one another.
+[^pipe-last]: This idea is that to harmonize with OCaml's automatic currying, parameters to which a function is more likely to be "partially applied" should be earlier in its parameter list. This cuts down on syntactic noise; particularly, pipes which apply to the _last_ argument (see?) don't require shuffling-about of the parameter order, e.g. `xs |> List.map f` rather than `xs |> (fun xs -> List.map xs f)`. Jane Street will tell you that [labels](https://ocaml.org/docs/labels) can [address](https://opensource.janestreet.com/base/) the issue best, but to my eyes, `:` and `~` were never meant to spend so much time that close to one another.
+
+[^makes-sense]: It makes sense then, that having a monad nets you an applicative functor--- how can one talk about composition without having application first, which is needed to consider function-like objects at all?
+
+[^other-functor]: A functor, in OCaml parlance, is distinct from anything called a "functor" elsewhere, being essentially a function from modules to modules. This can indeed become confusing. For practical reasons, modules and value-level programs are stratified from one another in OCaml, so a functor does not literally have a function type, but to think of them that way is still basically correct. See [1ML](https://people.mpi-sws.org/~rossberg/1ml/1ml-jfp-draft.pdf) if interested in an OCaml-like language without such a stratification.
+
+[^low-effort]: On the other hand, the derivations here can usually be performed rather mechanically, with little insight, by following the types in much the same way one might mechanically infer a direct proof in sentential logic, making them fairly low-effort and so still possibly not a waste of time.
+
+[^correct]: Assuming, of course, that you admit some definition of correct as roughly "making sense in context" or "being broadly useful".
+
+[^legis]: There are [laws about these sorts of things](https://hackage.haskell.org/package/base-4.14.1.0/docs/Control-Applicative.html), you know.
+
+[^unique-functor]: This is true is a [precise sense](https://mail.haskell.org/pipermail/libraries/2011-February/015964.html).

acl.cool/site/index.html

@@ -6,4 +6,4 @@
 </h1>
 
 <div id="writings" style="color: var(--lighter-color); line-height: var(--ui-spacing);"></span>
-    <p><strong>Welcome! Below are links to things I've made or just enjoy.</strong></p>
+    <p style="color: var(--darkest-color)">Welcome! Below are links to things I've made or just enjoy.</p>

build.sh

@@ -1,6 +1,6 @@
 #! /usr/bin/env nix-shell
-#! nix-shell -i bash --pure
-#! nix-shell -p bash harfbuzz soupault woff2 jotdown python3 recode --pure
+#! nix-shell --pure -i bash
+#! nix-shell --pure -p nodejs_24 bash harfbuzz soupault woff2 jotdown python3 recode nodePackages_latest.katex
 
 if ! [[ -d pgvv/ ]]; then
     python3 -m venv pgvv

css/looks.css

@@ -173,3 +173,12 @@ hr {
   border: none;
   background-color: var(--narrow-gray);
 }
+
+math[display="block"] {
+  margin-top: 0.5em;
+  margin-bottom: 0.5em;
+  position: relative;
+  left: 0;
+  right: auto;
+  text-align: left;
+}

shared_templates/main.html

@@ -9,6 +9,7 @@
   <link rel="stylesheet" href="/css/looks.css">
   <link rel="stylesheet" href="/css/code.css">
   <link rel="icon" type="image/png" href="/assets/favicon.png">
+  <!-- <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.22/dist/katex.min.css" integrity="sha384-5TcZemv2l/9On385z///+d7MSYlvIEw9FuZTIdZ14vJLqWphw7e7ZPuOiCHJcFCP" crossorigin="anonymous"> -->
   <script>
     const class_ = `font-${window.devicePixelRatio >= 1.3 ? 'hidpi' : 'lodpi'}`;
     document.documentElement.className = class_;

soupault.toml

@@ -127,16 +127,19 @@ widget = "insert_html"
 html = '<meta name="generator" content="soupault">'
 selector = "head"
 
-# <blink> elements are evil, delete them all
-[widgets.no-blink]
-widget = "delete_element"
-selector = "blink"
-
-# By default this widget deletes all elements matching the selector,
-# but you can set this option to false to delete just the first one
-delete_all = true
-
 [widgets.syntax]
 widget = "preprocess_element"
 selector = 'pre code'
 command = "./syntax_wrapper.sh ${ATTR_CLASS##*-}"
+
+[widgets.math-inline]
+widget = "preprocess_element"
+selector = "span.math.inline"
+command = "sed -E 's/^\\\\\\((.*)\\\\\\)$/\\1/' | katex --format mathml"
+action = "replace_element"
+
+[widgets.math-display]
+widget = "preprocess_element"
+selector = "span.math.display"
+command = "sed -E 's/^\\\\\\[(.*)\\\\\\]$/\\1/' | katex -d --fleqn --format mathml"
+action = "replace_element"

syntax_wrapper.sh

@@ -1,7 +1,7 @@
 #! /usr/bin/env sh
 
 if [ $# -lt 1 ] || ! pygmentize -L lexers | grep -qw "$1"; then
-    recode ascii..html
+    recode utf8..html
 else
     pygmentize -l $1 -f html | head -c -13 | awk -F '<pre>' '{print $NF}'
 fi