3 ms·
>goes through type theory, not philosophy. You’re going to be very surprised when you look up the origins of type theory.
by Sangermaine 8y ago
>goes through type theory, not philosophy.
You’re going to be very surprised when you look up the origins of type theory.
- hiker 8y agohttps://en.wikipedia.org/wiki/History_of_type_theory https://en.wikipedia.org/wiki/History_of_type_theory Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs terminate. The solution to this problem these days is to use a purely functional programming language with dependent types (e.g. Homotopy Type Theory, Lean). Haskell, for example, being a practical functional programming language, is logically inconsistent. Using the fix function: fix :: (a -> a) -> a fix f = let x = f x in x one can produce proof of everything Prelude Data.Function> :t fix id fix id :: a that is just an infinite loop. In a logically consistent functional language such as Lean https://leanprover.github.io https://leanprover.github.io, this definition is not allowed.