5 ms·

Which programming language are you using? It looks to me like you need exhaustiveness checking for pattern matching. Languages like Scala, OCaml, Purescript or

by manx 5y ago

Which programming language are you using? It looks to me like you need exhaustiveness checking for pattern matching. Languages like Scala, OCaml, Purescript or Haskell support this out of the box. Am I overlooking something?

labawi 5y ago
I think OP wants transitive exhaustiveness checks while supporting partial base functions. My suggestion: Must you have partial functions? Maybe you can model your data more tightly? If your conditions are too complex, maybe you could decompose them? A big reason I like ADTs with concise syntax is to model data with nearly¹ no room for invalid or useless data. Then all¹ functions are total and matches are checked for exhaustiveness. A nice matching syntax on top makes mistakes easy to spot. Not sure how to help with formal verification or exhaustiveness on partial functions. ¹ I don't model everything absolutely precisely, but deviations are more of an exception rather than the rule. Then they can be made apparent and reasoned about.
tomas789 5y ago
I have a list of entities. The entities are partitioned by different properties (like color, speed and so on, partitions usualy cover the whole list but not always). Compilers like Haskell and Fsharp can catch exhaustiveness over individual entities or each property individually. Problems arise when they are combined. For example first case covers red and blue entities, second case covers fast entities, thirs case explicitly covers entity 1 and 2. Now the question is whether this is exhaustive. Compiler of Fsharp just tells me it is not and one has to provide the otherwise case and do something there (raise exception, return none or something). But in this case the correctness is proven only during the execution. From the outside persons point of view this is the same behavior. The program has crashed. I as a developer can go through the cases and reason that those cases are actually exhaustive and move on. Problem is that this is time consuming and one would need to check everything every time the partitionings change (which happens).
- sn9 5y ago
  Are you using property-based testing tools like Quickcheck? Some Youtube videos: https://www.youtube.com/results?search_query=property+based+testing+quickcheck+John+Hughes https://www.youtube.com/results?search_query=property+based+... Article by author of Hypothesis, the property-based testing framework for Python: https://increment.com/testing/in-praise-of-property-based-testing/ https://increment.com/testing/in-praise-of-property-based-te... Pycon talk on how Contracts + PET gets you integration tests: https://www.hillelwayne.com/talks/beyond-unit-tests/ https://www.hillelwayne.com/talks/beyond-unit-tests/ An article from the property-based testing series on the blog F# for Fun and Profit: https://fsharpforfunandprofit.com/posts/property-based-testing-2/ https://fsharpforfunandprofit.com/posts/property-based-testi...

by manx 5y ago

labawi 5y ago

I think OP wants transitive exhaustiveness checks while supporting partial base functions. My suggestion: Must you have partial functions? Maybe you can model your data more tightly? If your conditions are too complex, maybe you could decompose them? A big reason I like ADTs with concise syntax is to model data with nearly¹ no room for invalid or useless data. Then all¹ functions are total and matches are checked for exhaustiveness. A nice matching syntax on top makes mistakes easy to spot. Not sure how to help with formal verification or exhaustiveness on partial functions. ¹ I don't model everything absolutely precisely, but deviations are more of an exception rather than the rule. Then they can be made apparent and reasoned about.

tomas789 5y ago

I have a list of entities. The entities are partitioned by different properties (like color, speed and so on, partitions usualy cover the whole list but not always). Compilers like Haskell and Fsharp can catch exhaustiveness over individual entities or each property individually. Problems arise when they are combined. For example first case covers red and blue entities, second case covers fast entities, thirs case explicitly covers entity 1 and 2. Now the question is whether this is exhaustive. Compiler of Fsharp just tells me it is not and one has to provide the otherwise case and do something there (raise exception, return none or something). But in this case the correctness is proven only during the execution. From the outside persons point of view this is the same behavior. The program has crashed. I as a developer can go through the cases and reason that those cases are actually exhaustive and move on. Problem is that this is time consuming and one would need to check everything every time the partitionings change (which happens).

sn9 5y ago
Are you using property-based testing tools like Quickcheck? Some Youtube videos: https://www.youtube.com/results?search_query=property+based+testing+quickcheck+John+Hughes https://www.youtube.com/results?search_query=property+based+... Article by author of Hypothesis, the property-based testing framework for Python: https://increment.com/testing/in-praise-of-property-based-testing/ https://increment.com/testing/in-praise-of-property-based-te... Pycon talk on how Contracts + PET gets you integration tests: https://www.hillelwayne.com/talks/beyond-unit-tests/ https://www.hillelwayne.com/talks/beyond-unit-tests/ An article from the property-based testing series on the blog F# for Fun and Profit: https://fsharpforfunandprofit.com/posts/property-based-testing-2/ https://fsharpforfunandprofit.com/posts/property-based-testi...