>goes through type theory, not philosophy.
You’re going to be very surprised when you look up the origins of type theory.
You’re going to be very surprised when you look up the origins 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
Prelude Data.Function> :t fix id
fix id :: a
In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.