Conversation

This Tweet is from a suspended account. Learn more

Aug 6, 2020

I’ve done lots of type-level hacking in haskell to the point I am traumatised to do it again and I wish I could just write some idris/agda and deliver it as a binary package to people 😭😭😭

Same but in Rust 😭😭😭

This is why I keep pushing static intro. I've done the Haskell type-level thing and it's soul sucking.

Replying to

and

Yeah, I want control over parametericity and inlining. Hence me wanting something like QTT and multistage programming for systems programming. Trying my best to get there eventually with Pikelet but it's slow, and there seem to be gaps in the theory on this stuff.

1:18 AM · Aug 7, 2020Twitter Web App

Replying to

and

Most of the static intro langs give you inlining. Parametricity is out the window.