does godel's incompleteness theorem shed any light on dynamic vs typed languages? [closed]

Question

I'm clojure user myself. I'm trying really hard to learn haskell and to better understand the type system. However, I feel that trying to 'type' everything is quite restrictive when the problem or the data is less defined.

I intuitively feel that godel's incompleteness theorem offers some insight into the typed/untyped debate. What are some simple problems that may trip up the typing system but not untyped ones?

---

According to http://en.wikipedia.org/wiki/Type_theory. "The types of type theory were invented by Bertrand Russell in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This theory of types features prominently in Whitehead and Russell's Principia Mathematica. It avoids Russell's paradox by first creating a hierarchy of types, then assigning each mathematical (and possibly other) entity to a type. Objects of a given type are built exclusively from objects of preceding types (those lower in the hierarchy), thus preventing loops."

Godel's theorem invalidated Principia Mathematica. What consequence does it have on Type Theory.

Answer 1

So, Godel's incompleteness theorem says, if I recall correctly, that any sufficiently powerful logical system cannot be both consistent and complete. A good type system is concsistent, so it must be incomplete, that is, it contains well-typed programs which will fail to compile.

In practice, this isn't often a problem. Why? Because type inference and type checking are two separate things. Type inference is usually undecidable, and involves taking an expression and determining its type. Most type inference algorithms are imperfect, that is, they can't always infer the type of an expression.

Type-checking, on the other hand, is easy. If you know the types of expressions in a program, it's dead easy to determine if it's well typed. So, all you have to do is, find the cases where the type inference engine needs help, explicitly tell it what the types are, and it's good to do the checking. This is why Haskell and ML still let you write signatures.

As DW says, any problem you can solve in Clojure you can solve in Haskell. A type checker doesn't change this at all. All a type checker does is, at compile time, finds things which could cause bugs at runtime.

For the most part, if it works on Clojure but not in Haskell, it means there will be a bug in your Clojure code. Dynamic typing is popular because you can write quickly, but dangerous because the compiler doesn't tell you when you mess up.

Answer 2

Haskell is Turing-complete. That means, any computation that can be expressed in Clojure, can also be expressed in Haskell (and vice versa). Consequently, there is no difference in the expressibility of the two languages. This remains true despite the type system.

I'm not aware of any insight that Godel's incompleteness theorem offers into whether statically typed languages are "better" than untyped languages (for some unspecified definition of "better").