Hacker News Reader

Comment by solomonb | Hacker News Reader

Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory.

The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."

All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.

View on HN

I'd never heard of Cubical Type Theory, how interesting. Aside from that, and Mikan - why they forked, their development/contribution policy (which I happen to agree with more or less); and the notion of equality and equivalence (you didn't use this word but I read an article¹ with a glimpse into these concepts).. "Equalities are paths" - I'm going to be thinking about that for a while. Anyway the link to 1lab and the comments in this thread gave me various ideas to chew on, there's lot of substance there.

On the 1lab site, I started with simply-typed lambda calculus, an all-time classic that I've always wanted to understand more fully. How the site is designed, I love the syntax-highlighted math/code and the interface where every single concept can be clicked and hovered over to show additional information with usually a link to its own page. It led me to a kind of branching, graph-like manner of learning, where I open pages on categories, products, morphisms, uniqueness, equality - filling holes in my understanding as needed, then going back to more specific ideas built from those general foundational concepts.

An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression, to support an autodidactic and exploratory style of learning. It relates to topics raised elsewhere in this thread, like a "proper IDE for math" (integrated development environment for mathematics) and a language-agnostic "standard library" of data structures, algorithms, definitions, theorems, etc., where programming languages can import from a shared corpus of mathematically rigorous primitives.

> how to use dependent types to explore, teach, and formalize mathematics in a pro-human way

I find it meaningful how you phrased this - at this point in history with the state of technology that can overwhelm and devalue human intelligence, it's more important than ever to focus on how we teach, learn, communicate and cultivate understanding.

On a tangent, one of my interests is the book _Reflective Programs in Tree Calculus_² by Barry Jay, its proofs in Rocq, his more recent article "Typed Program Analysis without Encodings"³, and the work of his main collaborator⁴. I lack the relevant academic background to fully grasp it yet, so I've been chipping away at learning the necessary basics. So the link to 1lab is appreciated, it's a resource I'll be digging into over time.

---

¹ With Category Theory, Mathematics Escapes From Equality https://www.quantamagazine.org/with-category-theory-mathemat...

² https://github.com/barry-jay-personal/tree-calculus/blob/mas... (PDF)

³ https://github.com/barry-jay-personal/typed_tree_calculus/bl... (PDF)

⁴ https://github.com/lambada-llc/tree-calculus

What a wonderful response :)

> I'm going to be thinking about that for a while.

This is a deep and fascinating world to get into. Enjoy!

> It led me to a kind of branching, graph-like manner of learning...

Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.

The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.

If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/

> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression

I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.

Thanks for further recommendations. Programming Language Foundations in Agda. The Diamond Age by Neal Stephenson. I made a note to look into these.

Oh I see one of the authors of PLFA is Philip Wadler, whose name I recognize from Haskell and various papers on programming language theory. There's a Lean version of the book too. https://github.com/plfa/plfl

> Working through a proof using a proof checker .. They all come with really sophisticated tools for interacting with the compiler and the code

I have some prior experience developing a specialized code editor for a template language, and remember thinking at the time how much more potential there is for an advanced interface that supports the author, that deeply integrates with type information, documentation, examples, etc. Not just for writing programs and templates, but also for "rich text" and multimedia documents - for example, including music scores, diagrams, graphs.

Speaking of dependently typed languages (whose definition I admit I don't fully grasp yet), it reminds me of a paper I find fascinating and have read multiple times.

Physics, Topology, Logic and Computation: A Rosetta Stone - https://arxiv.org/abs/0903.0340

Again I lack the foundational concepts to really understand it to satisfaction. So I'm sure the resources you recommended will be useful on my learning journey.

Reply on news.ycombinator.com