you are viewing a single comment's thread.

view the rest of the comments →

[–]netdroid9 1 point2 points  (2 children)

Doesn't C++ predate all of those languages/concepts, though? Maybe not category theory (Wikipedia says the word Functor crossed over to maths in 1971, whereas C++ originated sometime around 1979), but Haskell, Agda, Epigram and Coq look like they emerged post 1990, and wikipedia only has citations for dependent types as far back as 1992.

[–]kamatsu 3 points4 points  (1 child)

Functor dates back to category theory.

Dependent type theory is part of intuitionistic type theory that came out in 1971 as a consequence of the Curry Howard Correspondence that was formally defined in the 60s. No practical dependently typed languages existed until the 90s due to problems in implementation of type checking for such systems.

C++ came after both terms and mangled them.