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

@julesh sheeps :D

@julesh relevant: https://pivot-to-ai.com/2025/01/13/uk-government-plans-to-splurge-billions-on-ai-we-step-through-the-tricky-details/

@julesh 😴 😴 😴

@typeswitch @julesh doom crowbar mod

@julesh step 2: we need an economy framework. That way, even if you *can* produce 10 million m/pm, you'll want to be smart about it to avoid crashing the economy.

@julesh this is what peak performance looks like

Programs in Jermaine take a list of inputs to a disjoint union of outputs.

So this program takes a sum (s : Either a b) and branches off into two branches, one of which outputs (this : a) and the other (that : b)

concrete syntax is starting to take form (thanks to @julesh and @Andrev)

@julesh https://www.youtube.com/watch?v=V_A9sAaNawU

@julesh 🐞

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