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.
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:
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.