Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1.

Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU

Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side.

Now allow arbitrary programs to be types. We'll call these type programs.

Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing.

For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself.

Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis.

In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true.

You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here.

I find the whole thing fascinating myself, but haven't gone too deeply into it.

(BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)

In a very abstract way, it is a way to encode relationships between types on the type system.

You can express things like how are you allowed to consume elements from a data structure, how many elements a specific data structure is allowed/expected to have, how their form looks like and so forth, all at compile time.

Thus working as kind of profs that certain functions can only be called if the conditions are met.

https://en.wikipedia.org/wiki/Type_system

Most typed programming languages will allow you to form a pair of type (Integer, Integer), and reject programs which try to return something like (Integer, Float).

Dependently typed languages might allow you to declare a type (n, m) where n and m are integers, and n < m, and will reject programs which attempt to return pairs with n > m.

The key step here is that this rejection is done during compilation, and so while your program is running you can be absolutely sure that n < m.

Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class.

As an example this is Haskell's core language:

  data Expr b
    = Var   Id
    | Lit   Literal
    | App   (Expr b) (Arg b)
    | Lam   b (Expr b)
    | Let   (Bind b) (Expr b)
    | Case  (Expr b) b Type [Alt b]
    | Tick  (Tickish Id) (Expr b)
    | Type  Type
    | Cast  (Expr b) Coercion
    | Coercion Coercion

  data Type
    = TyVarTy   Var
    | LitTy     TyLit
    | AppTy     Type Type
    | ForAllTy  !TyCoVarBinder Type
    | FunTy     Type Type
    | TyConApp  TyCon [KindOrType]
    | CastTy    Type KindCoercion
    | CoercionTy Coercion

If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax.

And this is Lean core language (a dependently type language):

  inductive expr
  | var         : nat → expr
  | sort        : level → expr
  | const       : name → list level → expr
  | mvar        : name → name → expr → expr
  | local_const : name → name → binder_info → expr → expr
  | app         : expr → expr → expr
  | lam         : name → binder_info → expr → expr → expr
  | pi          : name → binder_info → expr → expr → expr
  | elet        : name → expr → expr → expr → expr
  | macro       : macro_def → list expr → expr

Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types.

So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time.

In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages.

That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.

Two sentence summary that glosses over a lot of things:

1. Types can be used to classify programs.

2. Dependent types can be used to classify programs by running other programs on them.

If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read:

https://mitpress.mit.edu/books/little-typer

When the type of a function mentions its parameter, it’s a dependent type (just like a normal function that mentions it’s parameter is a “dependent value”, so to speak.

Usually though one speaks of dependent types only when the parameter can range over not just types.