There's a broader class of problems where achieving totality by restricting the type is possible, but the cost-benefit trade-off of forcing everything into the type level comes out in the wrong direction. I ran into an example in https://medium.com/@cdsmithus/pair-programming-with-chatgpt-haskell-1c4490b71da6 (scroll to the end and see final code for Part IV, and the toMatrixVectorForm function), where in the general case I needed polynomial arithmetic, but in certain specific cases (where either one of the two players of the game adopts a pure strategy), I knew that the result would always be a linear expression. It would definitely be possible to annotate the polynomial type with a maximum degree, define higher-kinded arithmetic operations that would correctly propagate that across addition and multiplication, and use a bounded-length list type for variables in a term, all to avoid that one error case in pattern matching. However, it would have been a significant distraction from the problem being solved.

On Thu, Jan 26, 2023 at 10:46 AM David Feuer <david.feuer@gmail.com> wrote:

There are occasional situations where the data structure is right but the limitations of Haskell's type system prevent us from proving totality. I've only ever written a couple I'm proud of:

1. Data.Biapplicative.traverseBiaWith
2. Data.Sequence.zipWith and Data.Sequence.chunksOf

traverseBiaWith seems to need an "impossible" case to achieve the right semantics for lazy biapplicatives and infinite structures. Code shared by zipWith and chunksOf uses one (relying on the tree annotation invariant) to compute the result incrementally and (therefore) more efficiently.

On Thu, Jan 26, 2023, 8:34 AM Dan Dart <haskellcafe@dandart.co.uk> wrote:
> {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

I feel like that's just avoiding facing the problem. It makes sense
though, if you know 100% that there really, really is no other case.
But as previous repliers have said, that's probably not a case for
partials. If it's both known and partial, you're probably using the
wrong datastructure for it. There's a reason many Prelude replacements
don't include partial functions, and there's generally a better
solution for it in them. And even if you're using base Prelude (which
I am 99% of the time), things are only Maybe if they come from
somewhere where they possibly could be.

So, taking (!?) as an example, if you've statically set a list to
contain a value and want it out, and want to avoid using partial
functions like (!!) then perhaps static lists were not a good use case
for you, is what I think people are getting at.

> what if args is wrong?

Another solution I use a lot is to match on lists, e.g.:

doSomethingWithListOfParameters :: [Text] -> IO ()
doSomethingWithListOfParameters xs = \case
[] -> someActionUsingNoParameters
[a] -> someActionUsingOneParameter
[a, b] -> someActionUsingTwoParameters
_ -> fail "don't know that one, sorry"

I have adapted a lot of my code to use these uni patterns rather than
avoiding them, as most of the time when this happens, it's not an
impossible case for someone to pick the function up somewhere else and
call it in the "wrong" way, and I handle it.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.