4 ms·

I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contrac

by tomp 8y ago

I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover. lookup : (a : array) -> (n : int if 0 <= n < length(a)) -> whatever [0] https://github.com/tomprimozic/type-systems/tree/master/refined_types https://github.com/tomprimozic/type-systems/tree/master/refi... [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [2] https://rise4fun.com/Dafny/tutorial/guide https://rise4fun.com/Dafny/tutorial/guide [3] https://fstar-lang.org/tutorial https://fstar-lang.org/tutorial - see e.g. section 3 "First proofs about functions on integers" [4] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3

lmm 8y ago
The problem I have is that it's not so obvious to the human reader which things are automatically provable. Constraint solvers are often surprisingly good, and occasionally surprisingly bad, so I'm constantly scared of getting into a "it's working, don't touch it" situation where seemingly simple changes make code stop working. We're constantly told that traditional typechecking is very limited compared to other forms of formal analysis. But I've always found dependent type systems are enough to express the relevant business constraints, and making the actual typechecking stage trivial seems very worthwhile.
- tomp 8y ago
  Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...
  - lmm 8y ago
    > the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies. > Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems. > So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more... Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
    - tomp 8y ago
      > Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked. That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
      - lmm 8y ago
        > All practical languages (even Rust and Haskell) fail for "division by zero" Well, they don't have dependent types. In something like Idris you can do safe natural division. > most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).
chrisdone 8y ago
Adding examples, with dependent types we can write the type-safe printf in Idris: https://github.com/chrisdone/sandbox/blob/master/dependently-typed-printf.idr https://github.com/chrisdone/sandbox/blob/master/dependently... Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations: https://github.com/chrisdone/sandbox/blob/master/liquid-haskell-dates.hs https://github.com/chrisdone/sandbox/blob/master/liquid-hask... The `if ..` tests are all required, otherwise Liquid Haskell rejects the program. So I see value in both directions, if you extrapolate from these examples to harder problems.
tom_mellior 8y ago
> 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 < length(a)) -> whatever https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type: "In computer science and logic, a dependent type is a type whose definition depends on a value." In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependent types, but possibly restricted in some way. Can you explain the restrictions you have in mind to clarify (and motivate) the relationship between full dependent types and your refined ones? Is it something purely syntactic like "linear arithmetic only" (as I believe was the case for Liquid Types, at least originally) to ensure decidability? Edit: Even the very first sentence of the very first paper about Liquid Types (the base of Liquid Haskell) talks about dependent types: "We present Logically Qualified Data Types, abbreviated to Liquid Types, a system [...] to automatically infer dependent types precise enough to prove a variety of safety properties." (emphasis mine)
- 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!

by tomp 8y ago

lmm 8y ago

The problem I have is that it's not so obvious to the human reader which things are automatically provable. Constraint solvers are often surprisingly good, and occasionally surprisingly bad, so I'm constantly scared of getting into a "it's working, don't touch it" situation where seemingly simple changes make code stop working. We're constantly told that traditional typechecking is very limited compared to other forms of formal analysis. But I've always found dependent type systems are enough to express the relevant business constraints, and making the actual typechecking stage trivial seems very worthwhile.

tomp 8y ago
Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...
- lmm 8y ago
  > the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies. > Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems. > So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more... Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
  - tomp 8y ago
    > Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked. That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
    - lmm 8y ago
      > All practical languages (even Rust and Haskell) fail for "division by zero" Well, they don't have dependent types. In something like Idris you can do safe natural division. > most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).

chrisdone 8y ago

Adding examples, with dependent types we can write the type-safe printf in Idris: https://github.com/chrisdone/sandbox/blob/master/dependently-typed-printf.idr https://github.com/chrisdone/sandbox/blob/master/dependently... Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations: https://github.com/chrisdone/sandbox/blob/master/liquid-haskell-dates.hs https://github.com/chrisdone/sandbox/blob/master/liquid-hask... The `if ..` tests are all required, otherwise Liquid Haskell rejects the program. So I see value in both directions, if you extrapolate from these examples to harder problems.

tom_mellior 8y ago

> 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 < length(a)) -> whatever https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type: "In computer science and logic, a dependent type is a type whose definition depends on a value." In your example, you are using a dependent type: The type of n depends on the value a. So your refined types are dependent types, but possibly restricted in some way. Can you explain the restrictions you have in mind to clarify (and motivate) the relationship between full dependent types and your refined ones? Is it something purely syntactic like "linear arithmetic only" (as I believe was the case for Liquid Types, at least originally) to ensure decidability? Edit: Even the very first sentence of the very first paper about Liquid Types (the base of Liquid Haskell) talks about dependent types: "We present Logically Qualified Data Types, abbreviated to Liquid Types, a system [...] to automatically infer dependent types precise enough to prove a variety of safety properties." (emphasis mine)

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!