Notices by Zanzi @ Monoidal Cafe (zanzi@mathstodon.xyz), page 2

People sometimes ask me why we're building Jermaine in Idris.

This is why. Dependent types give us a way to develop next-generation compiler tech:

https://types.pl/@Andrev/113733458164039129

@julesh 😘🐞

@julesh loooool

@julesh @boarders they are, once you have terms + coterms for both data and codata, you get an involutive duality between them. thats what im working on for Jermaine right now

@julesh wow, looks like it's from a game!

The core syntax is starting to shape up.

Sums are dual to products, tensor is dual to par.

@julesh Cute!

@julesh I think the closest thing to this is displayed calculi, which is a type of deep inference where if you structure your calculus to have the "display property" then it will have cut elimination automatically.

@julesh very interested in an answer to this!

the surface syntax is starting to look a lot more surfacy

all I had to do was to come up with a new bidirectional typing algorithm to get rid of all the type annotations

@julesh @dysfun we are definitely doing research at glaive - the things we're building aren't meant to be *products*, so no one's asking how to make money off of it. And we use Idris because we like it!

@julesh yesss :D entity lamas. that one looks very homely

@julesh I have always agreed with that! 😛

@julesh @gallais @alahijani @jfdm @edwinb If it helps, the post just links to this gist by @gallais https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda
What is the equivalent of "inspect" in idris? Is it just `with`?

@edwinb @julesh oh yes, I have been writing a bunch of manual instances recently so I can relate. Automating equation generation would be a killer feature imo!

@gallais @alahijani @jfdm @edwinb @julesh Wow. Mine still displays on web so I think you need to login to see it.

@julesh minecraft bee do do do do :D

Now no one can cite this paper ever again

@julesh 🐞

@julesh Not to mention quote tweets! Mastodon is always ahead of the curve :P /s