Owen Lynch

Grad student at Oxford, Research Software Engineer at the Topos Institute.

Currently working on the programming language side of systems theory.

Trump is a fascist, fascists are bad.

Public Key

npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07

NIP-05 Address

olynch@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqsvfzz0lzddzjlvhtwz4q3xxtmzvu2cm0vxu663m5wjrxh80ag7nxspz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsy03dzg

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07

Show more details

Last Notes

2026-06-18 08:22:26 UTC

Someone needs to start a grant program for algebraic geometry and call it the fellowship of the ring.

2026-05-22 14:42:49 UTC

I'm trying to stick to my "ask mastodon rather than chatgpt" habit: does anyone have recommendations for interesting places to visit in Paris?

2026-02-11 11:20:03 UTC

- reply

@nprofile…xuzd Like, the problem in ITT is that the identity type is being given two universal properties: the universal property of the Jdentity, and the universal property of the singleton. It's not clear to me that these can be reconciled, because they imply different definitions for eval/reify/reflect.

2026-02-11 11:08:58 UTC

- reply

@nprofile…xuzd The way that I would imagine this working is that glue(p,q) computes to refl as soon as p and q are definitionally equal, and any proof of p = q eta-expands to glue(p,q). It does seem a bit dodgy though... I'm not sure I believe your "if it works in OTT it works in ITT" statement. The nice thing about OTT is that refl would compute to glue(p,p), and then we never look at it after that.

2026-02-08 22:28:57 UTC

- reply

@nprofile…xuzd Glad it was helpful!

2026-02-08 21:58:05 UTC

- reply

@nprofile…xuzd Ah, OK, I didn't realize that. I think my concept would more accurately be called structural isomorphism then.

2026-02-08 15:49:49 UTC

I just wrote up a brief account of my (probably shaky) understanding of what Narya is doing with "canonical types" -- might be interesting to other people who are writing elaborators and are interested in Narya's strategy. I'd also like to know if this strategy is original to Narya; I haven't seen it anywhere else but I'm fairly new to this game so perhaps it appears in another guise elsewhere.
https://owenlynch.org/blog/nominal-types-via-energies

2026-02-07 14:05:31 UTC

- reply

@nprofile…xuzd @nprofile…qgyt told me about the relative positioning trick for what he calls "60fps typechecking". Might be worth talking to him a bit about incremental architecture for proof assistants.

2026-02-03 17:11:06 UTC

- reply

@nprofile…xuzd many such cases

2026-01-28 10:49:49 UTC

- reply

@nprofile…xuzd oh yeah, I was thinking about the name for the concept, not the syntax. For the syntax, what about `↑a`?

2026-01-28 08:35:10 UTC

- reply

@nprofile…xuzd I'm not sure how applicable this is to Pterodactyl, but in my most recent implementation of this I did something like a "phase distinction" for singletons. E.g., each type has an underlying "unrefined type" and then in the mode shift, we check that the unrefined types are convertable, and then that the synthesized element is in fact an element of the expected type (which uses the refinements/singletons).
Checking that A <: B is then achieved by creating a neutral of type A, eta-expanding it (and eta-expansion for singletons resolves to the value that the singleton is at), and then checking whether it was an element of type B.
Maybe this treatment of singletons only worked in my setup though, I'm not sure (I wasn't implementing MLTT).

2026-01-28 07:58:40 UTC

- reply

@nprofile…xuzd As far as I can tell, there are two types of subtyping involved here: one is subtyping between theories, and the other is singleton subtyping. Is cast required for both kinds? E.g., if we have X : Monoid, do we also have X : { Monoid | car = X.car }? Or do we need an explicit cast there?

2026-01-26 20:53:25 UTC

- reply

@nprofile…t6k2 But most types are given universal properties precisely by reflection. Terms of sigma types are in bijective correspondence with dependent pairs of terms. If we are working in an LF, terms of pi types are in bijective correspondence with meta functions!
Introducing equality reflection as a rule in MLTT in order to make extensional type theory, if MLTT is specified as something sensible like a GAT or SOGAT, seems like a perfectly reasonable thing to do! We're already quotienting the syntax by eta and beta for all the rest of the type formers, why not equality too?

2026-01-26 13:33:27 UTC

My video on teaching @nprofile…e8e7 how to elaborate the simply typed lambda calculus is up! https://www.youtube.com/watch?v=uBjuFDs-shw&list=PLhgq-BqyZ7i5C6ZnaYiGDhiGZuvvtLh5o&index=9

2026-01-25 19:04:32 UTC

I just learned that there was a brief point in time where people referred to "typescripts" (drafts which had been *typed* rather than handwritten), until I suppose everyone typed everything, so it would no longer be confusing to have a non-handwritten manuscript! Funny bit of English on a Sunday for you all!

2026-01-19 14:06:30 UTC

- reply

@nprofile…xuzd I can always \def\smiley{\verb|:)|}, so it's all good :)

2026-01-19 13:08:08 UTC

Smh @nprofile…xuzd forester complains about my text-based emoticons because they aren't balanced parentheses.

2026-01-19 07:48:28 UTC

- reply

@nprofile…sqfw 🤯🤯🤯 it makes sense

2026-01-18 14:54:24 UTC

- reply

@nprofile…sqfw :O What does this mean?

2026-01-14 07:38:24 UTC

- reply

(This slide is from https://tdejong.com/mhe60/slides/buchholtz.pdf)

2026-01-14 07:38:01 UTC

People who are in this picture or want to be should come find me at POPL (Geometric Type Theory).
https://media.mathstodon.xyz/media_attachments/files/115/892/306/682/803/227/original/eb1882d6bd4499e9.png

2025-12-29 19:08:39 UTC

- reply

@nprofile…rrqe These are all good points.
I think the real question for me is how this effects my term/type *syntax*. E.g. now that (concrete syntax identifiers) can refer either to an element of a type or a proper judgment, should I have two mutually recursive syntax trees that I elaborate into or just one? And should syn/chk return a sum type between them?
Perhaps they really should be distinguished in the concrete syntax for clarity...

2025-12-28 22:49:00 UTC

- reply

@nprofile…rrqe Well, I think of "closure" as a description of an implementation technique, not really as a semantic object. It is a closure, but there are plenty of other things that are also closures.

2025-12-28 20:40:22 UTC

- reply

@nprofile…rrqe Yeah, I generally work in a 4 type setup:
term syntax
type syntax
term value
type value
So it seems like your proposal is the second of my two options, where I extend term syntax to be "the syntax of perhaps-not-fully-substituted term judgments" and analogous for the rest.
Just to make it clear what I mean by this, if I have
```
def f (x : Int) (y : Int) : Int = x + y
```
and I don't have pi types, then `f x` would be a "perhaps-not-fully substituted term judgment". Is there a better word for that?

2025-12-28 20:27:35 UTC

I'm implementing a type theory where the top-level bindings are *judgments* in the theory, rather than closed forms (this is important because I only have a restricted pi type). This means that evaluating an identifier (in the context of nbe) doesn't necessarily produce a "value" in the traditional sense. So I have two options:
1. Have eval return a sum type of (closed value, judgment)
2. Extend my type of values to include these "non-values".
Has anyone else run into this kind of problem before? Do people have recommendations for solutions?

2025-12-14 19:19:25 UTC

- reply

@nprofile…dand @nprofile…rrqe 100% agree with this, having the goal disappear is so frustrating.

2025-12-03 17:40:51 UTC

- reply

@nprofile…rrqe OK you win, yes.
I rephrase my earlier point as "ITT (with or without K) is intimately connected with the idea of weak equivalence, whether or not you care about shapes."

2025-12-03 14:26:55 UTC

- reply

@nprofile…rrqe Well for Lean it is the homotopy category which is relevant, because what looks like a pullback in Lean syntax is only semantically a pullback in the homotopy category.

2025-12-03 14:03:28 UTC

- reply

@nprofile…rrqe OK, good point, what I really mean to say is that a 1-categorical model has a (something like) a model category structure, and the homotopy category of this is highly relevant to understanding the semantics.

2025-12-03 13:57:41 UTC

- reply

@nprofile…rrqe But like, if you wanted to do a proper semantics for *Lean* you need this...

2025-12-03 11:02:42 UTC

Man, I wish that people made the pitch for (infinity,1)-category theory in the following way.
1. It's good to have a notion of model for type theory which encompasses the syntactic model.
2. We need to use intensional equality types in dependent type theory in order for elaboration to be computable.
3. 1-categorical models of dependent type theory don't make enough of a distinction between propositional/judgmental equality for the initial model to represent faithfully the syntactic model.
The fact that you can compute homotopy groups of spheres synthetically is a fun little side benefit, but you're forced into this *even if you don't want univalence* just to have the proper model theory for intensional equality types.
I was so frustrated for so long: "Why does everyone keep going to infinity? Can't we just do normal math??" Ah well.

2025-12-01 17:19:33 UTC

- reply

@nprofile…rrqe This gets back at my original point, when we say "homotopy pullback" it implies something fancy, when what we really mean is "pullback, but in the way that we care about, not subject to accidents of syntax." And it scares computer scientists, but it shouldn't; it's just "the normal set-theoretic definition of pullback, but in the internal language using an equality type."

2025-12-01 15:03:41 UTC

- reply

@nprofile…rrqe Fair... perhaps propositional equality is a bad term because equality is often not hpropositional either! What's a better name?

2025-12-01 14:17:52 UTC

Categorical semantics for homotopy type theory would be 500% less confusing if the word "homotopy" was replaced with "propositional." E.g., a propositional monomorphism is a morphism for which one has a proposition in the language saying that it's a monomorphism. I'm turned off by the idea that when I write a happy little elaborator someone makes me think about algebraic topology, but I like it when categorical models capture faithfully real world issues like the distinction between propositional and definitional equality.

2025-12-01 10:25:13 UTC

There's a succession of different categorical structures that correspond to larger and larger fragments of first-order logic:
- finite limit
- regular
- extensive
- topos (geometric logic)
We can think about a finite limit category as a clan (e.g. a model of dependent type theory with sigma types) where we have added extensional equality types.
If we instead add intensional equality types, we get to tribes. Thus, perhaps it makes sense to think about tribes as "intensional finite limit categories." Is there any work on moving up this hierarchy? That is, obviously people study adding pi types and fancy stuff to tribes, but is there a notion of a regular tribe? My guess is that a regular tribe interprets hProp-truncation, but I don't know what to think about further than that.

2025-11-30 21:07:41 UTC

I have an economics puzzle; are there any people who know economics on this site?
Suppose that there are two farming countries, A-stan and B-topia which both produce carrots. 20 years ago, transport between A-stan and B-topia was expensive, but now it has become cheap. This is causing a problem, because there are unpredictable climate cycles which make A-stan carrots far cheaper than B-topia carrots for decade-long stretches, and vice versa. Before cheap transportation, A-stan simply had more expensive carrots in some decades, and similarly for B-topia. However, now with cheap transportation, when A-stan carrots are cheaper, it is totally unprofitable to produce carrots in B-topia, and vice-versa. Consequently, any B-topia carrot farmer will be completely wiped out in the "B-topia lean years", and similarly for A-stan carrot farmers in the "A-stan lean years."
It seems like what would happen absent regulation/some kind of intervention here is the following. Suppose that when transportation becomes cheap, A-stan has favorable weather conditions. Then the B-topia carrot industry *collapses* over the next decade, taking with it generational knowledge, farms that have been in families for centuries get sold off to banks, etc.. The point is, stuff that has taken a long while to build up is totally wiped out. But then, another decade later, the climate changes back and now both A-stan and B-topia must have expensive carrots; clearly suboptimal, and also quite unfair!
I actually have a good amount of respect for neoliberalism/free trade, and I think "creative destruction" is important; what would a neoliberal solution to this look like?

2025-11-25 14:19:00 UTC

- reply

@nprofile…rrqe Consider the following geometric theory (if you will permit a made-up LF-style syntax for geometric theories which makes it slightly more convenient to talk about axiom schemas which involve base types)
X : Set
R : X -> X -> Nat -> Prop
_ : (x x' : X) -> ∃(n : Nat). (R x x' n)
_ : (n n' : Nat) -> (x x' : X) -> (n != n') -> (R x x' n) -> (R x x' n') -> ⊥
This is the theory of a binary function to the naturals.
Now, consider two models M1 and M2 and assume that M is the coproduct, with i1 : M1 -> M, i2 : M2 -> M the injections. Then (M.R (i1 x1) (i2 x2) n) must be true for precisely one n, for every (x2 : M1.X), (x2 : M2.X). However, for any n, there is a models N with injections j1 : M1 -> N, j2 : M2 -> N where (N.R (j1 x1) (j2 x2) n) is true, and thus there cannot exist a morphism M -> N. QED

2025-11-25 12:29:13 UTC

- reply

@nprofile…rrqe @nprofile…dg4r Man, I love topos theory. So complicated, but so many tools for figuring things out too! You can just work out an "introductory model theory-level" argument for why models of a geometric theory in "Set" aren't closed under coproduct, and that tells you something about crazy synthetic stuff.

2025-11-25 12:17:50 UTC

- reply

@nprofile…rrqe @nprofile…dg4r Thanks so much! I was having a good time showing that the go categories don't have products by hand, but this is much more efficient:)

2025-11-25 11:33:32 UTC

Reference request: what is the "best" category that Top (the category of topoi and geometric morphisms) is enriched in. Obviously it's enriched in Cat, but is it enriched in finite limit categories? Colimit categories?

2025-11-24 18:18:36 UTC

- reply

@nprofile…rrqe @nprofile…99up OK, this makes sense. Ah well.

2025-11-24 17:58:33 UTC

- reply

@nprofile…rrqe @nprofile…99up Actually, now that I think of it, there's no reason to have a separate universe of strict propositions in this setup; the closed modality can just serve as a "strict truncation" operator.
Perhaps this would address the concern about forcing people to make agonizing decisions by unifying the landscape of propositions a bit better?

2025-11-24 17:49:41 UTC

- reply

@nprofile…rrqe Not very useful for mathematics for the reason I mentioned that you would still have to have 1/x defined for x = 0?
I do think that @nprofile…99up's point that mainstream mathematicians really want proof irrelevance is a good one, but perhaps the answer is to teach them that they shouldn't want things they can't have...
Here's an idea to fix the above issue. What if we do something like postulate a neutral
inv : (x : R) -> (y : R) × (p : x ≠ 0) -> (y = 1/(x,p))
where 1/- : (x : R) × (x ≠ 0) -> R is the "normal" definition of inverse.
Then this serve as the "base function" for the refined inverse. Perhaps suitable elaborator support can make moving between two definitions (the definition which takes in the proof as a refinement and the real definition) smooth.

2025-11-24 17:17:11 UTC

@nprofile…rrqe Here's a thought for definitionally irrelevant propositions which have good support for unification: use a phase distinction!
Specifically, there is a phase distinction for refinement types whose open modality erases the refinement. If the typing judgment is "open-modal" with respect to this, then during conversion checking anything that is purely closed-modal can be treated as a singleton.
Then, you can have a universe of propositions SProp for which El P is always closed-modal and so definitional proof-irrelevance for El P doesn't mess with unification at all.
The problem, of course, is that (following up from a recent toot) a function
(1/-) : { x : R | x != 0 } -> R
must in fact be defined on all of R in the base type theory... So this doesn't do everything that one might wish for from strict propositions, but perhaps this is still an improvement.
I think the trick would be to figure out the right interaction between SProp and Prop; I will think about this a bit but perhaps you already have some ideas.

2025-11-09 12:37:03 UTC

- reply

@nprofile…ral2 What do you mean by "accidentally isomorphic"?

2025-11-08 20:49:54 UTC

This whole "we need higher morphisms so that path composition can be associative" seems *so* complicated compared to just taking a category enriched in presheaves on the discrete category on the reals, with Day convolution corresponding to addition.
Or, in plainer English, "have a notion of r-morphism for each r, and then an r-morphism and an s-morphism compose to form an (r+s)-morphism." If the r-morphisms from x to y are maps [0,r] -> X, then this gives a strict composition.
If you want to be fancier, you could enrich in presheaves on the category where the objects are real numbers, and a morphism from r to s is a continuous map [0,r] -> [0,s].
In fact, we could have a whole "weighted cubical set" of higher paths, where we considered r_1,...,r_n-cubes. You could compose strictly along cube faces no problem, no higher associativities needed!
Does anyone take this approach to infinity category in practice? Perhaps it doesn't actually buy you that much.

2025-11-07 17:40:58 UTC

- reply

@nprofile…ral2 @nprofile…rrqe A very precise approach to this is https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf

2025-11-06 15:56:07 UTC

- reply

@nprofile…ral2 What can I say, potato chips and chocolate milk really hit the spot sometimes :)

2025-11-06 14:07:09 UTC

- reply

@nprofile…rrqe I think the real question is whether a language supports a rigid, predictable indentation that increases by precisely one unit per nesting level, or whether it expects you to align things in a way that depends on the length of your variable names.
Spaces are evil for enabling the latter form of indentation-sensitive languages (like Haskell...), but I don't think are so bad in and of themselves.

2025-11-06 14:02:55 UTC

- reply

@nprofile…ral2 OK but for real I lowkey love meal deals.

2025-11-05 17:03:53 UTC

- reply

@nprofile…ral2 (for the curious: https://owenlynch.org/archive/2025-aria-ta1-seminar/1.html)

2025-11-02 13:16:07 UTC

- reply

@nprofile…rrqe In fast fourier transforms, you often round up the dimension of your vector to the nearest exact multiple of 2s and 3s so that divide and conquer works out :P

2025-11-01 15:30:02 UTC

How do typeclasses interact with univalence? It seems like the point of typeclasses is to distinguish between isomorphic types, as we might want to put different structures on such types. But this contradicts univalence; is this bad?

2025-10-28 10:30:30 UTC

- reply

@nprofile…ral2 Oh damn ur right. This is crazy.

2025-10-28 07:34:18 UTC

- reply

@nprofile…ral2 Lol, where did you even come up with this?

2025-10-28 06:56:18 UTC

- reply

@nprofile…ral2 Whaaat is this true?? How?

2025-10-19 21:38:20 UTC

- reply

@nprofile…rrqe I think that I'm finally discovering that classic style, whereas when I was programming Haskell years ago I was trying to do the fanciest trendiest stuff.
And I now know that *products* are so much work and I want to make *prototypes* at this time in my career, and I can relax on my code being "production-ready" as a result.

2025-10-19 21:08:10 UTC

- reply

@nprofile…rrqe @nprofile…2elt All makes sense; I think Haskell definitely is overrated for being "safe", especially when you see the kind of crap people pull *all the time* in order to get better performance.
I feel you on the upper bounds update; I was once assigned a ticket at an internship to make Semigroup instances for everything that was previously just a monoid so we could upgrade to ghc 8. Good times...

2025-10-19 20:48:58 UTC

- reply

@nprofile…rrqe @nprofile…2elt Yeah, makes sense to me. Out of curiousity, what made you switch away from Haskell to OCaml all those years ago?

2025-10-19 20:27:51 UTC

- reply

@nprofile…rrqe @nprofile…2elt Ooof. Are you still implementing Pterodactyl in Lean or have you moved to Swift?

2025-10-19 20:26:55 UTC

- reply

@nprofile…rrqe Yeah at first I thought the Lean lsp was so cool and slick, but then over time I grew to prefer the agda-mode in emacs, with its manual control over reloading.
Of course, it's a lot more work to go outside of the lsp model, and sadly vscode support is probably important for pterodactyl because you don't want to waste a class every semester teaching students how to install emacs...
I feel like the ideal experience would be a clutch pedal: you hold it down while you are making an edit and the lsp takes a chill pill, and then you release it when you are done and you get up to date semantic information.
I do think that continual semantic highlighting is nice, just I don't want the squiggly underlines causing me stress.

2025-10-19 20:21:31 UTC

- reply

@nprofile…2elt @nprofile…rrqe Yeah, this kind of thing is exactly my experience too; I hate having to second guess "is this error from my code, or is LSP just messing up" and *sometimes it is just LSP* which is really an extra level of mental effort that I don't want to have to worry about on a day-to-day basis.

2025-10-19 20:15:56 UTC

- reply

@nprofile…rrqe Well, first of all the parser for the lsp isn't resilient and it shows.
But secondly, I think I really prefer having control over when my code is checked for errors. The "show me syntax error on every keypress" is a cool gimmick that wears thin eventually.
In emacs, you can reload the ghci window with C-x C-l which is really nice, and then you can actually *play* with the definitions you just made! And it also will bring the errors from ghci in as red squiggles in the editor, so that's pretty convenient.
I think that 90% of the functionality of an lsp for me is in the context-aware autocomplete, e.g. when writing rust I want to just yolo autocomplete a method name based on my intuition about what it should be called. Oh and case splitting and renaming is nice, and hover type for local variables too. But renaming in the Haskell lsp is kind of buggy, case splitting doesn't work, and of course Haskell doesn't have methods. And `:t` works just fine for 90% of my "what type is this" query. It's even better because the type *stays up* when I keep typing rather than being in a little hover bubble that goes away. So overall the lsp isn't worth it, especially considering how often it hangs, which isn't *too* often but enough to annoy me.

2025-10-19 20:07:41 UTC

I got annoyed at the Haskell lsp, went back to using ghci, and then discovered that the regular old haskell-mode integration with ghci is an infinitely better experience for me than lsp ever was.

2025-10-19 12:49:51 UTC

- reply

@nprofile…rrqe Have you read The Once and Future King?

2025-10-19 11:23:53 UTC

- reply

@nprofile…rrqe @nprofile…yytj @nprofile…9t3n Are you just going to put that out there and then not tell us what that aspect is??

2025-10-19 06:17:34 UTC

@nprofile…yytj Why does SmallTT only support up to 64 local variables?

2025-10-15 18:10:42 UTC

- reply

@nprofile…rrqe @nprofile…yqfl @nprofile…dand My beef with the lambda cube (not sure if this is a similar beef) is that it puts an overly strong emphasis on being able to quantify over various things in *closed terms*, and thus misses that *judgments* (terms in a context) are the central object of study in type theory, and additionally the right model for the top-level bindings in a language. E.g. you can have top-level functions without having function types, and you can have top-level generic functions without having forall types. It took me a while to realize this.

2025-10-13 15:59:16 UTC

- reply

@nprofile…v2av I'm super glad that this is the same category as https://arxiv.org/abs/2005.05284; I was worried that I would have to learn a new category :P

2025-10-12 10:29:09 UTC

- reply

@nprofile…v2av @nprofile…62n0 @nprofile…ggyq This is kind of how internal categories in 1lab work: https://1lab.dev/Cat.Internal.Base.html

2025-10-03 10:28:59 UTC

- reply

@nprofile…6kk0 Wow, maybe swift is wolf number 3 in https://mathstodon.xyz/@olynch/115031755258791123

2025-10-02 19:02:07 UTC

- reply

@nprofile…6kk0 OK, this was roughly my understanding so I'm glad I wasn't missing something.
By the way, this all reminds me of @nprofile…uzsf's Coda project, which sadly got more or less abandoned. https://github.com/ekmett/coda/. The way he explained it to me was roughly that typeclasses should be a poset along with a (not necessarily injective) functor to the category of module signatures and functors between them. Adding new ways of deriving typeclasses from other type classes involves also proving as a side condition that any introduced diamonds are trivial.

2025-10-02 00:30:36 UTC

- reply

@nprofile…6kk0 By the way, is there a concise way of explaining the difference between locales and a module system? My understanding is that locales support a poset of implicit conversions, and also support extension; is there some way of understanding locales that makes these obvious features rather than just a grab bag of addons to a module system?

2025-10-01 15:56:25 UTC

- reply

@nprofile…6kk0 My personal research agenda right now is "ML module systems are great, ML module systems can be thought of as 'module systems for the cartesian closed doctrine', what happens if we look at module systems for other doctrines of categorical algebra???"
The three question marks indicate the missing step 2 between
1. Look at module systems for other doctrines.
2. ???
3. Profit.

2025-10-01 15:52:37 UTC

- reply

@nprofile…6kk0 In the sense that algebraic julia was version 0.1 of "software implementation of DSLs that have denotational semantics given by categorical systems theory/categorical algebra", then you could view catcolab as a version 0.2, and in the sense that principled means "report all errors during elaboration so that the user never sees a host-language stack trace", then yes, catcolab is principled.

2025-10-01 15:47:13 UTC

- reply

@nprofile…6kk0 Later down the line, we intend to allow users to try to decide morphism equality via e-graphs. But I don't want to rely on e-graphs in the conversion checker.

2025-10-01 15:44:02 UTC

- reply

@nprofile…6kk0 Word problems! If I'm presenting a category by generators and relations, then I can't decide morphism equality.

2025-10-01 15:26:51 UTC

- reply

@nprofile…6kk0 So, I have two phase distinctions. One is a classic static/dynamic phase distinction, which allows me to treat morphisms as opaque during conversion checking. The other is this "base type"/"refinement" phase distinction, which allows me to do this subtyping check in two stages. This is to make
[ A : (= Int), a : A ]
and
[ A : Type, a : A ] & [ .A := Int ]
convertable, even though they look quite different as type values.
Essentially, this is because the field types of a record are *syntax* (and a record type value closes over an environment), while refinements are *values*, which may not be valid to quote into the environment that the record type closes over, so I don't know how to "perform surgery" on the type definition to make the second one into the first one, and instead I just keep the specializations around and interpret them when I'm eta-expanding with respect to the type.
Maybe this is not the ideal way to do it, but this is how I've muddled through :P

2025-10-01 15:19:31 UTC

- reply

@nprofile…6kk0 I eventually plan to relax "convertable" to "is a subtelescope".
The point is though that there is a phase distinction whose open modality "forgets singletons", and first we check subtyping (or convertability) with respect to that, and then we check whether an eta-expanded element of A is an element of B. The eta-expansion "observes" whatever refinements have been put on, in any order, because eta expanding a neutral in a singleton type gives you the unique element of that singleton type.

2025-10-01 15:14:44 UTC

- reply

@nprofile…6kk0 I've been implementing extremely similar things recently... https://next.catcolab.org/dev/rust/catlog/tt/eval/struct.evaluator#method.subtype

2025-05-26 09:27:58 UTC

My dream CI setup for testing, linting, static sites, etc. would be:
- Have dependencies declaratively pre-built so I don't have to wait for apt-get to finish every freakin time. Nix does a poor job of this because I don't want to wait for nixpkgs to evaluate every freakin time.
- Be tied to a single machine with intermediate results locally cached
- Operate on the *diff* of a commit, so it didn't even need to look at files that didn't change and could pull their compilation results from cache

2025-05-22 13:19:05 UTC

- reply

@nprofile…6kk0 many such cases

2025-05-22 12:51:25 UTC

I'm really enjoying doing math informally in an extensional type theory. It shifts the ambiguity in my notation from "vibes for other mathematicians" to "rigorous, but modulo undecidable problems that could be formally extracted". And using longer variable names as I would while programming makes everything a lot clearer.
It would be pretty cool to have some kind of proof assistant for extensional type theory that would sometimes say "I don't know" for a conversion check, and then when reading informal math you could hover over something and it would show "this is true as long as you believe that these conversion checks I couldn't handle automatically are good"

2025-05-21 10:02:43 UTC

Today I learned about the construction of a topos from a tripos from Martin Hyland's "The Effective Topos".
It's a very intuitive construction. Basically, a tripos is a hyperdoctrine which gives a notion of proposition on a collection of objects, and the related topos is simply given by partial equivalence relations with respect to that hyperdoctrine.
It seems to me that one could perform this construction for a hyperdoctrine with less structure than a tripos, and this would be an interesting way of formalizing refinement types (and their extension https://dl.acm.org/doi/10.1145/3632869). That is, if we think of the objects in the hyperdoctrine as the "runtime types" and then the propositions as "runtime-erased verifications" this gives a neat account of verified computation.
Does anyone think about refinement types in these terms?

2025-05-21 09:25:51 UTC

- reply

@nprofile…6kk0 One interesting thing to note here is that ML didn't really come out of the PL community, it came from the fact that someone wanted a convenient language to *do a specific thing* (implement tactics for a proof assistant) and it turned out that a good solution for that was also a good solution for many other things.
Perhaps the problem with Java was that it wasn't created for its creators to do a specific thing; I could be wrong about this history though.

2025-05-21 09:10:35 UTC

- reply

@nprofile…6kk0 @nprofile…nalw I think the truth value of this depends on what you take "systems programming" to mean.
I like Andrew Kelley's definition of systems programming: systems programming is programming that is aware of the bottom-level APIs of the current system. https://youtu.be/Qncdi-Fg0-I?t=586
In the context of native software development, this means system calls to the OS.
And in this sense, you can absolutely do systems programming in safe Rust; there are safe Rust stdlib APIs with 1-to-1 mappings onto the underlying syscalls.

2025-05-12 16:02:30 UTC

- reply

@nprofile…v2av
https://media.mathstodon.xyz/media_attachments/files/114/495/700/914/402/958/original/bfb71bf63b7be67b.png

2025-04-13 12:09:43 UTC

I'm starting to think that one of the biggest benefits of a zettelkasten software (like Forester or whatever else) is simply that it reduces the friction of writing a medium-length thought down. Before I'd have to think "where should this go?" Now I just open a new tree and write. Of course, this is only achieved because I have the confidence that any features I need (e.g. tikz diagrams, KaTeX, links, bibliography) are supported; this means that I never have to decide between "markdown for convenience or LaTeX for good typesetting."
But it's a different value proposition than I originally thought, it's "this is a great place to write down plain text without fear that you will have to move it elsewhere when you need to put one diagram in it" rather than "you will use all of these features all the time." Sometimes the 90% solution (markdown) is really not sufficient, because without the last 10% of the features, you won't be confident to commit.

2025-03-28 22:41:13 UTC

- reply

@nprofile…6kk0 Ah OK! That is a reasonable scoping for Forester, it's one I disagree with but I can respect it and from that perspective the latex output is not so important.

2025-03-28 17:37:12 UTC

One of my favorite ideas in PL that I have seen recently (I can't remember all the places, but I think https://www.scattered-thoughts.net/#zest incorporates it) is to make type errors warnings, and compile them into runtime errors.
Of course, when you are deploying, you should turn those warning into compile-time errors. But why not allow the rest of the program to run during development?

2025-03-28 17:32:43 UTC

- reply

@nprofile…6kk0 lol, that's a good point, there's an uncanny valley of language shittiness.
But like, why not fully cross that valley? If we really want people to use Forester for writing papers, and writing a paper almost inevitably involves futzing with the journal template, then user-friendly customizability of LaTeX output is quite important, and this does seem to me like the most accessible way to do it because it involves skills that a user of Forester already develops.

2025-03-28 14:50:21 UTC

- reply

@nprofile…6kk0 Wait! I was thinking about extending Forester with an extension language, but Forester already is a programming language! An output backend for Forester could be specified by a Forester module which defined \p, \ul, \title, etc.
What do you think??

2025-03-28 14:19:04 UTC

- reply

@nprofile…6kk0 The concern about XML, that it exposes internal Forester abstractions that are changing quickly, definitely makes sense to me.
I worry that moving the XML to mirror the Forester IR would lead to a duplication between xslt and Forester itself though.
Here's a concept: what if the rendering stage uses something like a tagless final encoding, where we have a module signature which contains methods for each node in the current XML spec. Implementing this module signature would be essentially a cheap, typed version of the current xslt files.
Then using Dynlink, Forester could pull in additional backends at runtime.
This is similar to the Pandoc strategy for custom writers via Lua, except using OCaml rather than Lua.

2025-03-28 10:28:12 UTC

- reply

@nprofile…6kk0 I guess it depends on what an archival format is for. If the archival format is for making sure that what you publish will be able to be read *in some way* in the future, then HTML makes sense. If the archival format is for making sure that what you publish will be able to be read *in a way adapted to future standards* then I feel like there is an argument for XML, because XSLT allows it to be flexibly processed.
I do actually think that XML output is one of the killer features of forester, because it allows the LaTeX output to be endlessly customized once you understand a bit of XSLT.
Also, you should check out Xee: https://blog.startifact.com/posts/xee/, which is a modern XSLT implementation. If this ends up being what you want to use, I can help to bundle a statically compiled version alongside forester.

2025-03-26 18:50:27 UTC

- reply

@nprofile…6kk0 I did kind of like the idea that the "archive-quality" product of forester was the XML, but if the canonical links go to the HTML, then this kind of undermines this.

2025-03-26 13:28:45 UTC

- reply

@nprofile…6kk0 @nprofile…8atg Ah, I was googling f-expression instead of fexpr. Drat, I will have to come up with another name I suppose.

2025-03-26 12:49:28 UTC

I'm excited to share something I've been working with for a while in the context of small language experiments: a new "lower-house" syntax to compete with s-expressions (following the nomenclature of @nprofile…8atg in https://parentheticallyspeaking.org/articles/bicameral-not-homoiconic/). I call the syntax "f-expressions."
Implementation: https://github.com/ToposInstitute/fexplib
Documentation: https://forest.topos.site/public/foreign-topos-ocl-00CE.xml
Examples of use: https://github.com/ToposInstitute/emtt/tree/main/examples

2025-03-26 10:00:58 UTC

- reply

@nprofile…6kk0 Are you going to make "number of digits" a configurable parameter for forester? And are you going to give all your existing trees a leading 0?
And why not add two digits when you are at it, so that you can say you are moving from TPv4 to TPv6 (TP = tree protocol) :P

2025-03-26 09:52:39 UTC

- reply

@nprofile…6kk0 Also, are you going to run out of tree addresses soon @nprofile…6kk0?? What's your plan??

2025-03-26 09:51:26 UTC

- reply

@nprofile…6kk0 What I would hope from this is that the move from forest://host/tree to canonical URLs is essentially *injective*, so that links are still semantically intelligible.
One other question is how will this impact cross-forest transclusion?