I believe knowledge should be free & accessible. When I have the energy and time, I will contribute to putting more knowledge out there and sharing topics I am passionate about.
This blog will be more focused on programming and mathematics, while my more personal stuff will probably continue to live on my personal website: https://monoidmusician.github.io/.
I strive to be an open book, with minimal ego involved, just insight and connection. However, I am losing patience for putting energy into ephemeral instruction, so if you want to learn something serious from me directly, maybe we can collaborate on a short blog post instead of exchanging messages on social media where it will get lost quickly.
I would also like to share bits of how I customize my software experiences and navigate the tech world. If technology isnʼt working for the people, what is it doing? (Lining the pockets of capitalists and actively oppressing the working class, apparently. Sigh…)
Get the behind-the-scenes peek at the code and my account of the technologies that go into this blog.
Infodumping About Selective Applicative Functors 2024/04/10
selective applicative functors lie in between monads and applicatives in terms of their power, and show similarities with alternatives too
unfortunately, selective applicatives are tricky to formulate correctly, but the basic flavor is given by
selectandbranch:select :: m (Either u v) -> m (u -> v) -> m v branch :: m (Either x y) -> m (x -> z) -> m (y -> z) -> m zone way to think of it from a high level is that selective applicative functors let you have determined choice:
the computation itself gets to determine what branch to take, by whether it returns a
Leftor aRight
Pickling Tasty Data: The essence of runtime data (itʼs a graph!) 2024/01/28
I want to talk about data today. In particular, I want to talk about runtime representations of data, real data – data that can be mutable and referentially opaque at runtime – and demystify what they actually are in terms of more familiar notions of data.
You shouldnʼt just throw up your hands once you have cyclic references! Itʼs possible and worthwhile to design tools to work with the raw graph of runtime data, no matter its shape.
With the proper metaprogramming hooks, you could save and restore a whole runtime environment from the inside, which is pretty amazing to think about.
The main thing we will work up to (and go beyond) is Pythonʼs
picklemodule, including my own implementation of it for the Nasal scripting language (which I believe is cleaner in some respects, although obviously less industrial).
A Semiring From Any Semilattice: A mathematical pun? 2023/10/28
You can make a semiring out of a semilattice by adjoining a new zero element. Lifting the semilattice operation in the two obvious ways gives you
+and*. Idempotence gives distributivity(!).This construction answers the question, “if you need a semiring for static analysis, how do you also keep other data around that does not care about the branching structure?” (like, say, a monoid).
TransMorphism Type Theory MetaTheory 2023/10/13 – …
The Best Errors for Solving Dependency Versions 2023/01/02 – 2023/01/21
A novel algorithm for resolving dependency bounds to solved versions:
- Incorporates transitive dependency bounds for a breadth-first search:
- What dependencies are required no matter which package version in the range we commit to?
- Whatʼs the loosest bound for each dependency then?
- By taking this intuitive approach, we gain two things:
- Better errors, matching what users would expect.
- Efficiency too, if you could believe it.
- Implemented using semilattices (monoids).
Impossible Bézier Calligraphy: Approximating cubic nibs drawn along cubic strokes 2022/09/18 – 2023/04/23
Given a pen nib of some shape, what composite shape is produced when that pen is drawn along any particular path? If the inputs are cubic Bézier curves, is the output as well?
The catch? Itʼs mathematically impossible to model the output using cubic Bézier curves, as I determined after a bit of calculus. However, that doesnʼt prevent us from getting pretty darn close. Let me show you how it works out.
Interactive Parser Explanations 2022/07/20
I have been building this framework for explaining, analyzing, and teaching about LR(1) grammars for a couple months now. The interactive widgets here will allow you to build and verify your intuition by clicking through examples, because I believe that once you are armed with the basic ideas and the right intuition, you can figure out the rest of details for yourself. Alternatively, it can serve as a playground to test out hypotheses about grammars, see exactly where things go wrong when conflicts occur, and what to do to fix those errors.
Eudoxus Real Numbers as Slopes of Pixelated Graphs 2022/05/10 – 2022/07/20
This is a post on constructing real numbers without constructing rational numbers. Along the way the rationals will sort of be constructed, or at least heavily implied, but they donʼt directly figure into the definition! Instead all we need is functions from integers to integers.
The construction weʼll be talking about is my favorite esoteric construction of real numbers: the Eudoxus real numbers.
showNumber, or even use Towards an API for the Real Numbers.I post these for a few reasons. I donʼt really have the energy to write these things properly (and I am ever so ambitious in my goals). But if you want to nudge me to write on them – or even better, if you want to contribute in some way, even just chatting or pairing on it – Iʼd be willing to prioritize them.
Admittedly the “finished” posts are only 80–90% complete themselves, shhh…
Iʼve been thinking a lot about selective applicative functors lately. Mostly through the perspective of two contrasting applications: selective applicative parsers, and functors for typechecking with better errors.
The fun part of this work was how to interleave nested selectors.
My conclusion back then (2018) was that fully implementing :not() had edge cases that were not possible.
But it was written before the more advanced selectors like :has() became standard.
Relational operators versus algebraic operators
Infix, mixfix, distfix … but what about relfix?
I want a < b < c to stand for a < b && b < c!!
(And this to be an extensible system that users can add their own operators and precedences to.)
This is the main difference between how mathematicians (especially category theorists) treat and how programmers treat X -> Y -> Z, by the way.
The former means “two functions, which can be composed” and the latter means “a curried function of two arguments”.
I should do a blog post on what “effects” mean in FP culture
tl;dr is “effects are as effects do”
likeeee the real important point is itʼs all about what you leave implicit in your notation
itʼs about notation not semantics
in particular, this point about notation is necessary to explain why effects encompasses “pure effects” (like List, Either, Maybe, which are just data structures) and “real side effects” (like IO/Aff/Effect, of the “launch missiles” variety)
I suppose I need to pretend to recite the history of monads and do notation in Haskell (“programmable semicolon”)
and explaining why lists model “nondeterminism” could be a whole post of its own …
side-{effect, condition} really just mean “not explicitly tracked in the surface syntax”
I should also do a blog post on “what people get wrong about the lens/prism/optics laws”, thatʼll be simpler (if more tricky)
the main problem is that we donʼt have a good way to talk about them without invoking a metatheory of Haskell, with unification and possibly parametricity (Iʼll need to see if that comes up)
actually, maybe parametricity is “just” the answer, and we can extract a free law from the stated laws!
WIP: Why you should believe in HoTT Path Induction as a (Haskell) Programmer
Passive stability:
Imperative code has no passive stability: all global state is mutable, and small perturbations (say, modifying a prototype) can cause unpredictably large effects down the line, if not carefully managed. Untyped code is especially bad. Carefully managed imperative code may be stable, but this is active stability: it is not inherent to the framework but imposed on top.
Functional code on the other hand is not only passively stable, it is anchored down solid. Each building block is given a static, local denotation, and they compose together. You may still need nonlocal knowledge of the code to understand the intent of what everything represents (ahem, boolean blindness), but the local meaning is denotationally clear.
log levels considered harmful
data = informationbits & bytes + structureexpectations of what the bits & bytes can be and what they mean
Lebesgue measure and Lebesgue integration
My two observations:
Coercible