3 ms·
I would avoid using the terms "type" and "check" together for this, since "type checking" has a well established meaning (referred to as the "classical"/"logica
by chriswarbo 10y ago
I would avoid using the terms "type" and "check" together for this, since "type checking" has a well established meaning (referred to as the "classical"/"logical" approach in this README).
Random testing like this, as WaxProlix says, is reminiscent of QuickCheck; in that case you might replace "type" with "property", since the phrase "property checking" is associated with this approach.
Alternatively, stick with "type" (or maybe "contract"? These terms are all very overloaded!), but use "testing" instead of "checking".
Note that this approach is should be possible in Idris too, since we have equality types. For example, assuming we have some QuickCheck-style functions available, I could say:
someProp : Foo -> Bar -> Bool
someProp x y = whateverExpressionWeLike
somePropCheck : quickCheck someProp = True
somePropCheck = refl
This will only type-check (in the traditional sense) if `quickCheck someProp` evaluates to `True`; otherwise `somePropCheck` will be ill-typed. `someProp` and `somePropCheck` have no impact at runtime, since they're never called from anywhere (they could be encapsulated privately in a module too).
`quickCheck` can be a normal function; it's simple enough to generate "random" values in a pure way (e.g. Mersenne Twister with some arbitrary seed), although that would lose one of the features of property checking: each time it runs, we explore more of the possible inputs, and hence gain more confidence. Since runtime guarantees don't depend on the particular values generated by `quickCheck`, it's still "morally pure" even if implemented in an impure way; hence we could use a mechanism similar to "type providers" to impurely generate random values, and hence regain that feature.
- LightMachine 10y agoI agree with everything you said. On doing that in Idris (which is my dream language - the only reason I don't use it is its JS compiler is too slow), would it be possible to randomly generate elements of any data type, or would we have to write an `Arbitrary` instance for every type you want to test? I don't know/remember much about generics on Idris, would love to learn more. (Seriously, though, why is the JS compiler still so slow? Again - I'm willing to put substantial money into funding a better one...)
- chriswarbo 10y agoHmm, I imagine there's probably a generic way to do it; but I was imagining a straight port of the Haskell version. Note that it might be difficult to generate values of some heavily-constrained dependent type; you'd effectively be implementing a proof search!
- notjack 10y agoYou probably could, but part of the purpose of Idris is to statically prove things with dependent types rather than test them.
- chriswarbo 10y agoTesting and proving aren't mutually exclusive; there's also a more fine-grained distinction, between proving things (say, with pen and paper, or an SMT solver, or whatever) and proving things using the type system of the language they're implemented in. The nice thing about Idris is that it's specifically created with such "practical" issues in mind: it gives you powerful tools, but there's absolutely no obligation to use them. If you want to, you can avoid checking certain (or all) parts of a program. You need to define enough types to represent your computation/data, but not to prove its correctness; e.g. you can over-represent your domain using a bunch of sum types, stick infinite loops in the branches you know/think are unreachable, then turn off totality checking. If we compare this to, say, Coq or Agda, not only must you prove everything-you-write-in-those-languages, you must also prove everything-you-write in those languages! (i.e. everything you write must be proved, and only proofs written in Coq/Agda will be accepted). You can assert axioms, but not their computational/runtime meaning, which is problematic when using them as a programming language.