3 ms·

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 su

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