april aka cyberglot / is on Nostr

professional program keyboardist. software engineer who spends too much time thinking about type theory and programming language theory.

Last Notes

2025-04-23 14:07:28

- reply

@nprofile…6kk0 is it more mainstream? 🤔 for sure I’m biased

2025-04-23 12:29:26

new PL trend idea: we use System F as an example rather than STLC.

2025-04-10 14:33:34

I’m reading “Formal metatheory of second-order abstract syntax” by Fiore and Szamozvancev. On pages 6-7, they introduce a skew-monoidal closed structure, and then they say this (pic 1). I was interested on why a dependent sum is skewed, so I found out it’s a left adjoint to the base change functor (pic 2). Now, what coends have to do with the base change functor? Or they don’t have anything to do with each other, it’s just that dependent sums are left-leaning and don’t preserve colimits?
https://cdn.masto.host/cyberglotlol/media_attachments/files/114/314/125/231/464/650/original/7007c57ad525a8b6.jpeg
https://cdn.masto.host/cyberglotlol/media_attachments/files/114/314/125/302/286/051/original/3bb87e96f524b5d9.jpeg

2025-03-28 14:26:00

- reply

@nprofile…6kk0 unrelatedly, but still about forester, have you scheduled implementing parsing on tree-sitter or no plans for that? last I checked you were using Menhir?

2025-03-28 12:18:42

- reply

@nprofile…6kk0 while I agree with you, I feel that my transient notes are often useless over time. I’m usually extremely succinct, unless I had time to sit down with what I want to write. So, having an obligation to improve my notes helps me remember to schedule a time to find out what I want to write. On the other hand, it does create a feeling that I’m falling behind on that obligation.

2025-03-25 12:50:51

what “when legitimate” is supposed to mean? this is in the introduction of “category theory and applications” by marco grandis.
https://cdn.masto.host/cyberglotlol/media_attachments/files/114/223/152/584/101/218/original/0a72793728c87913.jpeg

2025-02-24 16:39:54

- reply

@nprofile…6kk0 I’m hoping to remove the whole roundtrip and the need for translation between levels and indexes, then the whole process amounts to just going from one thinning into another and it is traversal-free. I’m not sure if this is worth doing at all! it’s another instance of me yet again changing things and seeing what happens 😅

2025-02-24 14:01:57

- reply

@nprofile…6kk0 yesterday I started to implement thinnings for binders, but they are fairly sour to deal with without dependent types, but also I don’t want to use agda for this. 🥲

2025-02-24 14:01:57

- reply

@nprofile…6kk0 yesterday I started to implement thinnings for binders, but they are fairly sour to deal with without dependent types, but also I don’t want to use agda for this. 🥲

2025-02-24 13:11:36

- reply

@nprofile…6kk0 what are you using for binders? I’ve been using András’s names to de bruijn indexes/levels, but I don’t like it!

2025-02-24 13:06:19

- reply

@nprofile…6kk0 is this lean? 🤔

2025-02-20 13:01:58

I'm making this Tufte-inspired Typst template and I think it looks pretty good 🥰
it's based off of an already-existing tufte template for Typst, but I've changed lots of stuff and I think it will eventually become it's own thing.
https://cdn.masto.host/cyberglotlol/media_attachments/files/114/036/339/564/769/043/original/f9d4668afe1aab42.png