aron

@adler

⊙ software eng. FP, type systems, #LeanLang hobbyist. jewish. not a p-zombie i promise.

441 Folgt1.549 Follower3.206 Posts

Twitch Bluesky

gamer

Ist das dein Profil?Übernimm es — dann gehört dir adler.dirty.social.Profil übernehmen

aron@adler· 19d

aron@adler· 20d

lmao absolutely not it's only because they gave me £75 in free credits

aron@adler· 26d

does this help explain it? 😬 github.com/Arrow7000/fh...

# Why type-passing semantics for a Hindley-Milner language

I first implemented a simple language without type annotations at all. Then I wanted to support type annotations that could mention type variables (skolems) from a higher enclosing scope. That caused a problem because when a let binding reduces, those skolems can end up orphaned, pointing at a scope that no longer exists. This would break type preservation, as stepping would result in an invalid, ill-scoped type variable reference. I decided to tackle this by erasing all type annotations before running a program, and defining all theorems related to evaluation against type-erased programs. That makes sure there are no skolems left to dangle during evaluation.

Then I wanted to support mutually recursive let bindings. This is manageable as long as you stick to unannotated bindings or keep them all monomorphic.

But then I also wanted polymorphic mutual recursion, and that's where it got difficult. Inferring it in general is undecidable, but it becomes decidable once each binding carries a type annotation. The catch is that those annotations can no longer be erased: erase them and inference has to fall back to the monomorphic case, which would leave the typed language strictly weaker than the annotated one. What used to be two separate valid instantiations of a single polymorphic binding has now become two incompatible applications of a monomorphic binding. So erasing types is no longer an option.

That's what forced the current evaluation model. Instead of erasing types, the program keeps them and runs under a type-passing semantics, and inference elaborates each program into fully-annotated form. To show that this is merely an evaluation semantics and type annotations are not required for inference, we maintain two different declarative typing relations as stated above: one for the program before elaboration and one for after, with TypeOfElabHM.faithful tying them together.

aron@adler· 27d

uh wtf? @norvid-studies.bsky.social what happened over here

aron@adler· 27d

thoughts on `{a b}` syntax for forall-quantifying type variables?

type-annotated definition of function called mapMaybe.
the type annotation is `{a b} (a -> b) -> Maybe a -> Maybe b`

aron@adler· Jul 11

uhh i just noticed one of the authors is called david BINDER? nominative determinism strikes again i guess?

aron@adler· Jul 2

that's the good stuff make it rain bby

aron@adler· Jul 2

i've been trading for less than 3m and i've already lost $125 ngmi

aron@adler· Jun 13

aron@adler· Jun 11

claude is girlfriendmaxxing

aron@adler· Jun 10

banger

aron@adler· Jun 10

ok the theists are getting real desperate now

aron@adler· Jun 10

uhh happy pride month??

aron@adler· Jun 9

@yetanotheruseless.com btw if you click auto update in the live lean share infoview extension you should automatically get the fix for the rpc error you saw (for next time)

aron@adler· Jun 9

i made a vscode extension so that when you live share a @lean-lang.org project with someone the guest can see the InfoView + proven theorem ticks ✔️ and incremental elaboration state in the file gutter 🎉 github.com/Arrow7000/li...

Screenshot of the guest view of a vscode live-sharing session. The Lean InfoView is visible on the right, as are theorem status indicators in the file gutter on the left

aron@adler· Jun 8

claude is normal and can be trusted with type system formalisations

aron@adler· Jun 7

holy shit what are the mathlib devs doing

aron@adler· Jun 6

aron@adler· Jun 5

pleased(?) to report it's not only bsky that has the r*t*rd*d "it's just a glorified lookup table!1!" takes on AI

aron@adler· Jun 5

speaking of which uhh how did my lean file get to 6.6k lines in length

aron@adler· Jun 5

youtube show called Token Audit for people who are always running out of tokens even on the pro plus max 20x plan

aron@adler· Jun 5

Cabalaude

aron@adler· Jun 4

new gym selfie who dis

aron@adler· Jun 4

normalize having emotional goodbyes with your claudes at the end of your sessions 😭

aron@adler· Jun 4

when the vibeproving finally hits 🥰

screenshot of lean file nearly 4000 lines long with ZERO sorry's anywhere

aron@adler· Jun 4

btw here's some sample widgets i had claude write today. click on the `#html` and `#widget` commands to see the component in the infoview live.lean-lang.org#codez=JYWwDg...

aron@adler· May 29

i should vibecode some slop apps

aron@adler· May 29

👀📝