4 ms·

Dependent types are a false idol. It’s better to express propositions just as propositions, like in Isabelle/HOL.

AnthonBerg 5y ago
Tell me more! (As I see it – at least these days – dependent types just are. It’s very, very nice to just have higher-order unification and the things that sort of fall naturally out of having it.)
- amw-zero 5y ago
  They are a false idol in that, when people learn about them they seem like they’re the answer to all problems, and they’re not. The fact that types are equivalent to propositions doesn’t mean that making all of the propositions about your code at the type level is a good idea. For me, it’s completely unnatural, clunky, and more verbose than just writing propositions as logical statements. I found this talk from Xavier Leroy a while back too: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf. He is the main person behind CompCert, the formally verified C compiler. They do that verification in Coq, so I was expecting him to be a believer of dependent types. But he had this to say: “ Dependent types work great to automatically propagate invariants - Attached to data structures (standard); - In conjunction with monads (new!). In most other cases, plain functions + separate theorems about them are generally more convenient.” For that reason I prefer Isabelle/HOL as a theorem prover. The core logic is simpler, but you can express whatever you want as a theorem, without worrying about phrasing it within the type system. It feels a lot more natural. That’s not without downside either of course. Proofs in Isabelle notoriously must match the structure of the code being verified, so changes to the code require proof changes. Liam O’Connor wrote an example of where they he feels dependent types are better here: http://liamoc.net/posts/2015-08-23-verified-compiler/index.html http://liamoc.net/posts/2015-08-23-verified-compiler/index.h.... Even with that, I’d rather have simple code plus simple propositions with complexity at the proof level. This will likely be another eternal holy war though.
  - AnthonBerg 5y ago
    Thank you so much for taling the time to write this thoughtful and valuable reply! It helps me see what I think I’m seeing, or rather to define it. It also has helped me to perspectives I hadn’t seen. I’m coming to dependent types from here: “simple, clear code good yes program program argh I can’t express a very distinct thought without escaping to another language layer or generating code using string concatenation”, and from here: “my data structure is simple and clear but argh it needs a handwritten parser and serializer and it needs to be maintained and argh why am I writing a parser AND a serializer it should be just one bidirectional definition? and argh why do I need to write it for each output/input format?”, and from here: “my code is simple and clean and my variables are well named and my tests are well defined and my documentation is well written but argh why can’t I just fold the mechanics that the tests define into the code? as proofs? (and… argh? why can’t my variables and documentation and method names be checked against the code?)”. It’s metaprogramming that I’m thinking about. And most programming ought to be programming. But we definitely need metaprogramming, and it needs to be understandable and composable and simple and clear. And I don’t know if dependent types are a complete solution to that, but I do think that they are necessary for it. That-which-is dependent types, which by definition is a computation of what it is and is a proof of what it is. Those philosophical terms finally become practically grounded and practical help in a lot of the work I find myself doing. I’ll certainly look for the false idol too! My sincere thanks.

Tell me more! (As I see it – at least these days – dependent types just are. It’s very, very nice to just have higher-order unification and the things that sort of fall naturally out of having it.)

amw-zero 5y ago
They are a false idol in that, when people learn about them they seem like they’re the answer to all problems, and they’re not. The fact that types are equivalent to propositions doesn’t mean that making all of the propositions about your code at the type level is a good idea. For me, it’s completely unnatural, clunky, and more verbose than just writing propositions as logical statements. I found this talk from Xavier Leroy a while back too: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf. He is the main person behind CompCert, the formally verified C compiler. They do that verification in Coq, so I was expecting him to be a believer of dependent types. But he had this to say: “ Dependent types work great to automatically propagate invariants - Attached to data structures (standard); - In conjunction with monads (new!). In most other cases, plain functions + separate theorems about them are generally more convenient.” For that reason I prefer Isabelle/HOL as a theorem prover. The core logic is simpler, but you can express whatever you want as a theorem, without worrying about phrasing it within the type system. It feels a lot more natural. That’s not without downside either of course. Proofs in Isabelle notoriously must match the structure of the code being verified, so changes to the code require proof changes. Liam O’Connor wrote an example of where they he feels dependent types are better here: http://liamoc.net/posts/2015-08-23-verified-compiler/index.html http://liamoc.net/posts/2015-08-23-verified-compiler/index.h.... Even with that, I’d rather have simple code plus simple propositions with complexity at the proof level. This will likely be another eternal holy war though.
- AnthonBerg 5y ago
  Thank you so much for taling the time to write this thoughtful and valuable reply! It helps me see what I think I’m seeing, or rather to define it. It also has helped me to perspectives I hadn’t seen. I’m coming to dependent types from here: “simple, clear code good yes program program argh I can’t express a very distinct thought without escaping to another language layer or generating code using string concatenation”, and from here: “my data structure is simple and clear but argh it needs a handwritten parser and serializer and it needs to be maintained and argh why am I writing a parser AND a serializer it should be just one bidirectional definition? and argh why do I need to write it for each output/input format?”, and from here: “my code is simple and clean and my variables are well named and my tests are well defined and my documentation is well written but argh why can’t I just fold the mechanics that the tests define into the code? as proofs? (and… argh? why can’t my variables and documentation and method names be checked against the code?)”. It’s metaprogramming that I’m thinking about. And most programming ought to be programming. But we definitely need metaprogramming, and it needs to be understandable and composable and simple and clear. And I don’t know if dependent types are a complete solution to that, but I do think that they are necessary for it. That-which-is dependent types, which by definition is a computation of what it is and is a proof of what it is. Those philosophical terms finally become practically grounded and practical help in a lot of the work I find myself doing. I’ll certainly look for the false idol too! My sincere thanks.