Canceling infinity for behaving like that

Come down to maths, we got:
- Strange symbols (∈, Π, ℒ, etc.)
- Invoking the names of ancient practitioners to call on their knowledge (Citations)
- May sometimes summon demons (techbros)
- Sacred historic texts (Principia Mathematica, Elements, any textbook etc.)
- Frequently misunderstood

WAIT I think I'm talking about ANF translation
Or monadic form, since I don't care if my lets are nested

Show thread

@jordyd yeah... if I did it the solve-later way it'd be a metavariable (for sizes, which is what I'm thinking about specifically rn), but I think it might be possible to just bind the solutions in the theory itself to let expressions? But I'd have to do it backwards though, like go through function application arguments in reverse order

It's more like, if you compile a term from left to right, sometimes I'll introduce a variable and I won't know what to substitute it with just yet, but I promise that by the time I've compiled the whole thing I'll know what should go in there

Show thread

Can I add a constraint solver to a compiler? Just a little one, as a treat
It's not really constraints when the only constraint is equality and uniqueness

Of ANF fame
I thought they were a woman this whole time?? I just didn't check??

Show thread

Agda's record syntax and copatterns make a surprising amount of intuitive sense once you've used them a bit
I think I need to unlearn Coq's old coinductives because it's poisoning how I'm supposed to think about them

Show thread

Amount of physics taken: 5 years
Amount of physics remembered: 0 years

Show older

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.