3 ms·

Regarding the Haskell code, what about infinite lists? 1. Why didn't QuickCheck test the infinite case? 2. How do we write tests that fail (instead of hang) i

Regarding the Haskell code, what about infinite lists? 1. Why didn't QuickCheck test the infinite case? 2. How do we write tests that fail (instead of hang) if an infinite list is mishandled? It seems like infinite lists act somewhat analogously to nulls: rndSelect cannot handle them, and that fact is not obvious in its type.

uryga 7y ago
> How do we write tests that fail (instead of hang) if an infinite list is mishandled? easy, just solve the halting problem!
- millstone 7y ago
  Deciding type-safety of code also requires solving the halting problem, but haskell still tries! I guess the question could be practical. Some functions are supposed to handle infinite lists: rfold, map, etc. How are these functions (or other, nontrivial ones) tested in practice, to ensure that they do not become accidentally strict?
  - uryga 7y ago
    > Deciding type-safety of code also requires solving the halting problem, but haskell still tries! does it? afaik typechecking is decidable for most type systems, and only becomes undecidable with something like dependent types (or c++ templates) but i could be wrong
  - uryga 7y ago
    just noticed i forgot to reply to the rest of your comment! i'm not sure how it's done in practice (except for "thinking about it really hard"). i came up with something though: `map` should be easy, because it's productive, i.e. it yields one result-element after processing every input element. so we could just test it by doing something like map f [1, 2, error "too strict!" and checking if it blows up when we force the first 2 elements – if it does, it must've processed the third element (error) as well, so it's too strict; if it didn't, it hasn't touched the last element, so it's as lazy as we wanted (only processes the stuff we asked for) and would work for infinite lists too (i think). we could also do something similar for `foldr`: foldr (:) [] [1, 2, error "too strict!"] which just reconstructs the original list. then we can apply the same reasoning as above.
almostdeadguy 7y ago
You can have types in haskell that represent finite length lists. Here's a blog post giving an overview of several methods of doing so (and several examples of libraries in the wild that provide this): https://blog.jle.im/entry/fixed-length-vector-types-in-haskell.html https://blog.jle.im/entry/fixed-length-vector-types-in-haske... There's a tradeoff here between generality and how important it is to encode all invariants about a piece of data. Many haskell list processing functions are expressed in terms of right folds, which makes infinite lists fairly unproblematic to work with so long as only part of the list is demanded in the end, however for some cases you may want the type system to ensure you can't receive an infinite list.
domlebo70 7y ago
Because you can't.
anaphor 7y ago
I believe the point of QuickCheck is actually to try and minimize the size of the test cases as much as possible by finding the minimal failing test case. So it explicitly tries to avoid testing larger and larger inputs or outputs, even if they could be potentially infinite. If you want the ability to encode bounds inside the type itself, then you'll need to look at various extensions like DataKinds, TypeFamilies, etc, or at a dependently typed language like Idris.
pyrale 7y ago
The promise of better type systems os that more of your code will be secured by types, not that everything will be covered. That is why there are still people working on newer type systems (e.g. dependent types, linear types, etc). For the specific example you give, you can either use liquid haskell, which is an annotation system bringing richer types to haskell, or use another lang that has dependent types off the shelf.

uryga 7y ago

> How do we write tests that fail (instead of hang) if an infinite list is mishandled? easy, just solve the halting problem!

millstone 7y ago
Deciding type-safety of code also requires solving the halting problem, but haskell still tries! I guess the question could be practical. Some functions are supposed to handle infinite lists: rfold, map, etc. How are these functions (or other, nontrivial ones) tested in practice, to ensure that they do not become accidentally strict?
- uryga 7y ago
  > Deciding type-safety of code also requires solving the halting problem, but haskell still tries! does it? afaik typechecking is decidable for most type systems, and only becomes undecidable with something like dependent types (or c++ templates) but i could be wrong
- uryga 7y ago
  just noticed i forgot to reply to the rest of your comment! i'm not sure how it's done in practice (except for "thinking about it really hard"). i came up with something though: `map` should be easy, because it's productive, i.e. it yields one result-element after processing every input element. so we could just test it by doing something like map f [1, 2, error "too strict!" and checking if it blows up when we force the first 2 elements – if it does, it must've processed the third element (error) as well, so it's too strict; if it didn't, it hasn't touched the last element, so it's as lazy as we wanted (only processes the stuff we asked for) and would work for infinite lists too (i think). we could also do something similar for `foldr`: foldr (:) [] [1, 2, error "too strict!"] which just reconstructs the original list. then we can apply the same reasoning as above.

almostdeadguy 7y ago

You can have types in haskell that represent finite length lists. Here's a blog post giving an overview of several methods of doing so (and several examples of libraries in the wild that provide this): https://blog.jle.im/entry/fixed-length-vector-types-in-haskell.html https://blog.jle.im/entry/fixed-length-vector-types-in-haske... There's a tradeoff here between generality and how important it is to encode all invariants about a piece of data. Many haskell list processing functions are expressed in terms of right folds, which makes infinite lists fairly unproblematic to work with so long as only part of the list is demanded in the end, however for some cases you may want the type system to ensure you can't receive an infinite list.

domlebo70 7y ago

Because you can't.

anaphor 7y ago

I believe the point of QuickCheck is actually to try and minimize the size of the test cases as much as possible by finding the minimal failing test case. So it explicitly tries to avoid testing larger and larger inputs or outputs, even if they could be potentially infinite. If you want the ability to encode bounds inside the type itself, then you'll need to look at various extensions like DataKinds, TypeFamilies, etc, or at a dependently typed language like Idris.

pyrale 7y ago

The promise of better type systems os that more of your code will be secured by types, not that everything will be covered. That is why there are still people working on newer type systems (e.g. dependent types, linear types, etc). For the specific example you give, you can either use liquid haskell, which is an annotation system bringing richer types to haskell, or use another lang that has dependent types off the shelf.