All started around 1930, when mathematicians discovered the λ-calculus. It was Turing complete, so we wrote programs on it. Everything was great, until the first program crashed and the first paradox was found. The world was in flames, so humans looked for better.
Around 1940, the simple type was discovered. It solved everything: math was consistent again, programs stopped crashing. People were happy, until someone tried to make a linked list.
"Why do I need to duplicate my entire codebase?" - asked the angry developers.
At this point, half of humanity gave up on types. A duck religion was born. The other half looked for better.
Around 1970, polymorphism was discovered. Now we could create generic lists without giving up on types! C evolved to C++, Java was born, Go missed the ride, Haskell did it without hands. Great times. Everyone was happy again. Except for these mathematicians. What they even want to do? Prove things with code? Blasphemy.
Around 1980, dependent types were discovered. Hooray! Now we can do computations at the type level. It was like polymorphism on steroids. You want a function to return a string or an int, depending on the input? Now you could do that. You want a Vector to statically track its length? Why not! So we can also prove theorems, right! Hell yeah! Wait, no. Not quite.
"Where is induction?" - asked the mathematicians.
"We don't know! Give us some time!" - said the type theorists.
"Computers suck. I'm going back to paper." - said the mathematicians.
The type theorists then went on a decade-long journey to figure out what was missing. After long heated debates, they hired a senior developer who fixed everything with a hardcoded mess of specific cases, and, no less than 100k lines of code after, Coq was born, with a native system of inductive system capable of covering every case mathematicians could possibly need?
"Will you give us a chance now?" - begged the type theorists.
"Sure! This looks decent now. I've just proved two functions have the same input/output pairs! Now I can just assume they're equal, right?" - asked the mathematicians.
"FUCK YOU" - said the type theorists, before entering another decade-long journey to fix the inherent inflexibility of the systems they built.
(That's where we are now.)
. . .
All started around year 42, when the aliens invented the first Interaction Net computer. Programs ran in parallel, everything was fast, progress was rampant... until the first program crashed. So they added a node for type annotations.
A -> B ::= θf λx {(f {x: A}): B}
The simple type was born, solving all problems! Until someone tried to make a linked list... So they let the return type to depend on the input.
Π(x: A). B[x] ::= θv λx {(v {x: A}): (B x)}
Polymorphism was born. Dependent types came for free!
"Can we prove theorems now?" - asked an Alien mathematician.
"Well, not quite? But watch this." - replied an Alien type theorist.
Πf(x: A). B ::= θv λx {(v {x: A}): (B x f)}
Now the return type can depend on the function itself, and the first proof assistant was born.
"That's cool! I've just proved two functions have the same..."
"Say no more."
inet_funext
: (T U : *) (f g : T -> U) (h : ∀(t: T) (Eq U (f t) (g t))) : (Eq (T -> U) f g)
= λT λU λf λg λh λP λa (h $t (∀(u: U) (P (∀($t: T) u))) a)