1
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ I am admittedly not familiar with the "typed/untyped" debate. Could you perhaps provide an explanation or point towards a source that explains it? Can you explain what you mean by "less defined" or "quite restrictive"? $\endgroup$
    – mdxn
    Oct 4, 2013 at 1:07
  • $\begingroup$ The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency. - wikipedia $\endgroup$
    – zcaudate
    Oct 4, 2013 at 3:02
  • $\begingroup$ It's a gut instinct, but I feel that there problems out there where the type system is actually restricting rather than helping to solve the actual problem. There are always ways around anything of course, and most haskellers will say to me... You are just thinking about it the problem in the wrong way.. I'm trying to find evidence for the contrary. There are articles about why type systems are better than untyped but I haven't found many the other way - apart from anecdotal evidence $\endgroup$
    – zcaudate
    Oct 4, 2013 at 3:10
  • $\begingroup$ Sorry if I was unclear: I do understand Godel's theorems. I do not know specifically what difference your gut is telling you that suggests a potential problem with typed vs. untyped languages. This was why I asked you about the typed vs. untyped "debate" specifically and did not ask for an explanation of Godel's Incompleteness theorem. $\endgroup$
    – mdxn
    Oct 4, 2013 at 4:04
  • $\begingroup$ sorry about my response, my question really isn't about the actual debate but on the consequences of such a theorem. I've updated my question.. but here are two links: against dynamic - stackoverflow.com/questions/42934/…, for dynamic sites.google.com/site/steveyegge2/is-weak-typing-strong-enough $\endgroup$
    – zcaudate
    Oct 6, 2013 at 2:57

2 Answers 2

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Type systems for Turing-complete languages are not logically consistent. It’s true that there will be programs which give no type errors but are rejected by the typechecker, but such programs must exist only because of Rice’s theorem (basically, nontrivial properties of the behavior of programs in Turing-complete languages are undecidable). $\endgroup$
    – Blaisorblade
    Sep 16, 2018 at 19:57
5
$\begingroup$

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").

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.