Type systems in notes - stupid, or a stroke of genius? Without you having to read too much, it’s probably genius…
In computing, maths is used extensively in all sorts of domains for problem solving. The question is, can it solve our notes?
On the surface, this seems like a very silly question. “Of course not”, you may say, “maths is much too rigorous to represent something as fluid and unstructured as human thought”. Or maybe, just maybe, you might say: “maths with its notation is too complicated for the average person, and so any system that utilizes it is by extension complicated”.
In this series of blog posts I would like to explore several domains in which type theory (and perhaps some hints of category theory and lambda calculus) create very elegant, clean and easy-to-understand solutions to some rather complicated problems in our note taking experiences. What I would like to show is that, despite some scary looking notation, it’s possible to create underlying foundations which are pure and — frankly — beautiful.
Things Covered
I plan to explore several domains, including GTD, Zettelkasten and also builtin Norg syntax like links and inline link targets.
The goal is to understand what fundamentally makes many components of our notes tick, as well as how we can leverage these axioms to build out more complex and human-friendly workflows.
Links
- Link Integrity - Exploring type theory as a solution to complex note linking problems.