search

kowainik / stan

🕵️ Haskell STatic ANalyser
https://kowainik.github.io/projects/stan
Mozilla Public License 2.0
565 stars 48 forks source link

Mention inductive naturals for STAN-0104 #342

Closed josephcsible closed 4 years ago

josephcsible commented 4 years ago

STAN-0104 should mention that genericLength is safe to use even on infinite lists as long as it's used at a type like data Nat = Zero | Succ Nat. (This doesn't apply to 0105 or 0106, since sum (repeat Zero) and product (repeat (Succ Zero)) would still both be bottom.

chshersh commented 4 years ago

I think people who use inductive naturals know what they are doing. So they can safely ignore this particular inspection if they find it unhelpful. We could patch the existing pattern for STAN-0104 to not warn on this inspection if it's used with the inductive nats type, but there's no data Nat = Z | S Nat type in base or any of the boot libraries, so such pattern won't be helpful. Also, partially because of that, we can't really suggest using this data type as a possible solution: not clear what is the default library choice for such type, we can't write a pattern to not warn on this inspection when this solution is applied, and the code can become less performant due to usage of inductive naturals.