zanzi - Network

In the polymorphic lambda calculus, we can encode least and greatest type-level fixpoints using quantifiersIs there an analogous...

In the polymorphic lambda calculus, we can encode least and greatest type-level fixpoints using quantifiers

Is there an analogous construction for term-level fixpoints?

Does anyone here know contextual operational semantics? I'm trying to implement a calculus that's based on linear proof nets, but...

Does anyone here know contextual operational semantics?

I'm trying to implement a calculus that's based on linear proof nets, but they use contextual semantics in a cruicial way, and I just can't get my head around it

i fought this guy in dark souls

i fought this guy in dark souls

every compact closed category can be equipped with a canonical trace operator, and a star-autonomous category with a trace is automatically...

every compact closed category can be equipped with a canonical trace operator, and a star-autonomous category with a trace is automatically compact closed.

Question: Is there a way to equip a star-autonomous category with some manner of 'guarded trace', in a way that won't collapse it into a compact closed cat?

If you're wondering what compiler infrastructure would look like in dependent types, check out this blog post.We use this library for...

If you're wondering what compiler infrastructure would look like in dependent types, check out this blog post.

We use this library for the development of our language Jermaine at Glaive

https://mathstodon.xyz/@julesh/114160438017729875

Is there ever a use-case for needing untagged unions rather than sum types?

Is there ever a use-case for needing untagged unions rather than sum types?

Thank you all for coming, and for the great feedback! The recording is available here:...

Thank you all for coming, and for the great feedback!

The recording is available here: https://www.youtube.com/watch?v=0Qg_RnSHyhU&feature=youtu.be

https://mathstodon.xyz/@zanzi/114121677541946630

Very excited to present my take on bidirectional typing at MSP this Monday coming!We can use polarity and chirality (duality between...

Very excited to present my take on bidirectional typing at MSP this Monday coming!

We can use polarity and chirality (duality between producers and consumers) to develop a canonical bidirectional typing discipline that requires minimal annotations.

The hottest takeaway is that polarity exists even in languages that don't make it explicit.

https://mastodon.acm.org/@mspstrath/114121543187299720

is there a reference for combining bidirectional type-checking with unification? ie the bidi system infers most of the types, while the...

is there a reference for combining bidirectional type-checking with unification?

ie the bidi system infers most of the types, while the unification only fills in the type-annotations?

yeah, I dont think AI is coming for your job any time soon

yeah, I dont think AI is coming for your job any time soon

interestingly, this reminds me of dependent optics all over again - we have a thing with two generalisations - one that's simply typed...

interestingly, this reminds me of dependent optics all over again - we have a thing with two generalisations - one that's simply typed and monoidal, the other is fancy typed and cartesian.

you'd expect that combining the two would be easy, but no.

https://mathstodon.xyz/@zanzi/114020990758143013

I was hoping someone would say "Well, actually, substructural polymorphism is much easier than you think it is!" but so far no...

I was hoping someone would say "Well, actually, substructural polymorphism is much easier than you think it is!" but so far no one's done that.

So perhaps I'm correct that it's harder than people give it credit for.

https://mathstodon.xyz/@zanzi/114019638664236298

I'm writing a new blog series on practical implementation of substructural type systems, in Idris!The first blog post will look at...

I'm writing a new blog series on practical implementation of substructural type systems, in Idris!

The first blog post will look at substructural polymorphism and why it's *hard*, harder than people assume on first glance!

https://zanzix.github.io/posts/5-substructural-polymorphism.html

Twitter was always overrun by dumb people, but now it's overrun by dumb people who are *proud* of being dumb, and that's a whole...

Twitter was always overrun by dumb people, but now it's overrun by dumb people who are *proud* of being dumb, and that's a whole nother level of intolerable

Blursed idea: dependently-typed json syntax

Blursed idea: dependently-typed json syntax

Dependent types. the final frontier. to boldly type what no one has typed before.

Dependent types. the final frontier. to boldly type what no one has typed before.

does anyone have a non-trivial example of a linearly distributive category that's not compact closed, ie not Rel/Vect/Prof/Span?

does anyone have a non-trivial example of a linearly distributive category that's not compact closed, ie not Rel/Vect/Prof/Span?

A new chapter in categorical-ML has just dropped:Transformers are *applicative functors*, and we can use this to generalize them beyond...

A new chapter in categorical-ML has just dropped:

Transformers are *applicative functors*, and we can use this to generalize them beyond matrices

https://glaive-research.org/2025/02/11/Generalized-Transformers-from-Applicative-Functors.html

@JadeMasterMath id be curious what you think, I may have figured out dependent kinds, or at least getting close to it

@JadeMasterMath id be curious what you think, I may have figured out dependent kinds, or at least getting close to it