[arh68]

> Can a dependent type system catch all type errors at compile time?

I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

> because the value of getKeyboardInput could be anything

That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration:

    x = (parseInt(getKey) :: Int(>=0, <=10))

Then you type-annotate everything you can, marking every non-annotated expression as wild:

    w = ... :: Int(>=0, <=10)
    x = ... :: Int(>=0, <=2)
    z :: Int(>=0, <=20)
    y = w * x                 -- :: Wild
    z = y                     -- compiler should Scream!

Asking the compiler to infer arbitrary type declarations seems hard. I think y probably shouldn't be inferred as :: Int(0<=..<=20) unless there is a rule somewhere that Int(a<=..<=b) * Int(c<=..<=d) = .. :: Int(f<=..<=g).

The work still needs to be done (no magic bullet here), but we should be able to use the computer to generate well-defined type combinations.

[leoc]

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

IIRC dependently-typed languages dodge this bullet by not being completely Turing-complete (as 'twere).

[chriswarbo]

Not quite. Many dependently-typed languages aren't Turing-complete, but that's no how they 'dodge this bullet'.

Think about the following Java code:

    public int getMyInt() {
      return getSomeOtherInt();
    }

How hard does Java have to work to figure out whether getMyInt is well-typed? Does it have to solve the halting problem? No. It just checks the information that you have given it. If you wrote that getSomeOtherInt has return type "int" then getMyInt will type-check. If you gave it some other type, it won't type-check. If you didn't give it a type, it will complain about a syntax error. At no point will Java try to write your program for you (which would hit against the halting problem). The same is true in dependently-typed languages, except the types happen to be much stronger. You still have to write them down, write down values of those types, write conversion functions when you need to combine different types, etc.

Incidentally, if a language is Turing-complete, it actually becomes really easy to get a program to type-check; we just write infinite loops everywhere, which leads to logical fallacies ;) That's why many dependently-typed languages aren't Turing-complete (although many are; eg. those which distinguish compile-time terms from run-time terms, like ATS).

[Ralith]

You can compromise on turing-completeness, too. Idris, for example, lets the programmer decide whether a given definition should be required to provably terminate or not.

[ufo]

The real way dependently typed languages dodge the undecidability problem is taht they "give up" on some valid programs. The output of the typechecker is either "proved the program is correct", "proved the program is incorrect" or "incondusive". If the result is "inconclusive" then it means that the programmer needs to manually provide a proof of correctness.

[mnarayan01]

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

Guessing you're plenty clever...just didn't think about it enough :)

Simply transform a program into one which halts on a type error rather than whatever else it might be doing. Done.

[samatman]

Consider the case of a simple type system, where any statement in the language is of either type "true" or type "false"....

[jessaustin]

This proof is missing a few steps, at least if it's meant to convince slow thinkers like myself. b^)