Posted by baruchel 1 day ago
The Curry-Howard correspondence, using dependent type system to have "proofs" be equivalent to "types", is powerful, but it can be really confusing. From a human point of view, there is a huge difference between "Your proof is wrong" and "You wrote a statement that fails typechecking".
Intuitively, when you make an error with types, it should be something fairly trivial that you just read the error and fix it up. When you make an error in a proof, it's understandable if it's very complicated and requires thought to fix. The natural UI is different.
So I agree with the author that the greatest benefit of Lean is not its typesystem per se, but its community. Specifically the fact that Lean's library of mathematics, mathlib, is organized like an open source community with pull requests. Whereas Isabelle's library of mathematics, the AFP, is organized like a scientific journal with referees.
I'm working on a dependent type system at the moment for a new theorem prover - Acorn, at https://acornprover.org - and my hope is to combine the good points of both Lean and Isabelle. It's nice that Lean has the power to cleanly express the simple dependent types that mathematicians often use, like vector spaces or quotients. But if you use dependent types too much then it does get complicated to debug what's happening.
To clarify, as long as 5 and 10 are constants, this is entirely possible in C++ and Rust^1, neither of which are dependently typed (or at most are dependently typed in a very weak sense). In general, neither can ensure at compile time that an index only known at runtime is in bounds, even if the bounds themselves are statically known. A proper dependently-typed language can prevent runtime out-of-bound errors even if neither the indices nor the bounds are known at type check time.
^1 And weakly in many other languages whose builtin array types have compile-time bounds. But C++ and Rust let user-defined generic types abstract over constant values.
looks like this:
def batch_outer_product(x: TensorType["batch", "x_channels"],
y: TensorType["batch", "y_channels"]
) -> TensorType["batch", "x_channels", "y_channels"]:
return x.unsqueeze(-1) * y.unsqueeze(-2)
b, x, y = sp.symbols("b x y")
X = tg.Variable("X", b, x)
Y = tg.Variable("Y", b, y)
W = tg.Variable("W", x, y)
XWmY = X @ W - YI learnt a lot the first time around, so the newer one is much better :)
def full(size: int, fill: float) -> Float[Array, "{size}"]:
return jax.numpy.full((size,), fill)
class SomeClass:
some_value = 5
def full(self, fill: float) -> Float[Array, "{self.some_value}+3"]:
return jax.numpy.full((self.some_value + 3,), fill)Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types. It's fully possible to define a matrix that uses a generic type as the index for each dimension that doesn't allow expressing values outside the expected range; it would just be fairly cumbersome, and the usual issues would creep back in if you needed to go from "normal" integers back to indexes (although not if you only needed to convert the indexes to normal integers).
I find that the potential utility of dependent types is more clear when thinking about types where the "dimensions" are mutable, which isn't usually how I'd expect most people to use matrixes. Even a simple example like "the current length of a list can be part of the type, so you define a method to get the first element only on non-empty lists rather than needing them to return an optional value". While you could sort of implement this in a similar as described above with a custom integer-like type, the limitations of this kind of approach for a theoretically unbounded length are a lot more apparent than a matrix with constant-sized dimensions.
You can do this in C++ & Rust, and I've done something similar in Typescript. The point of the comment you're replying to is kind of making the point that pitches for dependent types probably should give examples of something not already solved by other systems (not that you can't do this in DT). See:
> Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types.
In order to adopt DT, you need to pay a combined cost of productivity loss in terms of established tooling and choose to forgo any human capital which is no longer applicable once you start using a language with Dependent types, and a loss of time spent learning to use a language that has dependent types, which almost certainly has a smaller library ecosystem than most mainstream languages without DT.
For that reason it's worth considering what examples illustrate a benefit that outweighs all the above costs. I don't think it's enough to simply assert some moral basis on safety when clearly salaries for work done in unsafe languages are already considerably high.
For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list. If I read input from a user, I might be able to do an initial check that a list of items is non-empty as part of the constructor for the type, but what happens if I want to start popping off elements from it? In practice, this seems like it would either force you to go back to manually checking or only ever process things in a purely functional way to avoid defining behavior that vary based on state that isn't known. If you're willing to take this approach, having the compiler enforce it is great! You have to be willing to use this approach often enough for it to be worth picking a language with dependent types though, and in practice it doesn't seem likely that people would choose to even if they were more aware of the option.
There's probably some truth in that (I'm probably in this camp as well), though I feel sometimes adoption of things like this can often be a communication problem, and the people who understand these technologies the most may struggle to identify what aspect of these technologies are valued more by the people they are trying to pitch them too.
Like they might even find those aspects boring and uninteresting because they are so deep into the technology, that they don't even think to emphasis them. Which feels like a similar story where a technology early to the party didn't take off until someone else came back to them later (like fat structs and data oritented design gaining some interest despite early versions of these ideas date back to Sketchpad (1963)).
> For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list
Yeah this example crossed my mind as well, it's not immediately clear how you deal with IO or data the result of inputs from the outside world. Although I have feeling this has to be a solved problem.
I guess more generally with API design, sometimes you don't really know the system you want to model yet so there's diminishing returns in being overly precise in how you model it if those things are subject to change. Not sure how substantive a concern this is when weighing up using dependent types, but it is something that crosses my mind as an outsider to all this dependent type stuff.
However the ergonomics could probably be improved.
The API design is a real real issue, which is why I think something more "gradual" would be best.
You can express a lot just carrying phantom types around and using basic pattern matching: in Rust I can express multiplication, concatenation of vectors to matrices, and inverses of square matrices, using phantom types.
But I can't say this, or anything remotely like it:
struct Matrix<M: u32, N: u32, T> {
dim: (M, N),
// imaginary dependently typed vectors
cells: Vec<M, Vec<N, T>>,
}
impl<M, N, T> Matrix<M, N, T> {
fn mul<O: u32>(&self, &other: Matrix<N, O, T>) -> Matrix<M, O, T> {
let cells: Vec<self.m, Vec<other.o, T>> = do_the_thing();
Matrix {
// any other values in dim, or a different type in cells, would be a type error
dim: (self.m, other.o),
cells
}
}
}
You could use statically sized arrays, but if you can't have the static sizes of the arrays as your type parameters, but instead some arbitrary M and N, the size of your data structure isn't part of your type and you don't get the statically verified safety benefits. You also can't express M + N or anything of the sort.
Neither C++ nor Rust really hurt for expressivity, though.
> A proper dependently-typed language can prevent runtime out-of-bound errors even if neither the indices nor the bounds are known at type check time.
Yes, but the way this is done is by threading a proof "this index is within bounds" throughout the code. At runtime (e.g. within 'extracted' code, if you're using common dependently-typed systems), this simply amounts to relying on a kind of capability or ghost 'token' that attests to the validity of that code. You "manufacture" the capability as part of an explicit runtime check when needed (e.g. if the "index" or "bounds" come from user input) and simply rely on it as part of the code.
It seems to me that dependent typing strictly requires going from runtime values to types.
(You can parametrize types by runtime values in c++ in a trivial sense, by enumerating a finite set a compile time and then picking the correct type at runtime according to a runtime value, still I don't think it counts as the set of valid types would be finite).
https://idris2.readthedocs.io/en/latest/updates/updates.html...
vname : Vect n a -> String
vname = "Vect " ++ show n ++ " " ++ nameOf a
class Named a where
nameOf a : String
vname : Named a => Vect n a -> String
≡ vname : String -> Vect n a -> String1. There is an extremely strict sense of the concept of type erasure where the grandparent comment is right.
2. But in a practical sense of "I don't want these values in my binary", you are right.
So to resolve this confusion, it might be best to say exactly what dependent types are. "Dependent types", for all their mystery, are just a combination of three simple ideas:
1. What if you could: write functions that return types?
2. What if you could: say that the value of the input to a function can determine the type of the function's output?
3. What if you could: say that the value of the first thing in a tuple can determine the type of the second thing in the tuple?
For a concrete example, here is a very simple dependently typed function
-- write functions that return types!
pickType : Bool -> Type
pickType True = Nat
pickType False = String
-- the return type changes based on input!
getValue : (b : Bool) -> pickType b
getValue True = 42
getValue False = "hello"
useValue : Bool -> String
useValue b = case b of
True => "The number is: " ++ show (getValue b)
False => "The message is: " ++ getValue b
As nice as this is, the story gets a little less clean once you look at taking a dependent argument as a value. For example, we could not write this:
takeValue : pickType b -> ()
takeValue value = ()
takeValue : (b : Bool) -> pickType b -> ()
takeValue b value = ()
Obviously, this might be undesirable. So then you might further ask, "what are the situations in which we don't really need to enforce this constraint? when can a function take a dependent value without needing to know the values it depends on?"
That is where QTT comes in, as developed in Idris 2. Idris actually takes it a step further than we need for this conversation. For our purposes, all we need to do is say that there are two options for arguments into a function: arguments that are never used at runtime, and arguments that may or may not be used at runtime.
Let's say a function never uses one of its arguments. Then, clearly, as long as the compiler knows what that argument is, it doesn't have to actually write runtime code to pass it to the function. Let's allow the user of our made up language to prefix types that are never actually used at runtime with `0`.
takeValue : (0 b : Bool) -> pickType b -> ()
takeValue b value = ()
And in fact, we can even pass b to another function as long as that function also marks its b as 0. (We know it will never actually get used so it's fine.)
takeValuePrime : (0 b : Bool) -> pickType b -> ()
takeValuePrime b value = takeValue b value
You hinted that there's more to QTT (or its implementation in Idris?) than this. Could you elaborate a bit on what these other features are, and what their purpose is?
Eigen::Matrix<float, 10, 5>
I just really want it in Python because that's where I do most of my matrix manipulation nowadays. I guess you also would really like it to handle non-constants. It would be nice if these complicated library functions like
torch.nn.MultiheadAttention(embed_dim, num_heads, dropout=0.0, bias=True, add_bias_kv=False, add_zero_attn=False, kdim=None, vdim=None, batch_first=False, device=None, dtype=None)
would actually typecheck that kdim and vdim are correct, and ensure that I correctly pass a K x V matrix and not a V x K one.
Python itself only gives you type annotations, but doesn't specify what they are supposed to mean.
(I think. Please correct me if I am wrong.)
Python does allow you to put anything in annotations. ( pep 3107 that defines type annotations says that explicitly [1]).
But it also defines a type checking annotations, which is a specific convention for using pep 3107 annotations. Type annotations were introduced in PEP 484 and updated in a lot of subsequent peps. The python typing system is fully specified in [3].
It does have several implementations, although the reference implementation is mypy
[1]: https://peps.python.org/pep-3107/#rejected-proposals
(defparameter *test-array*
(make-array '(10 5)
:element-type 'Float
:initial-element 0.0))
(typep *test-array* '(Array Float (10 5)))
Does that check run at compile time?
(defvar *example-dimension* 20)
(deftype Example-Array (element-type minor-dimension)
`(Array ,element-type (,*example-dimension* ,minor-dimension)))
- An asterisk, which means anything goes.
- A number, which means the array needs to have that many dimensions (so an (Array Fixnum 2) is a 2-dimensional array of fixnums).
- A list of numbers, asterisks, or a combination of the two, where an asterisk means 'this dimension can be anything' and the numbers mean exactly what you would expect.
Maybe something like that would be possible with Coalton, but I haven't played around a lot with that yet.
Often in dependently-types languages one also tries to prove at compile-time that the dynamic index is inside the dynamic bound at run-time, but this depends.
int foo(int i) {
int bar[4] = { 1, 2, 3, 4 };
return bar[i]
}
int foo(int i) {
int bar[4] = { 1, 2, 3, 4 };
if i < 4
return bar[i]
else
return 0
}
fn foo(i: 32) -> i32 {
let bar = [1, 2, 3, 4];
bar.get(i) // returns Option<i32>, not a raw i32
.unwrap_or(0) // provide a default, now we always have an i32
}
Implementing bounds checking that returns option types (which can also implement in C) is not exactly the same thing. But dependent typing can be more elegant - as it is here.
I remember being able to use telescopes [1] in Haskell long time ago, around 2012 or so.
[1] https://www.pls-lab.org/en/telescope
Haskell was not and is not properly dependently typed.
https://github.com/AKST/analysis-notebook/blob/main/lib/base... (Line 38)
It type checks, but I haven’t gotten a lot of mileage out of this (so far at least). I did something similar for vectors, which has been useful for when I destructure the elements, and it preserves that through vector operations.
https://github.com/AKST/analysis-notebook/blob/777acf427c65c...
The same is actually applies true for matrices, I wrote the multiplication to carry the new size into the output type
https://github.com/AKST/analysis-notebook/blob/777acf427c65c...
That said I mostly use this for square matrixes in web GL so you’re mostly working with square matrixes.
As an aside, this source is from a toy project largely more for leisure and fun, I don’t know if something like this would be suitable for a larger more data oriented project (at least in trend of how I represent data here).
Do you mean proposition as types? And proof has a program?
Or do you see it at somewhat a higher order, since values are proof for a type, and types can perhaps be proof at a higher level if they are first class citizen in the language?
(Which makes me think that dependent types is really a stairway between two type systems?)
Just wondering, since I had never personally seen it described in that fashion.
Other question: What is the function and runtime treatment of dependent types? Can they be instantiated on the spot by runtime values? A bit like defining/declaring functions that return arrays of runtime-known length? Does it involve two aspects of type checking? compile and runtime? Implementation-wise, doesn't it require too many indirections?
Generally in dependent type systems you are limited in some way in what sort of values a type can refer to. The fancy type checking happens at compile time, and then at run time some or most of the type information is erased. The implementation is tricky but the more difficult problem IMO is the developer experience; it involves a lot of extra work to express dependent types and help the compiler verify them.
Even in languages with dependent types, people tend to find it overly cumbersome to use them for actually prevent runtime errors like out-of-bounds access; they instead tend to save the dependent types for (1) data structure invariants that can be propagated easily, and (2) verification after the program has been defined.[0][1]
[0]: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
[1]: https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pd... ("Programming with dependent types: passing fad or useful tool?" by Xavier Leroy in 2009; things might have changed since 2009)
What do you mean? Every class is a type, so create your own class and control what goes in.
Numpy arrays have been checkable by dtype for a little while now, and I think recent versions also support shape constraints.
But the real challenge is deciding how much of Python's semantics to preserve. Once you start enforcing constraints that depend on values, a lot of idiomatic dynamic behavior stops making sense. Curious what ways there are to work around this, but I think that's for a person better at Python than I :)
I would have liked to read more about Lean's alleged performance issues, and the issues around intentional equality. For the latter, I understand one can run into the need for heterogeneous equality (https://lean-lang.org/doc/reference/latest/Basic-Proposition...) when types are propositionally equal, but not definitionally equal. It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason. If something may be stated as a theorem after the fact instead of putting it in the type, that was my preference.
Certainly there is something strongly aesthetically appealing about dependent type theory. The unification of programs and proofs and the natural emergence of independent proof objects. I am open to the idea that overly-dogmatic insistence on a type-theoretic basis to a theorem prover could lead to pragmatic issues, but I'd need to see more examples to be convinced there is a better foundation.
Anyway, I agree with Dr. Paulson's point that dependent types aren't necessary to verify interesting systems. He talked more of pure mathematics, but I am more interested in software verification. I work heavily in ACL2 which, not only does it not have dependent types, it doesn't have static typing at all! It is, however, also a first order logic and the both of these facts can sometimes be frustrating. Various libraries have been introduced to simulate typing and higher-ordered reasoning.
I think that, at least in software engineering, his point has not been disproven. Isabelle (classical) has a great track record in software verification. I don't see it as something inherently inferior to Rocq (dependently typed), which also has a great track record.
Lean doesn't have a great focus (yet?) on software verification. And Agda is also not mainstream on large-scale industrial verification. One interesting thing would be to compare Concrete Semantics [1] (Isabelle) vs The Hitchhiker's Guide to Logical Verification [2] (an approximate rewrite in Lean). I am still starting with the second one, so I can't say much yet, but it might be too basic to draw any conclusions.
Ultimately, refinement types embedded in general-purpose languages might be a more pragmatic approach. Leftpad proofs using Rust Creusot, Dafny, or LiquidHaskell are quite straightforward [3], but again this is just a toy problem.
[1] http://concrete-semantics.org
[2] https://github.com/lean-forward/logical_verification_2025
You get into types at the end. And sure, we don't need static types. Just like, outside of verification, we don't need garbage collection, or bounds checking, or even loops. But are the features useful? What takes us to the goal faster? And remember that also changes depending on who is doing the tasks. A lot of differents in tooling selection, across all kinds of work, come down to preference, not general utility, and they sure have nothing to do with necessity
Anyway, for what its worth, I generally agree that static typing is preferable. It is just a little more complicated in the context of theorem provers (as opposed to general-purpose, non-verification programming languages) where, for provers not based on type theory, propositions and proof obligations can be used where we might otherwise use types. This can be nice (generally more flexible, e.g. opportunities for non-tagged sums, easy "subtyping"), but also can be a downside (sometimes significant work reproducing what you get "for free" from a type system).
(And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)
For which reason sorry?
As an example, consider the dependent vector type `Vec n`, which is an array of length `n`. An `append` function would have type `{n m: Nat} -> Vec n -> Vec m -> Vec (n + m)`. That is, it takes an array of length `n`, and array of length `m`, and produces an array of length `n + m`.
Now imagine that you want to show that `append` is associative. That is, for all `x: Vec n`, `y: Vec m`, and `z: Vec o`, you have `append (append x y) z = append x (append y z)`. We can't prove this because we can't even state the theorem; it is not well-typed. The left-hand side has type `Vec ((n + m) + o)`, while the right-hand side has type `Vec (n + (m + o))`. Those two length values are of course propositionally equal, but they are not definitionally equal in type theories like Lean or Rocq's. That is, the equality is not immediately apparent to the type checker, and so requires a proof. But even with a proof, the statement is ill-typed (because equality is "intentional", not "extensional"). So you have to use a heterogeneous equality operator which allows you to compare two values whose types are propositionally but not definitionally equal. This equality is generally more difficult to work with.
Obviously this whole problem goes away if we use a non-dependent array type, as opposed to something length-indexed like this `Vec` type. So unless there is some reason to use the indexed type (e.g., perhaps the compiler can emit more efficient code), I would just use the non-indexed types and prove separately anything I want to know about the length.
BTW, here's a "discussion paper" by Paulson and Leslie Lamport about typing in specification laguages from 1999: https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulso.... Paulson represents the "pro-type" view, but note that since that paper was written, there have been developments in mechanised theorem proving of untyped formalisms, including in Lamport's own (TLA+).
More like “No free lunch.”
You can gain advantages, e.g. more complete compile time guarantees, but at disadvantages, e.g. greater program complexity, or longer compile times.
The subjectivity is whether the tradeoff is “worth” it.
That is true of static types in general.
The most unique/useful applications of it in production are based on combining dependent types with database/graph queries as a means. This enables you to take something like RDF which is neat in a lot of ways but has a lot of limitations, add typing and logic to the queries, in order to generally reimagine how you think about querying databases.
For those interested in exploring this space from a "I'd like to build something real with this", I'd strongly recommend checking out TypeDB (typedb.com). It's been in development for about a decade, is faster than MongoDB for vast swaths of things, and is one of the most ergonomic frameworks we've found to designing complex data applications (Phosphor's core is similar in many ways to Palantir's ontology concept). We went into it assuming that we were exploring a brand new technology, and have found it to work pretty comprehensively for all kinds of production settings.
"We build non-dilutive growth engines for industrial and climate technology companies by creating high quality development pipelines for institutional capital."
When you drive past a solar project on the side of the road, you see the solar technology producing energy. But in order for a bank to fund $100M to construct the project, it has to be "developed" as if it were a long-term financial product across 15 or so major agreements (power offtake, lease agreement, property tax negotiations, etc). The fragmentation of tools and context among all the various counterparties involved to pull this sort of thing together into a creditworthy package for funding is enormously inefficient and as a result, processes which should be parallelize-able can't be parallelized, creating large amounts of risk into the project development process.
While all kinds of asset class-specific tools exist for solar or real estate or whatever, most of them are extremely limited in function because almost of those things abstract down into a narrative that you're communicating to a given party at any given time (including your own investment committee), and a vast swath of factual information represented by deterministic financial calculations and hundreds if not thousands of pages of legal documentation.
We build technology to centralize/coordinate/version control these workflows in order to unlock an order of magnitude more efficiency across that entire process in its totality. But instead of selling software, we sell those development + financing outcomes (which is where _all_ of the value is in this space), because we're actually able to scale that work far more effectively than anyone else right now.
When I used to do F# for a living, I was really pushing for using F*, but it was impossible to get any buy-in from coworkers because the learning curve was comparatively steep. I probably should have pushed a bit more, but I figured that I'd potentially have more success trying to push people to use TLA+ (though that was also unsuccessful).
That was unsuccessful as well, and I've come to the (admittedly very cynical conclusion) that software engineers, generally speaking, will never learn anything new if it involves "math" in any way, shape, or form. Once I realized that, it became much easier to lower my expectations of my coworkers.
i think they simply thought it was not worth it. in fine we have limited time on this planet.
You stopped speaking their language
See here for a summary of the many results of the author and team's research project on formalization:
https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/
Especially interesting for me is the work on formalizing quantum computing algorithms and theorems (open access):
https://link.springer.com/article/10.1007/s10817-020-09584-7
Purescript might be favourite? Even by default you get more power than i.e. vanilla Haskell, with row-types. But then you can get type-level list, typelevel string, even typelevel regex! And you use these through type-classes in a kind of logic-programming way.