<div dir="ltr">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 <a href="https://medium.com/@cdsmithus/pair-programming-with-chatgpt-haskell-1c4490b71da6">https://medium.com/@cdsmithus/pair-programming-with-chatgpt-haskell-1c4490b71da6</a> (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.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 26, 2023 at 10:46 AM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto">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:<div dir="auto"><br></div><div dir="auto">1. Data.Biapplicative.traverseBiaWith</div><div dir="auto">2. Data.Sequence.zipWith and Data.Sequence.chunksOf</div><div dir="auto"><br></div><div dir="auto">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.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 26, 2023, 8:34 AM Dan Dart <<a href="mailto:haskellcafe@dandart.co.uk" target="_blank">haskellcafe@dandart.co.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}<br>
<br>
I feel like that's just avoiding facing the problem. It makes sense<br>
though, if you know 100% that there really, really is no other case.<br>
But as previous repliers have said, that's probably not a case for<br>
partials. If it's both known and partial, you're probably using the<br>
wrong datastructure for it. There's a reason many Prelude replacements<br>
don't include partial functions, and there's generally a better<br>
solution for it in them. And even if you're using base Prelude (which<br>
I am 99% of the time), things are only Maybe if they come from<br>
somewhere where they possibly could be.<br>
<br>
So, taking (!?) as an example, if you've statically set a list to<br>
contain a value and want it out, and want to avoid using partial<br>
functions like (!!) then perhaps static lists were not a good use case<br>
for you, is what I think people are getting at.<br>
<br>
> what if args is wrong?<br>
<br>
Another solution I use a lot is to match on lists, e.g.:<br>
<br>
    doSomethingWithListOfParameters :: [Text] -> IO ()<br>
    doSomethingWithListOfParameters xs = \case<br>
        [] -> someActionUsingNoParameters<br>
        [a] -> someActionUsingOneParameter<br>
        [a, b] -> someActionUsingTwoParameters<br>
        _ -> fail "don't know that one, sorry"<br>
<br>
I have adapted a lot of my code to use these uni patterns rather than<br>
avoiding them, as most of the time when this happens, it's not an<br>
impossible case for someone to pick the function up somewhere else and<br>
call it in the "wrong" way, and I handle it.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>