  We present a new technique called type targeted testing, which translates
precise refinement types into comprehensive test-suites. The key insight behind
our approach is that through the lens of SMT solvers, refinement types can also
be viewed as a high-level, declarative, test generation technique, wherein
types are converted to SMT queries whose models can be decoded into concrete
program inputs. Our approach enables the systematic and exhaustive testing of
implementations from high-level declarative specifications, and furthermore,
provides a gradual path from testing to full verification. We have implemented
our approach as a Haskell testing tool called TARGET, and present an evaluation
that shows how TARGET can be used to test a wide variety of properties and how
it compares against state-of-the-art testing approaches.
