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, this definition is not allowed.
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:
one can produce proof of everything that is just an infinite loop.In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.