[hiker]

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.