14 ms·

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code):

• nuncanada 13y ago
  Yes, Depently Typed languages can. They are full blown theorem provers...
  • JadeNB 13y ago
    Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems. (This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't need the full Gödelian power to observe that a priori theorems that must be verified at compile time can never account for data that are provided only after compilation.)
    • jarrett 13y ago
      > can never account for data that are provided only after compilation It seems to me they could. Suppose my program depends on external input D. That input could be a file it loads, keyboard input, network input, or anything else. Could I declare that I expect D to have properties P? And then, could the language force me to implement a code path for cases where D does not satisfy P? An example of such a code path would be to print an error message and then terminate the program.
      • JadeNB 13y ago
        Yes, this is a good point. I hope that what I meant was reasonably clear, but a more precise would have been something like "cannot prove certain assertions about data that are provided only after compilation".
    • sold 13y ago
      When I write a program, I don't want it to be just correct (true); I want it to be _provably_ correct; I want to be able to be convinced that it is correct, at least in principle, given enough time and whole specification of the system. Programs which are correct, but not provably so, should not pass code review and might as well be lumped together with those which are wrong. It doesn't matter if you are using a full-blown theorem prover or thinking about the code in your head; Gödel's theorems are not really relevant to programming, even when the code uses deep mathematics. I'm not sure I agree with "theorems that must be verified at compile time can never account for data that are provided only after compilation". At compile time, you prove the assertion "for every x, the program outputs correct answer for x". Now, you don't know that the user will enter say x=5 at runtime, but since you proved a theorem about _every_ x, this includes x=5. You cannot predict the future (the path that will be taken by the program), but once you prepare for all possible futures, you're safe.
      • platz 13y ago
        The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties.
• tel 13y ago
  Your idea about `maybe (int (>= 0, <= 10))` is exactly correct, but there's an important point to emphasize around it: In a DT language when you express such a type the compiler will demand that you write a type like maybe which can fail at runtime and demand that you handle that failure. To the compiler, `int` and `int (>= 0, <256)` are different types which require an explicit conversion (though the particular choice of conversion may be implicitly defined, viz. Idris' Coerce typeclass). In order to do multiplication like you suggested you would have to provide enough information to the compiler (either at compile time via constants or via a possibly failing mechanism which generates proof requirements at runtime) that your multiplication will not violate the constraints of the type. To you final point about tracking constraints, even those defined implicitly, I think the answer is no-ish. Most frequently, DT languages have such a richness of types that there's no way to infer them—you're forced to write out all of the top-level types. But the idea of passing around constraints like you're suggesting here is not impossible. You might imagine a pair type like (in no particular notation) (x, x => [Constraint]) where the first is a number and the second indicates a type-level function taking that particular number to a set of proofs that certain constraints are satisfied. We could indicate all of this at the type level and demand the compiler ensure that constraints are not violated (i.e. we end up coercing between constrained types like this and some coercions, those that coerce to supersets of the current constraints, are valid only) and we could also define a loose kind of (+), (*), (-) etc on this pair type such that the result passes along the proper constraints.
  • vilhelm_s 13y ago
    Agreed in general, but it is possible to enable this style of constraint propagation by being restrictive about what kind of contraints you can write. In particular, the "LIQUID" family of languanges that have been developed at UCSD allows properties which are conjunctions of LInear IneQUlites, and can infer them automatically. The programmer would annotate one declaration of a variable with a constraint like (0 <= x < 10), and the system tries to infer suitable constraints for all other variables (calling out to an SMT solver, and using invariant inference techniques from the program analysis community). Their latest research language is "Liquid Haskell", I think it could deal with jarrett's example out of the box (with the caveat that yes, you still need to write the test explicitly). They used to have an online demo where you could just type programs into a web form, but that doesn't seem to work right now...
• deleted 13y ago
  [deleted]
• JoshTriplett 13y ago
  The compiler doesn't necessarily have to have that level of inference; it can simply require the code to prove the constraints. For instance, parseInt will return an unconstrained int, so you'll get a type error trying to assign that to a range-constrained int. For your first and last examples, the multiplication operator on range-constrained ints can easily propagate the range constraints. In your last example, `z = w * x` would work, but assigning through the unconstrained int y may simply cause the last assignment z=y to produce a type error, forcing the code to re-establish the constraint explicitly.
• dllthomas 13y ago
  "Can a dependent type system catch all type errors at compile time?" Provably not, if you want a type checker guaranteed to finish.
  • jarrett 13y ago
    Could you give a brief overview of why? Does this come down to the halting problem?
    • arjunnarayan 13y ago
      Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.
      • Kutta 13y ago
        Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.
        • dllthomas 13y ago
          "You can always just refuse to run any function compile time that has not yet passed termination check." I don't understand this sentence.
          • Kutta 13y ago
            Both Idris and Agda check whether functions provably terminate. Halting problem notwithstanding it is possible to have conservative checks that never return false positives, so that an OK from the checker implies termination, but a FAIL doesn't imply non-termination. Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to occasionally run Idris functions (that's what makes it dependent). This is in fact the only source of potential non-termination in the checker. So, whenever Idris needs to run a function compile time, and it cannot prove termination via the checker, it just throws an error. (Side note: it is never required to run a function in order to the typecheck the very same function. All major dependent type checkers has the property that they never have to run a function that is not already checked).
• ardz 13y ago
  In DT languages you can even do something like: x of type: > 0, skyIsBlueNow().
• JadeNB 13y ago
  Without really addressing your question, notice that the power of dependently typed languages is not in the intelligence of the compiler, but in the expressivity of the type system. That is, the question becomes not "can the compiler catch this error on its own?", but rather "can the compiler verify my proof that I have not made this error?" A language with a very powerful type system can still have a very dumb compiler (although it will generate extremely slow code). EDIT: It occurs to me that this is well summarised by the apparently facetious remark "Ask not what your compiler can do for you; ask what you can do for your compiler."
• quandrum 13y ago
  Yes int x (>= 0, <=10) x = parseInt(getKeyboardInput) Dependent Type systems don't have to know what is possible keyboard input. They have to know what type the getKeyboardType function returns (and the parseInt), and if it's possible for that type to be out of the range of your constraint. If that's so, it throws an error. At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.
  • jarrett 13y ago
    > if it's possible for that type to be out of the range of your constraint....If that's so, it throws an error. If I'm understanding you correctly, that would seem to take a lot of the power out of dependent type systems. Almost all values will eventually depend on input from the outside world, so it seems you'd rarely have a chance to use your dependent type system. Haskell (which doesn't have dependent types baked in) has a good approach to possibly-invalid data via the Maybe type. E.g. Maybe Int means "either an integer, or nothing." So it forces you to explicitly handle the possible error cases.[1] To spell it out in Haskell terms: In the example of getting an integer from the keyboard, x is a Maybe Int. If the input is invalid, the value is set to Nothing, which is a unique constant. If it's valid, the value is of type Just Int. > At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe. But how do you get from untrusted, potentially invalid data into the world of trusted, guaranteed-valid data? How do you bridge the gap? I was suggesting some combination of an applyConstraint function and a Maybe type to achieve that. Are there other ways? [1] Actually, it will let you bypass the usual compile-time protections with the fromJust function. But if you want compile-time safety, either refrain from using fromJust, or use it only where you're absolutely sure the value won't be Nothing.
    • Dewie 13y ago
      I think a better example is the partial functions in Haskell like head or tail. They throw an exception on empty lists. You could make it return maybe [a] or a default value, but a common usage of head might be where you know yourself that the list is non-empty. Like: head . sort . f where f is a function that you know returns a non-empty list, perhaps because that's just the way it operates or because you checked it further up. You know that head won't crash since any reasonable implementation of sort returns a list which is just as long as the one that was given to it. Similarly: tail . sort . f won't crash. Moreover, the list will still be sorted, since you just removed the head of the list. This is all known to you, but you can't necessarily easily show it to the compiler. I don't know the motivation for wanting to know the input before it is given. Putting it in a Maybe is the only sensible option. Some things are just not known/unknowable before running a program. You wouldn't even need to run the program if you could prove absolutely anything about the properties of a program. Will the user input bleed through to all corners of the program? Well, why would it? You could have a sanitizing loop that refuses to pass "wrong" data to the pure (and dependently typed!) parts of the program, just looping over and over until the correct input is given.
• randyrand 13y ago
  | int x (>= 0, <=10) | x = parseInt(getKeyboardInput) Will be a compile time error because getKeyBoard input returns integers that are between 0-256(?) not 0-10 like 'x' wants.
  • jarrett 13y ago
    Exactly. That's why I proposed a Haskell-ish Maybe construct to represent the uncertainty of the input's validity. The code snippet: int x (>= 0, <=10) | x = parseInt(getKeyboardInput) ...was meant as an example of what won't work.
• arh68 13y ago
  > 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.
  • mnarayan01 13y ago
    > 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 13y ago
      Consider the case of a simple type system, where any statement in the language is of either type "true" or type "false"....
    • jessaustin 13y ago
      This proof is missing a few steps, at least if it's meant to convince slow thinkers like myself. b^)
  • leoc 13y ago
    > 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).
• rybosome 13y ago
  As others have noted, it's less about the compiler running code and making determinations as it is using extremely robust, information-rich types. For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector. Operations that increase the size of the vector are guaranteed to return a non-empty vector. They might look something like this: (::) : a -> Vector a n -> Vector a (S n) This says that an element cons a vector of any size results in a vector that is guaranteed to be non-empty. This means that you could safely write a function to retrieve the head of a list by restricting the type to lists that are guaranteed to be non-empty. head : Vector a (S n) -> a Something like the following pseudo-code in a REPL(I don't actually know a thing about Idris): let nums : Vector Int n = [] head nums ...would fail to compile, since the second type param to nums is simply `n` rather than `(S n)`, as required by our `head` function. All of the things you would expect from Haskell like the power of ADTs and pattern-matching apply here, so you get even more compile time type-soundness.
  • chriswarbo 13y ago
    > For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector. In case anyone's wondering, only the first of these (the element type) is a type parameter, since it has a constant value in all sub-expressions (ie. the cons cells all contain elements of the same type). The second is a 'type index', which is a more general term (type parameters are a special case of type indices), since its value changes in the sub-expressions (the cons cells have different lengths). The difference is that we don't need to pattern-match parameters on every recursive call, since they're guaranteed to be constant (although we can if we like). I didn't know this until I asked http://cs.stackexchange.com/questions/20100/what-are-the-difference-between-and-consequences-of-using-type-parameters-and-ty http://cs.stackexchange.com/questions/20100/what-are-the-dif...
    • rybosome 13y ago
      Makes sense; thanks for the clarification!
• RogerL 13y ago
  In Ada you have subtype, so you would write subtype my_type is Integer range 0..10; my_type x = 9; my_type y = 10; my_type a = x + y; So, obviously there is enough information to deduce at compile time that the sum operation yields an incorrect value. In practice, as many of the replies point out, you can determine no such thing (my_type x = user_input()). In that case Ada will throw a runtime exception. All this checking is expensive, so it ends up being much like C/C++, where you have debug and release builds, where the release builds do not do the checking.
• deleted 13y ago
  [deleted]