Kali
banner
kali-tt.bsky.social
Kali
@kali-tt.bsky.social
CS student at Yale, she/her
Last week I put work off for Future Me, and without realizing I have become Future Me. How does she always get me???
October 30, 2024 at 7:38 AM
Making a OCaml parser combinator library for fun! I’m going with an applicative interface instead of the standard monadic interface, which should allow me to get much better performance and error messages. It does restrict you to context-free grammars though, but that’s not much of a restriction
December 28, 2023 at 4:56 PM
I wonder if it’s possible to create a language-agnostic structured editor 🤔
December 26, 2023 at 10:24 PM
I’ve had people ask me “what is type theory” and the best answer I’ve been able to come up with is “the study of notions of well-formed syntax, and what properties that well-formedness implies”. For instance, for most languages well-formedness wrt the type system implies some sort of safety…
December 26, 2023 at 3:37 PM
I used to use Agda a lot, but tbh I'm much more satisfied with Coq for large-scale developments, the primary reason being Agda's proof automation is a lot less mature. That's something that can just be improved with time though, I wonder if anyone's made a tactic framework for Agda! #proofassistants
December 25, 2023 at 10:32 PM
Something people often get confused about is the relationship between type theory and set theory. You can think about it with this (somewhat ridiculous) metaphor: Type theory is like a poem, and set theory is like an *interpretation* of the poem. Let's dive into that a little more... 🧵
December 25, 2023 at 9:11 PM
OCaml's `Dynlink` module is so cool! I'm realizing that this is probably how Coq implements plugins? It's how I'm doing it in the proof assistant I'm implementing anyway. Hoping to have something usable soon... flip-flopped so many times on the design haha
December 25, 2023 at 4:36 PM
Been using OCaml a lot recently and loving it. Type parameters being backwards is a little weird, but that’s fine. Overall it’s a clean, consistent, expressive language that sets up nice guardrails without forcing you to stay inside them. I get why people say ML is a language design sweet-spot!
December 25, 2023 at 3:12 PM
Fun fact: You are topologically equivalent to a 7-holed donut, and thanks to homotopy type theory that means you are also equivalent to a certain higher-inductive type.

Thank you for attending my TED talk.
December 25, 2023 at 7:59 AM
The biggest issue I’ve noticed that every person who learns Prolog brings up is the lack of informative runtime errors. Instead of a nice crash message or whatever, you just get `false`.

I like logic programming! But this is a big issue it has. It comes down to something more fundamental though…
December 25, 2023 at 7:26 AM
Thinking about metalanguages for proof assistants… in theorem proving systems we almost always have some sort of proof automation, and if we want to create our *own* proof automation then we need some sort of metaprogramming. In Agda this is reflection, in Coq this is Ltac, etc… 🧵
December 25, 2023 at 6:31 AM