7 ms·

Dependent Haskell is not sound (type in type, i.e. a type level version of Russell's Paradox, and lack of totality checking). Its primary purpose is not theorem

Dependent Haskell is not sound (type in type, i.e. a type level version of Russell's Paradox, and lack of totality checking). Its primary purpose is not theorem proving per se, but rather unifying the explosion of GHC extensions that currently are weak approximations of a full dependently typed system. More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. Sure the article is a bit exuberant, but I think you're being a bit harsh here. Yes the field of formal verification, from my amateur practitioner's point of view, is a mishmash of techniques right now, with no single technique that has quite the right ergonomic vs power ratio that dominates over all others. But as far as I can tell there is in fact a significant amount research being done in dependent types. Many programming languages now have very limited dependent types. GADTs are one form that shows up in e.g. OCaml, Haskell, and Scala. Indeed Jane Street had a blog post about how GADTs were surprisingly useful for them (https://blog.janestreet.com/why-gadts-matter-for-performance/ https://blog.janestreet.com/why-gadts-matter-for-performance...). Ongoing research projects occur for languages such as Agda and Coq. Just like with formal specification systems like TLA+ and Alloy where you don't need to specify in exhaustive detail what you're after to see significant value, you don't have to prove comprehensive theorems to derive significant value from dependent types. An easy, lightweight win is to leave behind value specific tokens when performing some sort of runtime check rather than trying to prove the runtime check (e.g. keeping track that yes I ran the isPrime function on this number, rather than proving that a number is actually prime), which you can then use to subsume pre/postcondition contract systems, since you can attach markers of arbitrary checks being made that don't necessarily affect the value (e.g. keep track that I did check this user ID against a blacklist before trying to use it elsewhere). The main problem with dependent types as far as I can tell is that only very recently have we had languages that try to write actual programs with full-spectrum dependent types appear. Idris is really the only example I can think of. Languages like Agda are first and foremost provers. I suspect the vast majority of Agda programs are never run after they've typechecked. As a result we have little idea of what good practices with full-spectrum dependent types looks like. I have suspicions it looks fairly different from the hacks that current statically typed languages try to use to approximate it. For example I suspect some correct by construction approaches to ordinary statically typed FP languages quickly spiral into monstrosities with full-spectrum dependent types that can be nicely sidestepped again with evidence of runtime checks instead of full proofs. Even with Idris, we don't have people using these systems in anger. We don't know how much to expose of function implementations, how much a totality checker matters, how best to avoid proof infection (where because a low-level component demands a proper proof and that proof is used at runtime, you must deliver a valid proof and can't use some sort of TrustMe escape hatch of a null value that has any type). There are ideas. Idris 2 introduces a type system that distinguishes between proofs that are never used at runtime and runtime values, allowing users to safely use the TrustMe escape hatch if necessary. But there isn't a large community working with them while trying to ship business products. That for me is the greatest promise of dependent types in Haskell. Getting more real world experience of programmers using dependent types to uncover ergonomic holes. The Haskell community in the grand scheme of languages is small. It is nonetheless orders of magnitude larger than the full-spectrum dependently typed community and, if Dependent Haskell lands, represents perhaps the first time that a dependently typed language is used to directly write, rather than verify, production systems.

permeakra 7y ago
>More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing.
- pron 7y ago
  > They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing. That they can be used in a useful way doesn't mean you should have them. Other things (like contract systems) can do pretty much what dependent types do, but don't suffer from as many disadvantages. A tank could get your kids to school, but that doesn't mean it's a good idea to get a tank if what you need is to get your kids to school.
  - permeakra 7y ago
    >That they can be used in a useful way doesn't mean you should have them. It's a good enough reason to want them as an option. >Other things (like contract systems) can do pretty much what dependent types do If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic. Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism. As far as I can see, Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory). Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent.
    - pron 7y ago
      > It's a good enough reason to want them as an option. I'm not so sure. If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition? > If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic. There are many factors by which to judge the utility of specification and verification tools. There is no specific metric of "strength" that determines the value of a formalism. As Alonzo Church wrote in the paper in which he invented the lambda calculus, formal systems are not more or less true or more or less good; rather, they can be more or less convenient for different uses, and more or less aesthetically appealing to different people. In general, developers need a system that can be flexible. The difference in cost between verifying something with 99.9% confidence and with 100% confidence can be 10x. Sometimes you're willing to pay that 10x for a slight increase in confidence, and sometimes you're not. Often, the decision is different for different parts and different properties of a program, or for different properties of the same part of the program, or for the same property in different parts of the program. > Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism. You've studied all logics and all type systems and have concluded that all the type theories are always less awkward to all people than all "direct" program logics? Also, no logic is pretending to be or not to be a type theory. Type theories are not the canonical representation of logic. That's just not how formal systems work. > Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory). Hoare logic can be used for polymorphism, dynamic dispatch, higher-order subroutine, and anything else type theory can be used for. But I'm not claiming it's superior to type theory. Type theory is fine. > Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent. No, because the problem with dependent types is not the theory, which is, indeed, equivalent to whatever logic you choose and vice versa. The problem is that they force you to use deductive proofs for verification. Not only do you not want your specification method to force you to use a particular verification method, but rather you want flexibility because verification methods vary tremendously in cost, deductive proofs make for the worst default verification methods, as it's the most costly and least scalable (at least so far).

permeakra 7y ago

>More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing.

pron 7y ago
> They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing. That they can be used in a useful way doesn't mean you should have them. Other things (like contract systems) can do pretty much what dependent types do, but don't suffer from as many disadvantages. A tank could get your kids to school, but that doesn't mean it's a good idea to get a tank if what you need is to get your kids to school.
- permeakra 7y ago
  >That they can be used in a useful way doesn't mean you should have them. It's a good enough reason to want them as an option. >Other things (like contract systems) can do pretty much what dependent types do If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic. Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism. As far as I can see, Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory). Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent.
  - pron 7y ago
    > It's a good enough reason to want them as an option. I'm not so sure. If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition? > If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic. There are many factors by which to judge the utility of specification and verification tools. There is no specific metric of "strength" that determines the value of a formalism. As Alonzo Church wrote in the paper in which he invented the lambda calculus, formal systems are not more or less true or more or less good; rather, they can be more or less convenient for different uses, and more or less aesthetically appealing to different people. In general, developers need a system that can be flexible. The difference in cost between verifying something with 99.9% confidence and with 100% confidence can be 10x. Sometimes you're willing to pay that 10x for a slight increase in confidence, and sometimes you're not. Often, the decision is different for different parts and different properties of a program, or for different properties of the same part of the program, or for the same property in different parts of the program. > Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism. You've studied all logics and all type systems and have concluded that all the type theories are always less awkward to all people than all "direct" program logics? Also, no logic is pretending to be or not to be a type theory. Type theories are not the canonical representation of logic. That's just not how formal systems work. > Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory). Hoare logic can be used for polymorphism, dynamic dispatch, higher-order subroutine, and anything else type theory can be used for. But I'm not claiming it's superior to type theory. Type theory is fine. > Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent. No, because the problem with dependent types is not the theory, which is, indeed, equivalent to whatever logic you choose and vice versa. The problem is that they force you to use deductive proofs for verification. Not only do you not want your specification method to force you to use a particular verification method, but rather you want flexibility because verification methods vary tremendously in cost, deductive proofs make for the worst default verification methods, as it's the most costly and least scalable (at least so far).