3 ms·

> I don't think dependent types are the future of development, but instead I'd bet on refined types > ... > lookup : (a : array) -> (n : int if 0 <= n < lengt

• tomp 8y ago
  Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math"). The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up. Dependent types: everything is proved, by hand, by the user, who has to build up the whole program from basic blocks. Usually the "foundation" is taken to be some kind of type theory, either Martin-Löf Type Theory or more recently Homotopy Type Theory, which has some complexities (e.g. multiple types of equality) and limitations (e.g. languages cannot be Turing complete) that I don't really understand. "Pi types" abound. I'm not sure how much of this description really is fundamental about Type Theory, and how much is just due to the specifics of the implementations I've seen (Coq, Agda, Idris). Refined types: start with a program and add some assertions about the values (and possibly functions, but this can then get more complicated) in the program. The idea is that many of these can ideally be proven by automated SMT solvers, which support some "theories" (e.g. natural numbers, real numbers, bitfields (i.e. machine integers and floating point numbers), algebraic datatypes) and can prove some statements in these theories. As you mentioned, "linear arithmetics", along with "real number algebra", are complete and decidable theories, so in theory you should be able to prove anything about them, but I'm guessing that in practice you'd still want some timeout parameter on your SMT solver (like in type systems, where there are exponential edge cases, that thankfully don't arise often in practice), but they aren't very useful, so hopefully you can prove more than that, using the heuristics embedded into SMT solvers (e.g. you should be able to prove many non-linear properties of two-dimensional loops by lifting integers into reals). If the solver is unable to solve something, the programmer can still add hints (but this quickly gets complicated). A concrete difference would be, in dependently-typed language, you define a list type as type List a n = | Nil : List 'a 0 | Const : a -> List a n -> List a (n + 1) in a language with refined types, you can add length afterwards: type List a = <... whatever ...> property length : List a -> Nat And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things. Not sure if this makes a lot of sense, I haven't looked into this in a while and am also not aware of the most recent research in these fields. Hopefully someone can explain better!
  • mietek 8y ago
    > Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really understand … One sentence summary that glosses over a lot of things: In a dependently typed language, types can contain programs, and we want typechecking to terminate. You may also want to read how the author of Idris explains partial and total functions: https://livebook.manning.com/#!/book/type-driven-development-with-idris/chapter-1/141 https://livebook.manning.com/#!/book/type-driven-development...
  • tom_mellior 8y ago
    OK, I think I see where you're coming from. I don't think the distinction you make is a useful one. > A concrete difference would be, in dependently-typed language, you define a list type as [...] Coq is a dependently typed language, and while it has a definition like this for some thing (called vector, maybe? I forget), the definition for lists in the standard library is not dependent, and length is a separate function. You can still write a function like Fixpoint lookup (xs: list a) (idx: {n: nat | n < length xs}): a := ... I don't know how much experience you have with dependently typed languages, but it looks like you might have misunderstood tutorials showing that one can define a dependent list type as saying that one must define lists dependently? > And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things. Treating it as uninterpreted is quite weak. It allows you to prove simple callers of the lookup function, but not the implementation. Also, you would not be able to prove something like this: if idx < length xs then lookup (Cons foo xs) (idx + 1) else ... This is admittedly a silly example, but it should be provable. But you can only do that if you can reason about the relationship between length and Cons. As for automating proofs, I very very much agree that we need a lot more automation. But if that means crippling our theories to an extend that they are no longer expressive enough to verify our software, not much is won.
    • tomp 8y ago
      Cool, very interesting. I need to look into Coq again! Maybe it's closer to what I want than I thought!