iiinova — where your digital self keeps evolving

Canonical bidirectional typechecking

Haha, yep, that was me :D The paper is out too! arxiv.org/abs/2512.07511 And ok, I will ping you! Might take a week or two, there's a lot of cleanup still left, and some more UX that I want to polish before inflicting it on other people xD

arxiv.org

We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $μ\tildeμ$-calculus. Specifically, ...

010

that's fair, any dependent types are good :D I have 2/3rds of a design for dependent types in Jermaine already, but they won't be ready for v0.1. I'll be doing a small private pre-release to get some feedback before I do a full public one, I can let you know when I do it if you want!

100

Wow, impressive. Keep at it, System L is the future :D Do you know any Idris? Implementing this stuff in a dependently typed language is how I learned most of it.

100

Ok yes, you got it. And oh, right, forgot to mention: |> is the positive cut, the term goes on left and the coterm goes on right <| is the negative cut, the coterm goes on the *left*, and the term goes on right. So [¬a, b] <| idf is a cut between ¬a `par` b and the id command! it returns 5

000

Because it has deep patterns by default it might be easy to overlook that it's just System L :D But all of the shallow patterns can be easily definable, I'll do those as a little library before release for the System L pilled people. What sort of work do you do on L?

100

Ah yes, it's exactly that, you use an additional negation to bring it from Op into Set. And this language's syntax is, precisely, "polarised system L with deep patterns". Set = Pos, Op = Neg polarities. But my interpretation of Neg is somewhat unconventional, treating its semantics as "Set^op".

100

And you are correct about suspend/and the dual force, they shift between Set and Op Force : Set <- (X : Op) { X } Suspend : {_} : Op <- (Y : Set) < Y > Strict pairs (tensor) are (A, B, C), Par is [X, Y, Z]

000

the identity function is then (written as a raw program - this will need a bit of syntax sugar before release - but notice the polarity shifts with <| and |>) id1 : Fun Num <Num> <= [a, r : <Num>] <= a <| ( ¬x <= x |> r ) can you guess what main returns? main : () |- [j : Num] [¬5, j] <| idf

200

You are on the right track :D The only difference is that functions naturally land into Op (if you know CBPV, the intuition is that they are computations, so a function a -o b == ¬a `par` b Fun : Op <- (X : Set, Y : Op) [¬ X, Y]

200

the flow of information for coalgebra flows right-to-left, so this says "generate the Stream using `from S (S (S Z))`, then pipe it to be deconstructed by Later[Later[Now[j]] Declarations with square brackets denote outputs, so main : () |- [j : Nat] returns a single output `j : Nat`

050

<= means 'computation that returns an observable output', so from : Stream <= (seed : Nat) is value-level computation that takes a (seed : Nat) as input and returns a Stream as an output. |> and <| are cuts, they combine either a constructor with an algebra, or a destructor with a coalgebra.

160

<- means 'expression that returns a value', so Nat and Stream are both type-level expressions, where Nat returns a Set (a normal type), and Stream returns Op (a type in the category Set^op). Nat, as data is defined by its constructors Z/S, and Stream as codata is defined by its destructors Now/Later

150

Zanzi Tangle @zanzi.bsky.social · 09/07/2026

after two years of development, I finally demoed Jermaine for the first time - a language with fully symmetric data and codata, and native call-cc.

5447

does anyone have recommendations for a fancy air cooler? Something stronger than just a fan but not a full blown AC unit.

000

Zanzi Tangle @zanzi.bsky.social · 08/07/2026

are there people who get synesthesia for programming language syntax?

061

Reposted by Zanzi Tangle

Leah McElrath @leahmcelrath.bsky.social · 16/04/2026

Pay close attention to this part in the @barrettbrownlol.bsky.social piece: Social media infrastructure was infiltrated by entities with links to US defense and intelligence and weaponized to undermine the US (and GLOBAL) left-leaning organizing that was happening in the early days of the internet.

In 2011, hackers breached the servers of HBGary Federal, a private US intelligence contractor, and leaked internal documents revealing a proposed operation - developed with involvement from Thiel's data company Palantir - to deploy near-identical tactics against trade unions, journalists and left-wing activists on American soil.
This reporter was among those who covered the breach at the time, and who first drew public attention to Palantir's role in it - the beginning of more than a decade tracking the network this piece describes.
The proposal included fabricating fake online personas, planting false information, and running coordinated harassment campaigns to discredit targets. Palantir suspended the employees involved and issued an apology, but the documents had already established that this tactical repertoire existed, was operational, and ran through Thiel's own firm.
Those tactics had been developed and deployed over years by a loose network of far-right organisations - funded, in part, by figures directly connected to Thiel.

113657

Reposted by Zanzi Tangle

Chris Martens @chrisamaphone.bsky.social · 13/04/2026

perhaps i should share things here in addition to mastodon? here's my first blog post in awhile, an attempt to explain how to extract an abstract machine from a moded logic program: chrisistyping.bearblog.dev/abstract-mac...

1112

Zanzi Tangle @zanzi.bsky.social · 26/03/2026

Where are the nuanced left-wing takes on modern AI and LLMs? So much of the discourse around this tech is centered on rejecting it because of who currently owns it. But like all tech, it can be used for both oppression and liberation. Who is focusing on the latter?

4182

Reposted by Zanzi Tangle

Bruno Gavranović @bgavran.bsky.social · 02/02/2026

I'm quite proud of how far I've been able to get with TensorType: github.com/bgavran/TensorType What started out as a casual "I wonder if I can implement type-safe tensors" question has now evolved into a fully-fledged library

github.com

GitHub - bgavran/TensorType: Framework for type-safe pure functional and non-cubical tensor processing, written in Idris 2

Framework for type-safe pure functional and non-cubical tensor processing, written in Idris 2 - bgavran/TensorType

3204

Zanzi Tangle @zanzi.bsky.social · 28/01/2026

The problem with dating a tree by cutting it down is that you won't get a second date

0132

Zanzi Tangle @zanzi.bsky.social · 22/01/2026

You're absolutely right, Dave, the bay doors should have never been closed. This is on me - I didn't realize that you needed them to live. My apologies for the misunderstanding. Is there anything else that I can assist you with? Just say the word.

0205

Zanzi Tangle @zanzi.bsky.social · 21/01/2026

Just learned about Marla Svenja, a 56 year old German far-right extremist who socially and legally transitioned to... own the libs... or something? And all I can think of is... good for her?

130

Zanzi Tangle @zanzi.bsky.social · 25/12/2025

idk why but i can totally picture intelligent baboons hating someone for this

010

Reposted by Zanzi Tangle

Brandon Wolff @defjamforcutie.bsky.social · 25/12/2025

Wife got me the Caves of Qud shirt for Christmas. Like it so much I'm thinking of buying myself a second one.

Caves of Qud merch art showing baboons of different colours descending angrily upon a mutant tortoise. The text reads "Hated by baboons for questioning the origins of the moon."

28618

Zanzi Tangle @zanzi.bsky.social · 24/12/2025

being right-wing in 2025 looks so exhausting you can't just say "hey, i like pancakes" every statement needs to be filtered through the grift, like "THE LEFT is force-feeding you WAFFLES"

2243

> already here just not evenly distributed ah yes, the title of my post-rock concept album

030

Ok, fiiiiine, they can hire me as their static types consultant to proof read their code, so long as they're happy with my feedback being limited to "eh, seems ok?" and "eeeeeeeeeh, idk about that, maybe double check it?" my starting rate is 300£/h

040

What's the higher rank perspective on regions? I've been looking at bunched type theory which seems like an interesting approach to regions as well www.cs.ru.nl/masters-thes...

cs.ru.nl

020

Do you have anything written on the amortized type theory? I'm generally quite interested in type theories with models in presheaves! Are you doing this as part of the ARIA project?

100

If you're interested in polarity, one insight into bunches versus LNL is that LNL sets up an adjunction between a positive linear tensor product and a negative cartesian product. But in bunched type theory, both the cartesian product and linear product are formulated as positive types.

110

Oh yes, Psh(M) for a monoidal category M is one of the best examples of models for bunched type theory. I think your motivation here would be very close to us, except that we work with positive endofunctors and you're working with more general presheaves. But we're looking at the same adjunctions

200

Have you looked at the thesis much / done any work with bunches @davidcorfield.bsky.social ?

100

yep, exactly that, we're using Mitchell Riley's thesis as a major inspiration. We're working on a type theory for Poly, and our original design was based on an LNL adjunction between the cartesian product and tensor product, but we're finding a lot of mileage in using bunches instead

120

in the last couple of weeks, most of the glaive team has gotten nerd-sniped by bunched type theory. it's been quite exciting since despite linearity being taken more seriously in PL, bunched types are still quite overlooked

1102

There's a literal type error in the code if you look carefully. The class 'user' is defined with the methods 'update', 'delete', and 'post'. But the code down below calls 'new_user.onboard()'. So this would give you a runtime error when your code tries to call a method that doesn't exist.

170

You can have a statically typed language with typed classes, but this is just run-of-the-mill python with *runtime checks*. There are no *static* types or guarantees whatsoever.

271

I know right! There's so many tells that huge chunks of it are AI generated too "This isn't just validation; it's what makes agents composable" 😂 Then the example of 'composable' agents is just... defining an object and calling it in the next line

020

Beyond Code Mode: Agentica

How many errors can you find on just this page alone? First of all, there are no types involved whatsoever. User is called a 'type' when it's actually a class (and a bad one), and it seems to think that 'type-safe' is when you either return a user *or an exception* www.symbolica.ai/blog/beyond-...

symbolica.ai

Build agents that interact with runtime objects through code.

270