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).<p>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.<p>Alternatively, stick with "type" (or maybe "contract"? These terms are all very overloaded!), but use "testing" instead of "checking".<p>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:<p><pre><code> someProp : Foo -> Bar -> Bool
someProp x y = whateverExpressionWeLike
somePropCheck : quickCheck someProp = True
somePropCheck = refl
</code></pre>
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).<p>`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.