­jonoodle­ @ionchy@types.pl

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

I think I just described a let expression

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

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??

Wait is Amr Sabry not a woman?

​
I forgot we had this

does the f*ck emoji go under Miscellaneous

okay who added ​

​

@vdash https://twitter.com/jonmsterling/status/1382453125114630144
he's saying things again

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

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

Inductives start from nothing and build up with constructors, and coinductive start from everything and tear down with destructors is all

Something something monotone operators I don't remember this stuff

How to explain coinductives

​