Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.
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.
> For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type
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.
> 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.
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.
The advantage of dependent typing systems is that you can say that the arguments to a matrix multiplication function must have dimensions (m, i) and (i, n) and that result will have dimensions (m, n).
As others have said, this isn't a unique value proposition of dependent types, by all means dependent types provide a solution to this, but so do many other approaches.
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.
Yeah, right now there isn't really any example of the value tradeoff being high enough that its overcome the barriers to adoption. Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them; once that's been established, I think it's a lot easier to talk about why the approach hasn't yet become mainstream.
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.
> Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them
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.
The io issue can be solved in 2 ways:
* by returning the pair of the list and it's length.
* having functions that convert between simply typed and dependently typed lists.
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.
I haven’t entirely followed what you meant by a solution to IO, but I’m not to surprising to hear there’s a solution.
I guess the point I had in mind was, in making the case of dependent languages stuff like this may not be immediately apparent (I might be confusing the concept of total languages or programming which may not necessarily be coupled to dependent types).
> as an aside by IO I do mean anything not known at compile time (interrupts & user input, network responses, network requests [who API may change in a breaking way], database entries, etc)
Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type.
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
}
}
}
In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)
Are M and N supposed to be type parameters in your example? If so, then you don't need to store them in the struct. And once you remove that (and switch from dynamically sized vectors to statically sized arrays) your example becomes perfectly representable in Rust and C++ without dependent types
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.
Yes, the point of dependent types is that they give you the ability to do some sort of almost arbitrary (though not strictly Turing-complete) "computation" as part of type checking, which essentially dispenses with the phase separation between "compiling" and "running" code - or at least makes compile-time computation unusually powerful. So if you want to replicate the properties of dependent typing in these existing languages you'll need to leverage their existing facilities for compile-time metaprogramming.
> 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.
You can do arbitrary computations as part of type checking in C++, yet I don't think it should be considered dependently typed.
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).
The "runtime" values of a dependent type system are not quite runtime values either, because the computation is happening at compile time. When you "extract" a program from a dependently-typed to an ordinary programming language that can compile down to a binary, the dependent types are simply erased and replaced with ordinary, non-dependent types; though there may be "magic" casts in the resulting program that can only be proven correct via dependent types.
It's not that simple, right? Because the computation can actually rely on the types, so the types can't always just be erased. The complexity around knowing when the types are going to be erased or not is part of what motivated Idris 2's adoption of quantities.
QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like:
vname : Vect n a -> String
vname = "Vect " ++ show n ++ " " ++ nameOf a
Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation.
class Named a where
nameOf a : String
vname : Named a => Vect n a -> String
≡ vname : String -> Vect n a -> String
In a sense, both you and the grandparent comment are right, although it will take some time for me to explain why.
1. 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"
You can see that there's nothing here inherently that requires any of the types or values to be kept around at runtime in order to use this function. In fact, here's how you might use it:
useValue : Bool -> String
useValue b = case b of
True => "The number is: " ++ show (getValue b)
False => "The message is: " ++ getValue b
Once again, no type level terms need to be kept around at runtime to evaluate this. (Although you need a fairly intelligent typechecker in order to typecheck it.)
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 = ()
If you try to write this, you would get a classic "using a variable before it's declared" error, because nowhere in this have we defined what `b` is. Instead you'd have to write
takeValue : (b : Bool) -> pickType b -> ()
takeValue b value = ()
The type system forces you to thread the value of b through your code (as a parameter) to any function that takes a pickType b. So while every type-level term is technically erased at runtime, in the strict sense that the compiler is not adding any extra stuff to the runtime that you didn't write yourself, the value will not truly be "erased" because you are forced to pass it everywhere even though you don't use it.
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 = ()
Now this should typecheck just fine because we're not actually using b, right? The compiler can easily see that.
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
Now you can finally see where the "erasure" comes in. Any compiler can, as an optimization, erase values that are never used. And in dependently typed languages, it will often be the case that many terms are never actually used at runtime and can therefore be erased.
Thank you for spelling this out; comments like these make this website worthwhile. You've enlightened at least one person today.
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?
QTT supports three different "multiplicities". I discussed "used 0 times at runtime" (can be erased) and "used any amount of times at runtime" (cannot be erased). The remaining one is "used exactly once at runtime". These also cannot be erased, but allowing this constraint allows you to encode some very interesting things in the type system. The classic example is "resource protocols", e.g. file handles that force you to close them (and that you cannot use after closing).
The latter is what would be most useful imo. Even Matlab can type check matrix sizes with constants these days, but I often wish I could use variables to express relationships between the sizes of different dimensions of inputs to a function.
That's a good point, for example in Eigen you can do
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
Python has static typechecking which, while not perfect, works pretty well as long as you're not actually trying to circumvent it (or manipulating things "too dynamically")
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
The problem with runtime is when you make a mistake it can be a long time before you find out. Compile time means a large class of problems is prevented without perfect test coverage. On a small project it isn't a big deal but when you have hundgeds of developers over decades you will miss something
If I define a function foo which takes an (Array Float (10 5)) and then define a function bar which uses the result of calling foo with an (Array String (3 3)) then SBCL will print a warning. If I don't redefine foo and call bar with such an array then a condition will be raised. It's not quite the same as, say Rust's 'thing just won't compile', but that's due to the interactive nature of Common Lisp (I believe someone called it the difference between a living language and a dead language (though the conventional meaning of living language and dead language in programming is a bit different)).
No. You can replace them with asterisks to mean 'any length is fine', but you can't at compile time check something that's only known at runtime (granted, you could see that it can't match if the variables are, for example, an (Integer 1 10) and an (Integer 75 100)). Something you can do with variables is:
...and then you can declare variables to be something like, say, (Example-Array Boolean 5) and have it expand to (Array Boolean (20 5)). But the type declaration needs to be of the form (Array &optional element-typedimensions) where dimensions can be any of the following:
- 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.
Dependent types can do this. This is information that can be known at compile time by means of a proof that the values are what they should be (or within certain bounds) through the entire call chain.
C has such types and can guarantee that there is no out-of-bounds access at run-time in the scenarios you describe: https://godbolt.org/z/f7Tz7EvfE
This is one reason why I think that C - despite all the naysayers - is actually perfectly positioned to address bounds-safe programming.
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.
-fsanitize-bounds uses a runtime address sanitizer, surely? The program compiles fine. In a (strongly) dependently typed language, something like the following would refuse to typecheck:
int foo(int i) {
int bar[4] = { 1, 2, 3, 4 };
return bar[i]
}
The type checker would demand a proof that i is in bounds, for example
int foo(int i) {
int bar[4] = { 1, 2, 3, 4 };
if i < 4
return bar[i]
else
return 0
}
In languages with an Option type this could of course be written without dependent types in a way that's still correct by construction, for example Rust:
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
}
But ultimately, memory safety here is only guaranteed by the library, not by the type system.
You seem to be repeating what I said except you mixup strong and static typing. In a statically dependent-typed language you might expect it this not to compile, but this also depends. Run-time checking is certainly something you can combine with strong dependent typing.
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.
Update: For the interested, here are three ways to write this in C, the first using dependent type, the second using a span type, and the third using an option type. All three versions prevent out-of-bounds accesses: https://godbolt.org/z/nKTfhenoY
> using dependent type system to have "proofs" be equivalent to "types"
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?
Yeah, I just meant proposition-as-types. Sloppy terminology by me. I meant to complain about the general conflation of the "proving system" and the "typechecking system".
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.
One of the things I love about typescript is if your audacious enough you can kind of make some types like this (still a far cry from dependent types):
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.
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).
As other commenters have said, this doesn't need dependent types. Rust's const generics / C++'s non-type template parameters are enough.
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]
> Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.
What do you mean? Every class is a type, so create your own class and control what goes in.
Type checking is done statically without running the program. You don't need to execute any run-time logic to perform a check like this. What you are suggesting is a much, much weaker form of verification that doesn't require any type system at all.
I did a small small experiment in dependent typing for Python (and catching those errors before run time). It's a decently good fit, and with HM Type inference some neat things just fall out of the design.
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 :)
The dtype constraint can with pyright (and presumably others). We're still on older versions of numpy so I don't have first hand knowledge of the shape constraints.
Very interesting. My takeaway is that Dr. Paulson's answer to the question is that there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.
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.
> there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.
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.
Talking about non-necessary is IMO a cop-out: I bet we can verify systems with even fewer features that he is using, or just a different set of features that get him to the same spot. The interesting question is always whether a feature is useful enough.
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
I think the question of "necessity" is interesting, because between establishing that something is necessary vs the best option, I'd say the former is easier. And by agreeing that dependent types are not necessary (at least for certain design goals) we give space to the folks creating new provers to experiment with alternatives, which I think that is a good thing. I have been extremely impressed during my limited interactions with Lean, but I'm also vaguely aware of enough pain points to be interested in what other provers can do without being based on curry-howard.
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).
There are "provers not based on type theory", most notably the Mizar system, that still prefer types (where possible) to propositions and proof obligations. Mostly, because type checking and type inference are inherently a lot more efficient than fully-general proof checking and automated proving - hence it's convenient to have a separate formalism for the efficient subset of logic that's restricted to such "taxonomy-like" reasoning. (There is a similar case for using restricted "modalities" instead of fully-general first order logic for reasoning over "possible worlds": that too involves a significant gain in efficiency.)
(And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)
This is why dependent types work for modelling maths: you don't actually use your proofs as programs. Sure, the formalism would allow you to, but since you don't care about lemmas like "this proof and that proof are _the same_ for certain kinds of 'inputs,'" you don't run into issues with dependent types. If you try using dependent types, lemmas like the above quickly become necessary and also quickly become unprovable.
There are some theories like HoTT where it's convenient to let the same terms act as proofs while still having computational content and sometimes a distinct identity ("proof relevance"). For example a "proof" of isomorphism that might be used to transfer results and constructions across structures, where isomorphisms can be meaningfully distinct. Of course you do retain a significant subset of purely logical arguments where no computational content is ever involved and "identity" becomes irrelevant again.
>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.
I was referring to issues that arise around the need for heterogeneous equality.
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.
It's interesting just how much of the debate in modern logic boils down to aesthetic preferences. On the other hand, I guess that if there were overwhelming practical advantages, there wouldn't be much to debate...
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+).
The bigger problem with HOL (or simple type theory) is not the lack of dependencies, but rather the lack of logical strength. Simple type theory is equivalent in logical strength to bounded Zermelo set theory (i.e. ZF without Foundation or Replacement, and with Separation restricted to formulas with bounded quantifiers). This is unfortunately too weak to formalize post-WW2 mathematics in the same style as is done by ordinary mathematicians. Similarly, it does not offer a great way to deal with the size issues that arise in e.g. category theory.
I haven't followed closely, and I'm only faintly acquainted with algebraic geometry and category theory. But the TFA links to a formalization of Grothendieck schemes, which are definitely post-WW2 material, and they rely on the Isabelle's locales feature. Are you familiar with this work? How far from the "ordinary mathematician's style" is it?
You can always add axioms to improve logical strength. For example, one common approach for dealing with size issues in set theory is positing so-called 'inaccessible cardinals' which amount to something quite similar to the 'universes' of type theory.
Adding axioms to simple type theory is more awkward than adding them to a set theory like ZFC. One approach to universes I’ve seen in Isabelle/HOL world is to postulate the existence of a universe as a model of set theory. But then you’re stuck reasoning semantically about a model of set theory. Nobody has scaled this up to a large pluralist math library like Mathlib.
So, we've been down this rabbithole at Phosphor (phosphor.co) and have explored/made a couple of really big technology bets on it.
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."
Sure. Would contextualize by saying that infrastructure is a financial product: climate/industrial projects are sited in the physical world and have a hard upfront cost to produce a long term stream of cash flows, which, from a finance perspective, makes it look a lot like debt (e.g. I pay par value in order to achieve [x] cash flows with [y] risk).
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.
Reminds me a lot of AngelList, which was initially nominally just a mailing list that connected angels and early stage startups, but eventually found that the restriction was in special purpose vehicles and automated the hard legal work of making many individual funding vehicles, and thus was behind the scenes actually a legal services company, if you squint.
My abandoned PhD was in formal methods and I find dependent types to be pretty neat, but every time I've tried using a dependently typed language for anything it's always been an uphill battle.
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 would be interested to read the author's take on F. Since they are focused on math applications in this post, and F is very much focused on verified software on not on mathematics, it is a bit off topic. My (inexpert) understanding is that F* is based on an extensional type theory (different that CoC in this way) and can, but needn't, work with proof objects, since its refinement typing can just push constraints into the SMT database. I've found it pretty light weight and "opt-in" on the dependent types, and so it seems quite nice from a usability perspective IMO. But, as I say, I think it really would not address the author's question "how do we know it's right". On this point, I think the worlds of software verification and automated theorem proving for mathematics can be quite far apart.
They will absolutely learn new stuff, but that stuff won't involve math, at least not formally. The second I've used any mathematical notation to describe anything, people just tune out.
I used to think dependent types were the future, but once I actually started working on real projects, I realized they might be logically elegant and reduce errors, but the development efficiency really takes a hit. These days, I care more about solutions that are clear, maintainable, and easy to get started with. If a tool gets the job done, can scale, and the team can understand it, then it’s a good tool.
You just prove / use dependently typed languages / tla+ where it makes sense, not for everything. The latter might make sense if it's mostly automated maybe, but it takes really painful elaborate work to get full coverage and for sure most stuff really doesn't need that. I always think these formal methods + unit/integration tests cover so much that you are already far more robust than most on earth.
I think I mostly liked those type-systems that lean towards dependent, but not go all the way.
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.
> But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space.
I believe proof by reflection relies on proof objects? Georges Gonthier's proof of the four-colour theorem crucially uses proof by reflection.
Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place. If anything, the viability of proof by reflection simply shows that the divide with LCF-like checkers is not really that large.
> Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place.
I think the difference is that in a type theory you can prove the soundness of the decision procedure to be correct within the system?
From "Metatheory and Reflection in Theorem Proving: A Survey and Critique" by John Harrison, 1995:
> "No work on reflection has actually been done in HOL, but Slind (1992) has made
some interesting proposals. His approach is distinguished from those considered
previously in two important respects.
First, he focuses on proving properties of programs written in Standard ML
using the formal semantics to be found in Milner, Tofte, and Harper (1990). This
contrasts with the other approaches we have examined, where the final jump from
an abstract function inside the logic to a concrete implementation in a serious
programming language which appears to correspond to it is a glaring leap of faith. [...]"
Proving that your LCF-like tactics are sounds using the (informal) semantics of the tactic language (ML) seems cumbersome.
Furthermore I believe proof by reflection crucially relies on computation happening at the logical level in order to minimise proof checking. Harrison concludes:
> "Nevertheless it is not clear that reflection’s practical utility has yet been convincingly demonstrated."
This was from 1995, so fair enough, but Paulson should be aware of Gonthier's work, which makes me wonder if anything changed since then?
The basic idea is: You run a program F on some input x, obtain r, and then you have some sort of justification why F x = r is a theorem. There are various levels of how you can do this, one is for example that "running the program" consists of applying a curated set of (proven) rewriting rules that take you from the theorem F x = F x to the theorem F x = r by applying them only to the right hand side. That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.
So this is not a matter of dependent or static typing or not, the idea is simple and the same (e.g., I've used it for my PhD thesis in Isabelle that is from 2008), it is just a matter of how practical this is to use in your theorem prover of choice.
> That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.
I don't think it's "basically the same", because this application of the rewrite rules in a LCF-like system is explicit (i.e. the proof checking work grows with the size of the problem), while in proof by reflection in a type theory it happens implicitly because the "rewriting" happens as part of reduction and makes use of with the definitional equality of the system?
For small and medium examples this probably doesn't matter, but I would think that for something like the four colour theorem it would.
As I said, it depends on how you practically implement it.
I've used it for proving linear inequalities as part of the Flyspeck project (formal proof of the Kepler conjecture), and there I implemented my own rewrite engine for taking a set of rewrite rules and do the computation outside of the LCF kernel, for example by compiling the rules to Standard ML. You can view that engine as an extension of the LCF kernel, just one more rule of how to get theorems. In that instance, it is exactly the same.
How does the proof of correctness work in this case? Is the rewriting ultimately resorting to proof steps within the kernel like a LCF-tactic would, or is there simply an informal argument that whatever you're doing in the rewriter is correct, on par with the proof kernel itself?
There is a proof as part of my thesis that the engine is correct, but it is not formal in the sense of machine-checked.
Note that the final result of the Flyspeck project does not depend on that proof, as the linear inequalities part has later on been redone and extended in HOL-Light by Alexey Solovyev, using just the LCF kernel of HOL-Light. Which proves that using a simple LCF kernel can definitely be fast enough for such computations, even on that scale!
The claim that dependently typed languages are inherently reliant on fully written-out proof objects looks quite wrong to me. You could easily imagine a proof term with opaque typed "holes" (written `_`) where the content of each "hole" is simply replaced by a LCF-like proof script that was somehow proven (in entirely unspecified ways, having to do with the peculiar programming language that the LCF-like checker uses for its implementation - so the soundness boundary has been expanded a lot, we have given up on having an easily checkable 'kernel'!) to generate some term of the correct type, starting from its environment. Since the content is opaque, no other part of the proof development can tell what exactly was in the hole, and we can dispense with writing that part of the proof term out.
If you mean that implementing the LCF architecture OP advocates for or evaluating any one implementation of it for soundness isn't easy, I absolutely agree. But assuming that you've solved that part, making use of it within a system that otherwise uses dependent types is not that hard.
So it seems the thesis of some pretty in the know mathematicians is that the secret of dependent types is knowing when not to use them. Is that necessarily an argument against Lean or Rocq? In the sense could one simply just not use the dependent types on offer in these languages in certain circumstances, and try emulate an Isabelle proof using custom built tactics?
Sounds like for most implementations of DTs, you have to go all in which is likely overkill for many LoB apps doing CRUD with some custom logic on it. The ideal would be to be able to delegate some modules onto a separate system using DTs and the rest using your good old OOP
There are some analogies between your good old OOP and dependent types, in that a derived object in OOP has a "type" (which is reflected in its methods dictionary - it's not merely a runtime "tag") that varies at runtime based on program logic. You can implement some of this with typestate, but for full generality you need to allow for downcasts that might only become statically checkable when you do have full dependent types.
Agree with this. The punchline here is not "dependent types bad", it is "choose your battles". Isabelle/HOL pushed frighteningly far without proof objects or dependent types, from schemes to BSG, and never hit the mythical wall. What moved the needle was automation, libraries, and legible proofs, not a fancier core calculus. Lean is great, but if the toolchain bogs down and equality games leak into your day, your fancy types are like Tesla FSD: impressive demo energy, unpredictable commute (no offense to anyone who uses it regularly). Knowing when not to use them is the real superpower imho.
If you need finely indexed invariants, sure, reach for DT. For the other 95%, HOL plus type classes and locales, backed by a small kernel and big libraries, will get you to production faster and with fewer regrets. Milner's LCF insight still pays the bills. And yes, croissants are delicious, but optional axioms are a risky breakfast.
I hate titles like "Why don't you use blah-blah". Usually because blah-blah might be an acceptable (maybe good?) solution to a problem which I don't have. Let me ask in return: Why should I even care about blah-blah. If the first (two?) paragraphs don't give a clear answer to that, never mind!
For what it's worth, the article is the author arguing why they don't personally use blah-blah (Dependent Types) despite being a leading academic in the field (PLT) where blah-blah is frequently touted as the holy grail of that field, and justifies his experience using blah-blah-2 (Higher Order Logic), a tried and true "sophomoric" choice that seems dusty and crusty by comparison (literally, PLT undergrads learn how to formalize systems using blah-blah-2-reduced frequently in their sophomore years, as a way to learn SML). The rest of the article is really only interesting for the PLT/proof automation community since it is pretty niche. His conclusions is that you don't need the shiny new blah-blah to do things, often in more complicated ways, if older blah-blah-2s can do things mostly just as well and have the benefit of simplicity and ease of automation.
The title currently on HN has dropped the quotes that are in the article title: the article is not titled Why don't you use dependent types? (i.e. asking that question of the readers) but is titled "Why don't you use dependent types?" (i.e. the author quotes that question and answers it in the blog post).
Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.
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.
> For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type
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.
You can do that in python using https://github.com/patrick-kidger/torchtyping
looks like this:
There's also https://github.com/thomasahle/tensorgrad which uses sympy for "axis" dimension variables:Quick heads-up that these days I recommend https://github.com/patrick-kidger/jaxtyping over the older repository you've linked there.
I learnt a lot the first time around, so the newer one is much better :)
Ah, I would have never thought jaxtyping supports torch :)
Is there a mypy plugin or other tool to check this via static analysis before runtime? To my knowledge jaxtyping can only be checked at runtime.
I doubt it, since jaxtyping supports some quite advanced stuff:
> 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.
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.
The advantage of dependent typing systems is that you can say that the arguments to a matrix multiplication function must have dimensions (m, i) and (i, n) and that result will have dimensions (m, n).
As others have said, this isn't a unique value proposition of dependent types, by all means dependent types provide a solution to this, but so do many other approaches.
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.
Yeah, right now there isn't really any example of the value tradeoff being high enough that its overcome the barriers to adoption. Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them; once that's been established, I think it's a lot easier to talk about why the approach hasn't yet become mainstream.
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.
> Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them
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.
The io issue can be solved in 2 ways: * by returning the pair of the list and it's length. * having functions that convert between simply typed and dependently typed lists.
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.
I haven’t entirely followed what you meant by a solution to IO, but I’m not to surprising to hear there’s a solution.
I guess the point I had in mind was, in making the case of dependent languages stuff like this may not be immediately apparent (I might be confusing the concept of total languages or programming which may not necessarily be coupled to dependent types).
> as an aside by IO I do mean anything not known at compile time (interrupts & user input, network responses, network requests [who API may change in a breaking way], database entries, etc)
Cheers for your insight btw
You don't need dependent types for that, either.
Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type.
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:
In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)Are M and N supposed to be type parameters in your example? If so, then you don't need to store them in the struct. And once you remove that (and switch from dynamically sized vectors to statically sized arrays) your example becomes perfectly representable in Rust and C++ without dependent types
That's the "carry phantom types around" option, but it only gets you so far. If you never need to compute with the term, it's enough (see https://play.rust-lang.org/?version=stable&mode=debug&editio...).
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.
Yes, the point of dependent types is that they give you the ability to do some sort of almost arbitrary (though not strictly Turing-complete) "computation" as part of type checking, which essentially dispenses with the phase separation between "compiling" and "running" code - or at least makes compile-time computation unusually powerful. So if you want to replicate the properties of dependent typing in these existing languages you'll need to leverage their existing facilities for compile-time metaprogramming.
> 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.
You can do arbitrary computations as part of type checking in C++, yet I don't think it should be considered dependently typed.
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).
The "runtime" values of a dependent type system are not quite runtime values either, because the computation is happening at compile time. When you "extract" a program from a dependently-typed to an ordinary programming language that can compile down to a binary, the dependent types are simply erased and replaced with ordinary, non-dependent types; though there may be "magic" casts in the resulting program that can only be proven correct via dependent types.
It's not that simple, right? Because the computation can actually rely on the types, so the types can't always just be erased. The complexity around knowing when the types are going to be erased or not is part of what motivated Idris 2's adoption of quantities.
https://idris2.readthedocs.io/en/latest/updates/updates.html...
QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like:
Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation.In a sense, both you and the grandparent comment are right, although it will take some time for me to explain why.
1. 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
You can see that there's nothing here inherently that requires any of the types or values to be kept around at runtime in order to use this function. In fact, here's how you might use it: Once again, no type level terms need to be kept around at runtime to evaluate this. (Although you need a fairly intelligent typechecker in order to typecheck it.)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:
If you try to write this, you would get a classic "using a variable before it's declared" error, because nowhere in this have we defined what `b` is. Instead you'd have to write The type system forces you to thread the value of b through your code (as a parameter) to any function that takes a pickType b. So while every type-level term is technically erased at runtime, in the strict sense that the compiler is not adding any extra stuff to the runtime that you didn't write yourself, the value will not truly be "erased" because you are forced to pass it everywhere even though you don't use it.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`.
Now this should typecheck just fine because we're not actually using b, right? The compiler can easily see that.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.)
Now you can finally see where the "erasure" comes in. Any compiler can, as an optimization, erase values that are never used. And in dependently typed languages, it will often be the case that many terms are never actually used at runtime and can therefore be erased.Thank you for spelling this out; comments like these make this website worthwhile. You've enlightened at least one person today.
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?
QTT supports three different "multiplicities". I discussed "used 0 times at runtime" (can be erased) and "used any amount of times at runtime" (cannot be erased). The remaining one is "used exactly once at runtime". These also cannot be erased, but allowing this constraint allows you to encode some very interesting things in the type system. The classic example is "resource protocols", e.g. file handles that force you to close them (and that you cannot use after closing).
I see, so it unifies type (or I suppose term in this case?) erasure and linear typing? Thanks for the explanation!
Exactly!
The latter is what would be most useful imo. Even Matlab can type check matrix sizes with constants these days, but I often wish I could use variables to express relationships between the sizes of different dimensions of inputs to a function.
That's a good point, for example in Eigen you can do
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 is a dynamic language where everything happens at run time, including checks of variable types. So you can already do this.
Python has static typechecking which, while not perfect, works pretty well as long as you're not actually trying to circumvent it (or manipulating things "too dynamically")
I think Python actually has multiple, different static typechecking systems, depending on which checker you use.
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.)
You are slightly 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
[2]: https://peps.python.org/pep-0484/
[3]: https://typing.python.org/en/latest/spec/index.html
The problem with runtime is when you make a mistake it can be a long time before you find out. Compile time means a large class of problems is prevented without perfect test coverage. On a small project it isn't a big deal but when you have hundgeds of developers over decades you will miss something
In Common Lisp:
And the type check will return true.Compile-time checks is what's implied in virtually all these conversations.
Does that check run at compile time?
If I define a function foo which takes an (Array Float (10 5)) and then define a function bar which uses the result of calling foo with an (Array String (3 3)) then SBCL will print a warning. If I don't redefine foo and call bar with such an array then a condition will be raised. It's not quite the same as, say Rust's 'thing just won't compile', but that's due to the interactive nature of Common Lisp (I believe someone called it the difference between a living language and a dead language (though the conventional meaning of living language and dead language in programming is a bit different)).
Can you replace 10 5 and 3 3 with variable names and still get the warning without first calling the function?
No. You can replace them with asterisks to mean 'any length is fine', but you can't at compile time check something that's only known at runtime (granted, you could see that it can't match if the variables are, for example, an (Integer 1 10) and an (Integer 75 100)). Something you can do with variables is:
...and then you can declare variables to be something like, say, (Example-Array Boolean 5) and have it expand to (Array Boolean (20 5)). But the type declaration needs to be of the form (Array &optional element-type dimensions) where dimensions can be any of the following:- 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.
Dependent types can do this. This is information that can be known at compile time by means of a proof that the values are what they should be (or within certain bounds) through the entire call chain.
C has such types and can guarantee that there is no out-of-bounds access at run-time in the scenarios you describe: https://godbolt.org/z/f7Tz7EvfE This is one reason why I think that C - despite all the naysayers - is actually perfectly positioned to address bounds-safe programming.
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.
-fsanitize-bounds uses a runtime address sanitizer, surely? The program compiles fine. In a (strongly) dependently typed language, something like the following would refuse to typecheck:
The type checker would demand a proof that i is in bounds, for example In languages with an Option type this could of course be written without dependent types in a way that's still correct by construction, for example Rust: But ultimately, memory safety here is only guaranteed by the library, not by the type system.You seem to be repeating what I said except you mixup strong and static typing. In a statically dependent-typed language you might expect it this not to compile, but this also depends. Run-time checking is certainly something you can combine with strong dependent typing.
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.
Update: For the interested, here are three ways to write this in C, the first using dependent type, the second using a span type, and the third using an option type. All three versions prevent out-of-bounds accesses: https://godbolt.org/z/nKTfhenoY
I thought that this was a GCC extension(you need to use #define n 10 instead of int n = 10). Is this not the case anymore?
This is in ISO C99. In C11 it was made an optional feature but in C23 we made the type part mandatory again.
"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."
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.
> using dependent type system to have "proofs" be equivalent to "types"
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?
Yeah, I just meant proposition-as-types. Sloppy terminology by me. I meant to complain about the general conflation of the "proving system" and the "typechecking system".
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.
One of the things I love about typescript is if your audacious enough you can kind of make some types like this (still a far cry from dependent types):
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).
As other commenters have said, this doesn't need dependent types. Rust's const generics / C++'s non-type template parameters are enough.
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)
> Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.
What do you mean? Every class is a type, so create your own class and control what goes in.
Type checking is done statically without running the program. You don't need to execute any run-time logic to perform a check like this. What you are suggesting is a much, much weaker form of verification that doesn't require any type system at all.
I did a small small experiment in dependent typing for Python (and catching those errors before run time). It's a decently good fit, and with HM Type inference some neat things just fall out of the design.
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 :)
> For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.
Numpy arrays have been checkable by dtype for a little while now, and I think recent versions also support shape constraints.
Can these constraints be statically checked with mypy or a language server?
The dtype constraint can with pyright (and presumably others). We're still on older versions of numpy so I don't have first hand knowledge of the shape constraints.
Very interesting. My takeaway is that Dr. Paulson's answer to the question is that there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.
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.
> there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.
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
[3] https://github.com/hwayne/lets-prove-leftpad
Talking about non-necessary is IMO a cop-out: I bet we can verify systems with even fewer features that he is using, or just a different set of features that get him to the same spot. The interesting question is always whether a feature is useful enough.
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
I think the question of "necessity" is interesting, because between establishing that something is necessary vs the best option, I'd say the former is easier. And by agreeing that dependent types are not necessary (at least for certain design goals) we give space to the folks creating new provers to experiment with alternatives, which I think that is a good thing. I have been extremely impressed during my limited interactions with Lean, but I'm also vaguely aware of enough pain points to be interested in what other provers can do without being based on curry-howard.
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).
There are "provers not based on type theory", most notably the Mizar system, that still prefer types (where possible) to propositions and proof obligations. Mostly, because type checking and type inference are inherently a lot more efficient than fully-general proof checking and automated proving - hence it's convenient to have a separate formalism for the efficient subset of logic that's restricted to such "taxonomy-like" reasoning. (There is a similar case for using restricted "modalities" instead of fully-general first order logic for reasoning over "possible worlds": that too involves a significant gain in efficiency.)
(And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)
This is why dependent types work for modelling maths: you don't actually use your proofs as programs. Sure, the formalism would allow you to, but since you don't care about lemmas like "this proof and that proof are _the same_ for certain kinds of 'inputs,'" you don't run into issues with dependent types. If you try using dependent types, lemmas like the above quickly become necessary and also quickly become unprovable.
There are some theories like HoTT where it's convenient to let the same terms act as proofs while still having computational content and sometimes a distinct identity ("proof relevance"). For example a "proof" of isomorphism that might be used to transfer results and constructions across structures, where isomorphisms can be meaningfully distinct. Of course you do retain a significant subset of purely logical arguments where no computational content is ever involved and "identity" becomes irrelevant again.
>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.
For which reason sorry?
I was referring to issues that arise around the need for heterogeneous equality.
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.
Thanks, very clear explanation.
It's interesting just how much of the debate in modern logic boils down to aesthetic preferences. On the other hand, I guess that if there were overwhelming practical advantages, there wouldn't be much to debate...
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+).
I wouldn’t call it “aesthetics” per se.
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.
What do you mean with greater program complexity in this context?
Dependent types require additional source code.
That is true of static types in general.
The bigger problem with HOL (or simple type theory) is not the lack of dependencies, but rather the lack of logical strength. Simple type theory is equivalent in logical strength to bounded Zermelo set theory (i.e. ZF without Foundation or Replacement, and with Separation restricted to formulas with bounded quantifiers). This is unfortunately too weak to formalize post-WW2 mathematics in the same style as is done by ordinary mathematicians. Similarly, it does not offer a great way to deal with the size issues that arise in e.g. category theory.
I haven't followed closely, and I'm only faintly acquainted with algebraic geometry and category theory. But the TFA links to a formalization of Grothendieck schemes, which are definitely post-WW2 material, and they rely on the Isabelle's locales feature. Are you familiar with this work? How far from the "ordinary mathematician's style" is it?
You can always add axioms to improve logical strength. For example, one common approach for dealing with size issues in set theory is positing so-called 'inaccessible cardinals' which amount to something quite similar to the 'universes' of type theory.
Adding axioms to simple type theory is more awkward than adding them to a set theory like ZFC. One approach to universes I’ve seen in Isabelle/HOL world is to postulate the existence of a universe as a model of set theory. But then you’re stuck reasoning semantically about a model of set theory. Nobody has scaled this up to a large pluralist math library like Mathlib.
[This comment was responded to by the author in an addendum to their post.]
So, we've been down this rabbithole at Phosphor (phosphor.co) and have explored/made a couple of really big technology bets on it.
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.
Can you expand on
"We build non-dilutive growth engines for industrial and climate technology companies by creating high quality development pipelines for institutional capital."
Sure. Would contextualize by saying that infrastructure is a financial product: climate/industrial projects are sited in the physical world and have a hard upfront cost to produce a long term stream of cash flows, which, from a finance perspective, makes it look a lot like debt (e.g. I pay par value in order to achieve [x] cash flows with [y] risk).
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.
Reminds me a lot of AngelList, which was initially nominally just a mailing list that connected angels and early stage startups, but eventually found that the restriction was in special purpose vehicles and automated the hard legal work of making many individual funding vehicles, and thus was behind the scenes actually a legal services company, if you squint.
What made you choose TypeDB? What kind of performance are you getting out of it?
Just spotted this! We (I'm CTO at TypeDB) just released some early benchmarks: https://typedb.com/blog/first-look-at-typedb-3-benchmarks/
My abandoned PhD was in formal methods and I find dependent types to be pretty neat, but every time I've tried using a dependently typed language for anything it's always been an uphill battle.
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 would be interested to read the author's take on F. Since they are focused on math applications in this post, and F is very much focused on verified software on not on mathematics, it is a bit off topic. My (inexpert) understanding is that F* is based on an extensional type theory (different that CoC in this way) and can, but needn't, work with proof objects, since its refinement typing can just push constraints into the SMT database. I've found it pretty light weight and "opt-in" on the dependent types, and so it seems quite nice from a usability perspective IMO. But, as I say, I think it really would not address the author's question "how do we know it's right". On this point, I think the worlds of software verification and automated theorem proving for mathematics can be quite far apart.
oh, people will learn new stuff. they do all the time.
i think they simply thought it was not worth it. in fine we have limited time on this planet.
They will absolutely learn new stuff, but that stuff won't involve math, at least not formally. The second I've used any mathematical notation to describe anything, people just tune out.
> The second I've used any mathematical notation to describe anything, people just tune out.
You stopped speaking their language
Great, I love this stuff.
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
I used to think dependent types were the future, but once I actually started working on real projects, I realized they might be logically elegant and reduce errors, but the development efficiency really takes a hit. These days, I care more about solutions that are clear, maintainable, and easy to get started with. If a tool gets the job done, can scale, and the team can understand it, then it’s a good tool.
You just prove / use dependently typed languages / tla+ where it makes sense, not for everything. The latter might make sense if it's mostly automated maybe, but it takes really painful elaborate work to get full coverage and for sure most stuff really doesn't need that. I always think these formal methods + unit/integration tests cover so much that you are already far more robust than most on earth.
I think I mostly liked those type-systems that lean towards dependent, but not go all the way.
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.
> But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space.
I believe proof by reflection relies on proof objects? Georges Gonthier's proof of the four-colour theorem crucially uses proof by reflection.
Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place. If anything, the viability of proof by reflection simply shows that the divide with LCF-like checkers is not really that large.
> Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place.
I think the difference is that in a type theory you can prove the soundness of the decision procedure to be correct within the system?
From "Metatheory and Reflection in Theorem Proving: A Survey and Critique" by John Harrison, 1995:
> "No work on reflection has actually been done in HOL, but Slind (1992) has made some interesting proposals. His approach is distinguished from those considered previously in two important respects. First, he focuses on proving properties of programs written in Standard ML using the formal semantics to be found in Milner, Tofte, and Harper (1990). This contrasts with the other approaches we have examined, where the final jump from an abstract function inside the logic to a concrete implementation in a serious programming language which appears to correspond to it is a glaring leap of faith. [...]"
Proving that your LCF-like tactics are sounds using the (informal) semantics of the tactic language (ML) seems cumbersome.
Furthermore I believe proof by reflection crucially relies on computation happening at the logical level in order to minimise proof checking. Harrison concludes:
> "Nevertheless it is not clear that reflection’s practical utility has yet been convincingly demonstrated."
This was from 1995, so fair enough, but Paulson should be aware of Gonthier's work, which makes me wonder if anything changed since then?
The basic idea is: You run a program F on some input x, obtain r, and then you have some sort of justification why F x = r is a theorem. There are various levels of how you can do this, one is for example that "running the program" consists of applying a curated set of (proven) rewriting rules that take you from the theorem F x = F x to the theorem F x = r by applying them only to the right hand side. That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.
So this is not a matter of dependent or static typing or not, the idea is simple and the same (e.g., I've used it for my PhD thesis in Isabelle that is from 2008), it is just a matter of how practical this is to use in your theorem prover of choice.
> That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.
I don't think it's "basically the same", because this application of the rewrite rules in a LCF-like system is explicit (i.e. the proof checking work grows with the size of the problem), while in proof by reflection in a type theory it happens implicitly because the "rewriting" happens as part of reduction and makes use of with the definitional equality of the system?
For small and medium examples this probably doesn't matter, but I would think that for something like the four colour theorem it would.
As I said, it depends on how you practically implement it.
I've used it for proving linear inequalities as part of the Flyspeck project (formal proof of the Kepler conjecture), and there I implemented my own rewrite engine for taking a set of rewrite rules and do the computation outside of the LCF kernel, for example by compiling the rules to Standard ML. You can view that engine as an extension of the LCF kernel, just one more rule of how to get theorems. In that instance, it is exactly the same.
How does the proof of correctness work in this case? Is the rewriting ultimately resorting to proof steps within the kernel like a LCF-tactic would, or is there simply an informal argument that whatever you're doing in the rewriter is correct, on par with the proof kernel itself?
There is a proof as part of my thesis that the engine is correct, but it is not formal in the sense of machine-checked.
Note that the final result of the Flyspeck project does not depend on that proof, as the linear inequalities part has later on been redone and extended in HOL-Light by Alexey Solovyev, using just the LCF kernel of HOL-Light. Which proves that using a simple LCF kernel can definitely be fast enough for such computations, even on that scale!
The claim that dependently typed languages are inherently reliant on fully written-out proof objects looks quite wrong to me. You could easily imagine a proof term with opaque typed "holes" (written `_`) where the content of each "hole" is simply replaced by a LCF-like proof script that was somehow proven (in entirely unspecified ways, having to do with the peculiar programming language that the LCF-like checker uses for its implementation - so the soundness boundary has been expanded a lot, we have given up on having an easily checkable 'kernel'!) to generate some term of the correct type, starting from its environment. Since the content is opaque, no other part of the proof development can tell what exactly was in the hole, and we can dispense with writing that part of the proof term out.
That's how F* (FStar) works, right? You may write out proof objects manually but most of time they are inferred by SMT
That doesn't sound that easy.
If you mean that implementing the LCF architecture OP advocates for or evaluating any one implementation of it for soundness isn't easy, I absolutely agree. But assuming that you've solved that part, making use of it within a system that otherwise uses dependent types is not that hard.
So it seems the thesis of some pretty in the know mathematicians is that the secret of dependent types is knowing when not to use them. Is that necessarily an argument against Lean or Rocq? In the sense could one simply just not use the dependent types on offer in these languages in certain circumstances, and try emulate an Isabelle proof using custom built tactics?
Sounds like for most implementations of DTs, you have to go all in which is likely overkill for many LoB apps doing CRUD with some custom logic on it. The ideal would be to be able to delegate some modules onto a separate system using DTs and the rest using your good old OOP
There are some analogies between your good old OOP and dependent types, in that a derived object in OOP has a "type" (which is reflected in its methods dictionary - it's not merely a runtime "tag") that varies at runtime based on program logic. You can implement some of this with typestate, but for full generality you need to allow for downcasts that might only become statically checkable when you do have full dependent types.
Agree with this. The punchline here is not "dependent types bad", it is "choose your battles". Isabelle/HOL pushed frighteningly far without proof objects or dependent types, from schemes to BSG, and never hit the mythical wall. What moved the needle was automation, libraries, and legible proofs, not a fancier core calculus. Lean is great, but if the toolchain bogs down and equality games leak into your day, your fancy types are like Tesla FSD: impressive demo energy, unpredictable commute (no offense to anyone who uses it regularly). Knowing when not to use them is the real superpower imho.
If you need finely indexed invariants, sure, reach for DT. For the other 95%, HOL plus type classes and locales, backed by a small kernel and big libraries, will get you to production faster and with fewer regrets. Milner's LCF insight still pays the bills. And yes, croissants are delicious, but optional axioms are a risky breakfast.
Same reason I don't use a variety of other good programming ideas: the tools I use don't support it usefully.
The juice isn't worth the squeeze.
The real skill is knowing when not to make something dependent otherwise you just slow yourself down.
Is it me or do dependent types look really similar to the axiom of choice?
I hate titles like "Why don't you use blah-blah". Usually because blah-blah might be an acceptable (maybe good?) solution to a problem which I don't have. Let me ask in return: Why should I even care about blah-blah. If the first (two?) paragraphs don't give a clear answer to that, never mind!
For what it's worth, the article is the author arguing why they don't personally use blah-blah (Dependent Types) despite being a leading academic in the field (PLT) where blah-blah is frequently touted as the holy grail of that field, and justifies his experience using blah-blah-2 (Higher Order Logic), a tried and true "sophomoric" choice that seems dusty and crusty by comparison (literally, PLT undergrads learn how to formalize systems using blah-blah-2-reduced frequently in their sophomore years, as a way to learn SML). The rest of the article is really only interesting for the PLT/proof automation community since it is pretty niche. His conclusions is that you don't need the shiny new blah-blah to do things, often in more complicated ways, if older blah-blah-2s can do things mostly just as well and have the benefit of simplicity and ease of automation.
In coding terms this is the equivalent of Donald Knuth writing a blog post titled “Why I don’t use version control.”
The title currently on HN has dropped the quotes that are in the article title: the article is not titled Why don't you use dependent types? (i.e. asking that question of the readers) but is titled "Why don't you use dependent types?" (i.e. the author quotes that question and answers it in the blog post).