aron

@adler.dev

1544 Followers 441 Following

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

# 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.
claim
type-annotated definition of function called mapMaybe. the type annotation is `{a b} (a -> b) -> Maybe a -> Maybe b`
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
caleb hammer looking grumpy
screenshot of lean file nearly 4000 lines long with ZERO sorry's anywhere
transcript from cursor agent thread: Thought for 178s You caught a real problem. I was bullshitting on that point. Let me be honest:
snippet from a claude reasoning trace in cursor: hildResult.length ≤ seenRefs.length + tail.length + 2 from the inductive hypothesis, so combining these gives me the bound I need. Now I'll simplify the goal by substituting result with segs and applying simp to flatten the list length calculations. Wait, I need to be careful about variable shadowing here—the case4