> But dependent types (and static types in general) don't exist at runtime!
That isn't entirely true when it comes to dependent types and can be seen as a design choice. Types can depend on values and those values can often exist at runtime. Erasure only applies to parts we can determine are not computationally relevant.
For example `Vec n a`. The `n` is a natural number you may need at runtime, such as to get the length without walking the list. A dependent pair `Sigma(n : Nat). Vec n a` carries that `n` at runtime as ordinary data.
In fact many dependently typed languages have techniques, such as quantitative type theory, to assert what is needed at runtime.
You've exactly described the answer, but to people who don't know much about dependent types, this may be a little unclear. The point is that there are two sorts of dependent types.
When people who don't know much about them think of dependent types, they are probably thinking of functions, which can take a value on the left hand side to be used in the type on the right. Confusingly, these are normally called "dependent products" in the type theory. However since this is confusing and they are generally written with a capital Pi, they are often just referred to as "Pis". For example
Pi x:nat . Vec x string
is a function that takes a nat (non-negative number) and returns a Vector whose length is that nat and which is encoded in the type.
On the other hand, you are talking about pairs (confusingly: "dependent sums", here "sum" being something like a union/enum in type theory), often called "Sigmas". These are pairs (2-tuples) of values in which the type of the second value depends on the value of the first. So, your example, a pair where the vector length is held in the first element and the vector itself in the second. In this contrived example, Vector may not know its own length at runtime, so we need to package them up together.
Sigma x: nat . Vec x string
These are both "dependent types", but people who are only passingly familiar with them might mostly know about the first.
(Why are functions "dependent products" and pairs "dependent sums"? I've never understood this but I've heard hand-wavy explanations that infintitary products are functions and infinitary sums are products ¯\(ツ)/¯)
Pairs in general (ie binary products) are always sums. A pair type `X * Y` is a multiplication, which is equivalent to `enum {Y y_x0,Y y_x1,Y y_x2,...}` or `Y + Y + Y + ...`, effectively a sum type where the descriminant of the enum is a X, and each case of the enum contains a Y. This is equivalent to how 3 * 7 = 7 + 7 + 7, where you have three terms of size seven.
Similarly, functions in general (ie (binary) exponentiations) are always products. A function type `X -> Y` (or `Y ^ X`) is a exponentiation, which is equivalent to `struct {Y y_x0,Y y_x1,Y y_x2,...}` or `Y * Y * Y * ...`, effectively a product (or latent array) type where the index of the 'array' is a X, and each element of the 'array' is a Y. This is equivalent to how 7 ^ 3 = 7 * 7 * 7, where you have three factors of size seven. (Note that functions have the exponent/argument first and the base/result second.)
All of the above applies without dependent types. Dependent types let the `Y` type depend on which value of type X is involved. (That is, the Y type depends on the X value.)
This is such a short sighted take. Number theory was considered beautifully useless for centuries, and now it’s the backbone of the cryptography that secures every bank transaction. We don't know where the pursuit of knowledge will take us.
Thinking in such a utilitarian way feels like a flavor of Meditations on Moloch.[1] Just look at how short-term, quarter-to-quarter thinking is affecting the economy and the lived experience of every human on earth. It’s horrible.
>
This is such a short sighted take. Number theory was considered beautifully useless for centuries, and now it’s the backbone of the cryptography that secures every bank transaction
If you refer to RSA or Diffie-Hellman: the number theory that it is based on is from 17th to at most 19th century, i.e. it precedes modern number theory.
I do consider modern number theory to be fascinating and do claim that many results from it could have huge applications in society, but the argument that parts of modern asymmetric cryptography is based on number theory is rather an argument that we don't need any number theory research anymore because these insanely old results that are used in cryptography have already been known for centuries - so no new research is necessary. :-(
We didn't know what investigations were going to lead to RSA or Diffie-Hellman and any particular breakthrough is standing on a mountain of prior work that didn't have an obvious application but nonetheless was necessary to get to a breakthrough.
Honestly I can't believe I even need to state this. Its literally how science works..
> We should evaluate research by the research itself
Why is this the argument when someone challenges your source, but when it comes to someone else's source your argument is:
> This is research from a labor advocacy group, with the explicit aim of the organization to advocate for this sort of thing. This doesn't mean the research is is automatically invalid, but it is bias worth mentioning.
Not necessarily, not in some of the most useful ways of simply having a significantly more capable way of automating research & experimentation of many sorts. Anyone with a dataset and a laptop with a decent gpu, or pretty reasonably priced API or subscription to access models that don't even need to be frontier level, they can setup a loop for intelligent iteration through countless analytical methods, subset analysis, enriching the data with other sources, search and retrieval of research literature to cross reference results of analysis with other findings and write a basic summary for the person to review, look for alternative methods for analysis.
Yes, not everyone will be able to launch a swarm of agents and a few billion tokens, but scientific research has always had areas where the most advanced tools were beyond the reach of every scientist who might like to have access.
Only for about five more years. In 7-10 years the price of memory and compute should drop by 80-90%. In ten years the bleeding edge 14,000 token/s machines and 4TB memory is going to look quaint, "that stuff can't even bootstrap a kernel and entire (usable) posix-compliant OS in less than a week" vs the future of "the computer updates it's firmware in real time to meet the needs of the current task"
But why would these same trends not also vastly improve the capabilities of the top hardwares and ability of the trillion-dollar companies to leverage their economies of scale?
I'm all for the idea that AI capabilities can be democratized and help ordinary scientists outside of a handful of labs. But it seems there would need to be some checks against Big Tech and it won't happen by just letting the free market do its thing.
The margins on GPUs are estimated at 80% right now. So the price would most likely drop by 70% just by building the additional manufacturing capacity. Assume some modest reductions in cost and the price should drop by 80-90%.
The only reason computers are so expensive is that demand is so out of control.
Crashed demand after one of the big AI labs (probably Anthropic because they focus way too hard on expensive frontier models) become insolvent and every trader panic sells tech stocks.
Even if that doesn't happen, a lot of non AI companies like Oracle that invested too much on data centers will fail and have to sell their hardware. Big models are getting too expensive for a lot of smaller businesses so demand migrates to less GPU hungry ones. That means Oracle might be left with excess capacity.
And we also get more supply because high margins attract investment. 7 years is a realistic time frame to build new DRAM fabs and packaging, it might take even less if governments treat it as a security issue.
Maybe but are those limitations more or less onerous than the current requirements to contribute to scientific research? It remains to be seen I think.
Not only resources being controlled by a few organizations, but the noise of all of the people who have used AI to “discover” something novel, when they don’t understand the domain in the first place. When everyone is discovering something, but what they are publishing is either incorrect or already known, how do you wade through the slop to find the gems (maybe academic publishing was already filled with human slop, though).
All journals will be brute-forced to death. Not the greatest time to be Phd student. And many people have no shame. They just use agents to make whole papers. Those who don’t, will double-guess their life choices.
The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
I've never used Rocq but from what I understand the core type theory is also a version of CIC and like Lean it has strong support for tactics. Rocq defaults to an axiom free core making it constructive. Classical axioms like propositional extensionality and axiom of choice are things you opt into deliberately.
From what I understand the Lean community leans (haha) classical and uses these axioms throughout mathlib. By staying constructive you guarantee that closed proofs can, in principle, evaluate to a canonical form.
> The secret of Lean4 is that its actually a great programming language
Kind of feels like you have to specify for what here, as no programming language is just "great at everything", they all have their places (except Clojure and children which is great at everything obviously). Say I run shell commands, obviously a PL based around proofs will be way too much, compared to if I want to create aircraft stabilizer with movable control surfaces.
If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.
"sufficiently capable" is doing an insane amount of heavy lifting here. Like you can only interpret a theory into another one if the target is at least as strong as the source and even then "to and from" is a MUCH stronger condition that most pairs of theories do not satisfy.
Then when a translation exists the proofs can blow up in size to where you lose feasibility and understandability even tho they are technically still proofs.
Regardless of all that, I wasn't even bringing up 1lab because of the choice of language or type theory. I bring it up as an example of a pro-human way of presenting formalization.
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.
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.
> 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.
> 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.
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.
Nice. Your github repository on lambda calculus looks quite comprehensive. If you add detailed notes on each of the items, you could easily turn it into a book titled, "Type Theories using Lambda Calculus with Implementations in Haskell" ;-)
That isn't entirely true when it comes to dependent types and can be seen as a design choice. Types can depend on values and those values can often exist at runtime. Erasure only applies to parts we can determine are not computationally relevant.
For example `Vec n a`. The `n` is a natural number you may need at runtime, such as to get the length without walking the list. A dependent pair `Sigma(n : Nat). Vec n a` carries that `n` at runtime as ordinary data.
In fact many dependently typed languages have techniques, such as quantitative type theory, to assert what is needed at runtime.
reply