The future of Dependent Haskell

[atravers]

@tomjaguarpaw

It’s hard to summarize how I feel about generators, but maybe this does the job: “generators are often complicated enough to themselves need tests”.

Alternatively:

• a practical test should not require its own tests

because of the risk of infinite indeterminate regress:

• test1 needs test2 which needs test3 which needs test4 which needs …

which isn’t practical.

Similarly:

• a practical type system should not require its own type system

because there really is an infinite hierarchy of types!

Trying to solve the problems in one type system by introducing another type system makes as much sense as:

• trying to solve the problems in one test by introducing another test;

• trying to solve the problems in one testsuite by introducing another testsuite.

Adding more tests, testsuites, and type systems means more code, and more code means more bugs.