In Further Praise of Dependent Types
golem.ph.utexas.edu
golem.ph.utexas.edu
Okay...
> x:A ⊢ B(x): Type
I'm lost.
- There is a variable called `x` in scope.
- `x` is known to have type `A`.
- `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this.
Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
https://en.wikipedia.org/wiki/Gymnasium_(Germany)
And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof.
It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs.
> I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course.
A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations?
They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
I've never heard of "sequent calculus" before, and I don't expect anyone I know to have heard it. Apparently it's not calculus.
> They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
I don't think universities are watered down because they don't teach notation that most people don't know and find obscure. My university is famous for a difficult admissions process, tough courses that most people only learn 2/3 of the material, and grading curves calibrated so getting 60% on exams is enough for a B or A.
----
https://en.wikipedia.org/wiki/Sequent_calculus
Wikipedia says "Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments."
I didn't learn "every statement is conditional" logic involving turnstiles, I learned something where the assumptions were given in the problem, and each line was proven based on the previous lines, which boiled down to the initial givens.
https://en.wikipedia.org/wiki/Gymnasium_(school)
> I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.
Dismissing this foreign language aspect as easy to learn doesn't get to the heart of the matter. Is it really too much to be ask to be taught in vernacular English rather than foreign Church Latin, er, Mathematical Notation?
[1] Assuming that you don't get an answer like "a monad is a monoid in the category of endofunctors," which unfortunately does tend to be the case for higher mathematical concepts.
An opinion that’s largely held by programmers and not people who actually do maths. You learn the symbols and notation as you go and it very quickly becomes understandable. I certainly Duns I have less issues understanding mathematical notation than I do reading some programming languages.
> how is one supposed to search for ℜ? That’s chalkboard R, represents the real numbers. Searching “fancy R mathematics” (in Duck duck go) nets a page that explains what the chalkboard R, N, P, Q and C symbols all mean.
> Is it really too much to be ask to be taught in vernacular English Mathematical texts used to be written in plain English without the notation, it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
The "people who actually do maths" will almost by definition exclude anyone who has issues understanding the notation. You need to look at the latter group of people to work out if the notation is unnecessarily obtuse.
> it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
As a counterexample, consider the proof that undirected Hamiltonian cycles is NP-complete, by reduction from directed Hamiltonian cycles. Karp's original paper says literally just this:
N = V × {0, 1, 2}
A = {{<u,0>, <u,1>}, {<u,1>, <u,2>} | u ∈ V} ∪ {{<u,2>,<v,0>} | <u,v> ∈ E}
By contrast, a vernacular English description would look like this:
Replace every node in the directed graph with a set of three nodes in a line. Gather all the incoming edges to the first node, and all the outgoing edges to the last node. Every path that visits every node exactly once must reach the middle node by starting at the first node and going through to the last node, and thence to the first node of a corresponding subsequent node, so every Hamiltonian path in the undirected graph is a Hamiltonian path in its directed counterpart.
More verbose, yes, but (IMO) easier to grasp.
This 'argument' always just seems to be a thinly veiled excuse to avoid putting in the bare minimum effort required to understand a complicated topic.
I mean, what's why I said almost?
> It's also not particularly difficult to pick up.
Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.
[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...
It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules.
The top-left rule on page 52 says that given that:
- In context Gamma, T1 = T2 where both have kind *
- If x : T1 is added to the context Gamma, K1 = K2
you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2.
A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used.
The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
Gamma |- exp : A
This is a common pattern that says that exp has type A when the contents of Gamma are in scope.
Gamma |- exp1 = exp2 : A
This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope.
I've found that most type system rules follow the same format more or less.
Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)
-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.
(You can probably tell I didn't enjoy the experience...)
The article "Why 'Functor' Doesn't Matter" [0] is relevant.
In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1].
For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me.
[0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma...
[1] https://math.stackexchange.com/questions/286077/implies-righ...
[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...
To describe this with Python's type hints, for example, you would write this:
def B(x: A) -> Type:Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on).
However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.
The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C).
On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`).
The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".
"It's Time for a New Old Language" – Guy Steele [video] (youtube.com)
https://www.youtube.com/watch?v=dCuZkaaou0Q
https://news.ycombinator.com/item?id=15473199
He calls it "Computer Science Metanotation".
Okay
So imagine how you would design a language with dependent types that would match the productivity of Interface Builder when designer GUIs.
Or a being able to provide something like Unity.
Not only the whole interactive design process, but also the ability to ship UI components that can be integrated into the designer's toolbox.
How would a drag & drop action, or mouse click binding an event to a slot, reflect into the existing type definitions.
Plus that was just one example, I can pick Delphi, Smalltalk, Windows Forms/WPF/UWP, VB or plenty others as example.
I guess you did this with Idris?
When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further.
When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront.
There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax):
f : Int -> Int -> Bool
data T : Int -> Int -> Type where
Tz : T 0 x
Ts : T a b -> T (a + 1) (b + 1)
g : (x : Int) -> (y : Int) -> Maybe (T x y)
The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it.
It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.
There is always a necessary distinction between specification and implementation: if there weren't, one of them would have no value. We often suggest that the intent of a piece of code should be specified in comments, and this is in that category. This way, the compiler can read your comment and figure out if it needs updating! Languages without dependent types work this way too - but you have to try very hard indeed to be eloquent in type signatures, and being able to talk about values lets you say a bit more.
Coming onto your second point: if the function is only valid for some set of values of the given type, why is it 'not really called for' to create specialised types for it? If you call it with something else and it runs, it will be a bug. Newtypes or wrappers are common patterns.
I think that most mainstream typed languages have common constructs to offer that 'A or a B' value you want: this is solved via inheritance, `Either`, `Result`, or `std::variant`.
My point about newtypes and wrappers is that they are almost pure overhead for helper functions. There is a reason why we don't define precise types for each of our intermediate calculations in general, and this doesn't change when we move those computations to a separate function.
Finally, inheritance is not a real solution for returning A or B, with inheritance I can only return a C that both A and B derive from, and this C often doesn't exist and can't be added post-hoc. What you normally do is go for Object or void*, which is much closer to dynamic typing than inheritance. And most mainstream typed languages don't have Either or Result. C++ with std::variant is the only exception, I forgot that it was added. BTW, I should be more explicit - the way I see it, the mainstream typed languages are Java, C#, C, C++, and maybe Go.
You can achieve this with other languages (e.g. Smalltalk), but many of the most popular languages feel more like inanimate tools (some very good ones!).
- The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling.
- Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I've written about my experience doing that here: https://www.stephanboyer.com/post/134/my-hobby-proof-enginee...
- But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free!
- Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser!
- Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error.
- Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language.
- Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism).
- Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution.
Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.
Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
The Coq language groups types into two categories: Set and Prop. Prop, which (informally speaking) contains all your proofs, is erased when you "compile" your Coq code into another language like Haskell or OCaml. This is something people have thought about quite a bit already.
I think the reason people aren't using dependent types has more to do with the ecosystem around these languages: the tooling, the libraries, the documentation, the tutorials, ... None of that is where it needs to be for these languages to be appealing to industry programmers.
> Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
I have serious doubts about this. Rust, like every mainstream language, already has too many features that overlap with what dependent types give you for free. Also, Rust is not a functional language (some people claim it to be, but there are side effects everywhere!), so it would be a bit of an impedance mismatch.
As much as I'd like to believe in this unicorn language that is better than all the others, experience has taught me to be skeptical of that. Programming is used to solve so many different kinds of problems that it's hard to imagine a one-size-fits-all solution, but I won't claim it's impossible.
Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
The issue is that I think all of the current dependently typed languages don't have zero-cost abstraction and compiled code efficiency as a primary goal, they are designed for research or as machine-checked proof systems.
There's also the issue that some features may not compose well, e.g. Rust's ability to mutate a single field in place (needed for zero-cost since CPUs can do that with a store instruction) doesn't compose very well with dependent types because that can change the type of other fields, and also linear types (again needed to fully use CPUs) don't go well with having proof-like types that refer to other values, etc. All this seems fixable, but it seems quite involved to find the most general and ergonomic solution.
You don't need linear types for in-place updates. You can use a monad (which is another thing you can easily do with dependent types) to express the side effect of doing mutations. Then you can compile that monadic Coq code to Haskell, which then compiles to efficient machine code that actually does in-place updates.
Though, perhaps it is also worth mentioning that Idris 2 has both linear types and dependent types.
Regarding the need for automatic memory management: yes, most dependently typed languages have a garbage collector, but many "real" programming languages have garbage collectors and programmers are still happy to use them. I don't know why everyone in this thread is so concerned about performance. Dependently typed code can compile to reasonable machine code without any stretch of the imagination.
> Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
Memory layout is certainly something that needs to be dealt with, but compilers can monomorphize where possible to generate fast code with unboxed types in many cases. I don't think this is the main blocker for dependent types. I've written dependently typed code that easily outperforms the dynamically typed code I write for production at work (by at least an order of magnitude). In fact, dependent types can be used to guarantee that certain things don't need to be checked at runtime, which can in some cases give even better performance than what you'd get in a regular old statically-typed language.
I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.
Mandatory GC is not a zero-cost abstraction (it is ridiculously inefficient and unnecessary in general), and a language with mandatory GC is a non-starter as a universal language. C programs (like web browsers) are starting to have new code written in a different language only now that Rust is available as the first zero-cost non-GC safe language.
Yes, dependent types improve performance by eliding checks, but that's only likely to be a net win if the rest of the compilation is optimal.
Even more, the performance limitations of most GC languages have more to do with the lack of good ways of writing code which simply doesn't allocate, rather then the problem of collection. GCs are often faster than malloc/free, but not as fast as simply not allocating/freeing anything.
Finally, it's important to remember that there are algorithms that are significantly more difficult to implement without a GC tahn with a GC. Even simple compare-and-swap atomic sets can require many times more code and care to implement if you have to handle cleanup of temporaries as well.
malloc/free is fast with a moving GC, but moving is not, and if an object is never moved it's likely that it should not have been allocated on the heap in the first place.
The cmpxchg problem is solvable by epoch-based reclamation libraries (RCU, crossbeam-epoch, etc.), and while a traditional GC also solves it, it's not necessary.
AIUI, dependently-typed languages don't really have a fixed phase distinction between "compile time" and "run time". The type checking pass can involve execution of "run time" code (this is one way to understand why these languages are generally not Turing complete), and "run time" code may be required to somehow build complex code like a JSON parser "on the fly", depending perhaps on user input.
In practice, some systems have a "code extraction" component that's intended to filter out the "irrelevant" parts of the code and transpile it to a conventional programming language, which obviously reintroduces a separate "run time" deployment step. This could definitely be done using, e.g. Rust, provided that the issues due to a lack of general GC in that language are addressed too.
Do it! There's a dearth of such a format for the more "hi-falutin" topics out there. Doesn't need polish or total precision either, "us programmers" can deal with IRC-like stream-of-tid-bits.
Question: if compile-time evaluation of language X is fully-featured-fully-capable X (sans IO / syscalls, say) with "types as values" (of compile-time-only type `type`, say), ie. given Turing-completeness, where you can have functions that build up and return types --- do you still need complex theoretical type system constructs like "dependent"/"refinement"/"row-polymorphic" etc natively.. say at compile time, given sufficient prim builtins and storage-describing "prim types" (int, arr, tup) any further type-details are described programmatically. I suppose this leads to being able to express predicates that the type checker can "evaluate" in tandem with those compile-time evals..
I haven't gotten to the dependent types part yet. I find most tutorials one these languages start with the theory up front. I'm taking a more pragmatic tack by demonstrating the language through examples building on familiar learning patterns of writing simple programs first and working your way up.
It is a neat way to write programs!
- how much of the burden of writing the proof falls on me, and how much falls to the compiler? I've seen Idris type signatures, and I didn't find them super easy to grasp.
- What are the full range of things I can express? What can't I express, even with dependent types? I come from math, so I'm used to have infinite flexibility to define what goes into my set of possible values. When I first learned Haskell I was surprised that I couldn't easily define types like "this set, modulo an equivalence relation". Or something like: "Int, but only even numbers".
- how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through? I already run into this all the time in Haskell, with Maybes thay I _know_ to contain a value, or Lists that I know not to be empty. There is a real trade off between writing clear code, and wrapping/unwrapping values all the time everywhere.
Length-indexed vectors is a great example, because it is such a non-story in math, and yet for programming I have to front-load all this complexity to express something so utterly trivial. It's part infuriating, part enlightening how surprisingly tricky seemingly small things can be.
The compiler in Idris can do some magic, but usually the burden is mostly on you to write proofs. Idris (and similar languages) have assistance in editors to help you automatically write code and proofs.
> What are the full range of things I can express?
Dependent types as present in Idris, Coq, Agda, etc. can serve as a foundation for mathematics, so… pretty much anything!
For your example, most such languages don't have quotient types, so you'll still need to use setoids or similar to model quotients.
> - how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through?
It's pretty much the same situation as Haskell or Rust, but I think having to write fromJust / unwrap is great. It tells you when you're reading the code exactly what assumption has been made, and it doesn't seem awfully burdensome.
> yet for programming I have to front-load all this complexity to express something so utterly trivial.
What's "all this complexity" that you're referring to?
Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
> I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing?
Most of my experience with dependent types comes from a language called Coq (as well as one of my side projects, which is a new dependently typed language). Agda and Idris (among others) also support this style of programming. Idris goes further and uses dependent types to provide amazing IDE capabilities. There's a YouTube video where the designer of Idris used his IDE to automatically implement matrix transposition (the type was so precise that the compiler discovered the only sensible implementation).
Unfortunately I think the world is still lacking a good general-purpose dependently typed programming language suitable for production use (though I'm working on it).
> Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
Generally speaking, dependently typed languages are functional. The fundamental concept in dependently typed languages is the dependent function type, also called "pi type" or (confusingly) "dependent product type". So, the whole thing is based on functions and their types. One could imagine some kind of hybrid language, but combining dependent types and implicit side effects (like imperative languages have) is an active area of research.
I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)`
Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...
1 - 'compile-time' code execution of some arbitrary code with the result of that execution then being available at run time
2 - a specific type of function which takes the AST of some language and then uses some procedural methodology to mutate/alter that AST transforming it into some other AST
I would say, that while dependent types can be a useful basis for covering several of the typical use cases of macros, they do not without some additional structure, provide a firm proof/type theory for the whole scope of macros.
I would suggest that the most sound attempts at describing the computational phenomena encapsulated by the most common usage of the term 'macro' would be found in the following: a) implementation of Temporal Logic (per Frank Pfenning's interpretation) for description of compile-time code execution and b) implementation of Modal Logic, describing multi-staged compilation, as in Davies and Pfenning
So, I would not say that dependent types can eliminate macros, but they do cover a chunk of the areas that are often implemented by macros, including generics and other type based compile time code patterns.
I don't think dependent types are essential for giving language a formal semantics though, I think discourse representation theory has a more direct approach.
Haha, this got a laugh out of me :). While this is true in principle, the reality can be quite messy! For instance, there seems to be little consensus about what the words "vector", "contravariant", "covariant", and "coordinate" should mean on the Wikipedia page [1] claiming to explain just that!
[1] https://en.wikipedia.org/wiki/Talk:Covariance_and_contravari...
A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }".
My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.
Which is not possible for any language targeting real machines since floats have fixed precision.
The example normally given is, for instance, being able to define a function whose return type depends of the value (not the type) of its argument – for example, a function which takes in a natural number and returns an array with exactly the length of that natural number.
Dependent types are one of the axes in the Lambda Cube: https://en.wikipedia.org/wiki/Lambda_cube – types have terms the way sets have elements (roughly speaking) and so you can [1] relate types with types (type operators), you can [2] relate terms with types (polymorphism), and lastly [3] types with terms (dependent types) – giving a three-dimensional type theoretic space.
(Btw, I don't know if it even makes sense to talk about relating terms with terms or what feature of type theory captures this notion – so don't ask me!)