3 ms·

Yes, that sounds pretty impossible. Is there an example of this?

by sillysaurus3 12y ago

wolfgke 12y ago
Google "haskell quickcheck".
- charlieflowers 12y ago
  Does quickcheck run at compile time for Haskell? (I've dabbled with Haskell, and I've read about Quickcheck in other languages besides Haskell. In those other languages, Quickcheck definitely does not "happen" at compile time ... does it for Haskell?)
  - codygman 12y ago
    I'm pretty sure quickcheck is run when you do "cabal test", though you could make a compiler wrapping script that fails if your quickcheck tests fail.
Verdex 12y ago
I've seen this attitude a couple of times before and I think it's a perfectly valid reaction to have towards these statements because you're correct. It is impossible. However, type systems heavily steeped in type theory get around it being impossible by cheating. For example ... Consider the halting problem. It's pretty common knowledge that given a program and some input there's no general algorithm that tells you if that program halts when the programming language is turing complete. However, we know that every simply typed lambda calculus program halts if it passes the type checker, so did we defeat the halting problem? No we cheated because simply typed lambda calculus isn't turing complete. The problem with type theory is that sometimes it excludes good programs that we want to run just because we don't know how to prove that the program is good (or maybe it's even unprovable). So we try to develop new type theories that will allow us to prove more and more good programs are in fact good.
tel 12y ago
It's absolutely possible for certain values of "power of your type system", "power of your program's types", and "extensiveness of your unit testing system". A few points to elaborate this. 1. Types absolutely can capture (trivially often) invariants which can never be satisfactorily covered by unit tests. This is the difference between proof and evidence. 2. Unit tests are far easier to write for many kinds of program behavior. Even though you can encode essentially anything you want into sufficiently powerful type systems, their proofs can be too challenging to practically build. 3. Type checking works very differently from testing. It's not red-green-refactor. It's more like "describe your problem in types and then slowly discover the only possible program which is correct". The feedback cycle here is very fast, but sometimes more inhospitable. Major research focus is on making this better, though. I'd say some of the most advanced HCI work is being done in dependently typed proof systems... but it's targeted only at people who understand and use dependently typed proof systems to begin with. 4. Unit tests often duplicate functionality which is trivially and automatically inferred by a type system. This is why, for certain invariants, types are "free" and unit tests are both incomplete and a big violation of DRY. So, essentially, the unit tests which get written for you automatically are the trivial ones which are inferable properties. A dynlang usually does not have sufficient structure to enable this inference so you have to cover it with unit tests or contracts. More advanced, un-inferable properties can be handled and checked on compilation as well, but typically it takes some effort to build this stuff. Interestingly, though, you usually do it with heavy automation driven by the (partial) inference that the compiler provides—it becomes a conversation between you and the compiler as you develop the program which satisfies the type specification you gave.

Yes, that sounds pretty impossible. Is there an example of this?

wolfgke 12y ago

Google "haskell quickcheck".

charlieflowers 12y ago
Does quickcheck run at compile time for Haskell? (I've dabbled with Haskell, and I've read about Quickcheck in other languages besides Haskell. In those other languages, Quickcheck definitely does not "happen" at compile time ... does it for Haskell?)
- codygman 12y ago
  I'm pretty sure quickcheck is run when you do "cabal test", though you could make a compiler wrapping script that fails if your quickcheck tests fail.

Verdex 12y ago

I've seen this attitude a couple of times before and I think it's a perfectly valid reaction to have towards these statements because you're correct. It is impossible. However, type systems heavily steeped in type theory get around it being impossible by cheating. For example ... Consider the halting problem. It's pretty common knowledge that given a program and some input there's no general algorithm that tells you if that program halts when the programming language is turing complete. However, we know that every simply typed lambda calculus program halts if it passes the type checker, so did we defeat the halting problem? No we cheated because simply typed lambda calculus isn't turing complete. The problem with type theory is that sometimes it excludes good programs that we want to run just because we don't know how to prove that the program is good (or maybe it's even unprovable). So we try to develop new type theories that will allow us to prove more and more good programs are in fact good.

tel 12y ago

It's absolutely possible for certain values of "power of your type system", "power of your program's types", and "extensiveness of your unit testing system". A few points to elaborate this. 1. Types absolutely can capture (trivially often) invariants which can never be satisfactorily covered by unit tests. This is the difference between proof and evidence. 2. Unit tests are far easier to write for many kinds of program behavior. Even though you can encode essentially anything you want into sufficiently powerful type systems, their proofs can be too challenging to practically build. 3. Type checking works very differently from testing. It's not red-green-refactor. It's more like "describe your problem in types and then slowly discover the only possible program which is correct". The feedback cycle here is very fast, but sometimes more inhospitable. Major research focus is on making this better, though. I'd say some of the most advanced HCI work is being done in dependently typed proof systems... but it's targeted only at people who understand and use dependently typed proof systems to begin with. 4. Unit tests often duplicate functionality which is trivially and automatically inferred by a type system. This is why, for certain invariants, types are "free" and unit tests are both incomplete and a big violation of DRY. So, essentially, the unit tests which get written for you automatically are the trivial ones which are inferable properties. A dynlang usually does not have sufficient structure to enable this inference so you have to cover it with unit tests or contracts. More advanced, un-inferable properties can be handled and checked on compilation as well, but typically it takes some effort to build this stuff. Interestingly, though, you usually do it with heavy automation driven by the (partial) inference that the compiler provides—it becomes a conversation between you and the compiler as you develop the program which satisfies the type specification you gave.