Kali

So to answer the question directly: No this is not a limitation. You can store an (algebraic) effectful computation in a structure by "thunking" it behind a function that takes unit, like I did above.

Languages make this less obvious by putting the effect on the function type, but just think of a monadic computation `m : M a` into a computation `m : () -{M}→ a`. You can always move from the algebraic effects world into the monad world with no issues.

This may make the connection clearer: Algebraic effects are exactly equivalent to the free monad on some effect signature. Algebraic effects _are_ one specific monad.

Last week I put work off for Future Me, and without realizing I have become Future Me. How does she always get me???

This is so beautiful :) thank you for sharing

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

I’m more wondering about what desired editing features are shared between languages

e.g in theorem provers there’s a great need for in-depth typing info at every point in the program, but for other languages not so much. Do we target the largest denominator? I’m not sure

You look beautiful! Happy Christmas 🙏

I wonder if it’s possible to create a language-agnostic structured editor 🤔

Ah man I thought OCaml overloaded record fields 😢 that sucks, good to know

Anyway, to reiterate: Type theory is the study of (notions of) syntactic well-formedness, and what we can derive from it. #proofassistants

math, or powerful to the point where we can create entirely new logics!

The connection to well-formedness is usually lost in this way - type theory subsumed simpler notions of well-formedness, but it also handles those much more complex cases, and so we focus on them since they’re interesting…

There’s an informal well-formedness check in *all* math. Type theory *formalizes* these informal checks!

A type theory is two things: The syntax of the theory, and the typing judgement. This typing judgement can be simple to where it’s reduced to the informal well-formedness left implicit in all…

“this string of symbols represents an object that I’m working with”. For instance, “nrjfuhejsis” is not a word, and our brains know that automatically! This exact same thing happens in math. For instance I know that “∨×⇔∛∑∪” doesn’t make sense as a logical formula - it’s just a random string! …

like guaranteeing the absence of unsafe casts, like interpreting a string as an integer or what have you

The mathematical context for this is interesting. In any sort of math, we have the syntax for what we’re doing - the notation we use to represent our objects - and we have some notion of…

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…

So adorable!

Please show me! I haven’t yet run into the situation you describe

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

trying out new features and axioms in their type theories, seeing whether those additions make sense and what semantics they can be given. Type theory is much more broad and diverse than set theory. Perhaps this will change as it ages and we will settle on a single theory like people settled on ZFC.

For instance homotopy type theory interprets types not as sets but as *topological spaces*, giving rise to a new and useful axiom (called "univalence").

Type theory is very different from set theory in its diversity - set theorists have mainly settled on ZFC, whereas type theories are constantly...

and we trust sets, so we believe we can trust types. Type theory is the syntax, set theory is the semantics.

The neat thing is that set theory isn't the only semantics we can give to type theory! I've been saying "type theory" as if it's all one thing, but there are *many* different type theories…

This is exactly the relationship between type theory and set theory. Set theory is old and trusted, while type theory is new and quickly evolving. We thus make sure all our new type theories are logically consistent by *interpreting* them into set theory - we can think of types in terms of sets...

This happens all the time in math! How do we know we can trust new methods of reasoning (new logics)? The best way is essentially just to related it to some older method of reasoning (older logics) that we already trust. The new logic is called the "syntax" and the old logic is the "semantics"...

translate the formulas from this untrusted logic to the trusted one. Maybe you try some other, more indirect translation. But either way, what you're trying to do is *define* the untrusted logic in terms of the trusted one

What you've stumbled on is the distinction between "syntax" and "semantics"…

"How do I know that these rules are *correct*? What if these rules actually allow me to prove a contradiction or some other kind of logical inconsistency?"

You don't trust this logic yet! So what you might do is go to a logic you *do* trust, and try to compare the two. Maybe you try to...

I can write down a logical formula like "A implies B" and then prove that using the rules of the logic. We can state and prove more and more complex formulas, and come to more and more complex conclusions.

But you might have a nagging doubt as you use these rules...

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... 🧵

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

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!