A dependent type is a type that depends on a value. What something is depends on something else; What something is is derived from something else – with computation. What dependent types are are calculations of type structure.
Unbounded, this becomes intractable like all unbounded computational expressivity. So that’s what modern dependent type systems need to solve—and they do. There exist formal results that frame the computational expressivity of dependent type systems and make perfectly feasible and tractable the task of deriving significantly complex types. Automatically.
The Idris language is a great example of where we’re heading.
The reason I’m more interested in this sort of thing rather than Copilot is that dependent type systems are based on formally rigorous methods. You end up with formally verified programs, by way of the same mechanisms that allow you to derive them automatically. They’re also easier to compose, for the same reasons.
Edwin Brady’s Idris demonstratons on Youtube show a bit of what’s possible. In one, the compiler automatically writes a formally-correct type-directed matrix multiplication function. In another, run-length encoding and decoding functions are generated from a type definition.
The book Type-Driven Development with Idris is a great read. Mind-expanding.
Programming is automation. The automation of automation is… dependent types.