Newest at the top
| 2026-01-27 11:06:41 +0100 | <int-e> | (unless you want to distinguish between linear and quadratic growth, say, but I didn't do that) |
| 2026-01-27 11:06:06 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-01-27 11:05:48 +0100 | <int-e> | jreicher: Anyway. The reason why I wrote up that example was to show that it wouldn't rely on any big patterns or huge numbers of arguments but stay polynomially bounded in the number of cases, at which point the precise parameter you pick stops to matter. |
| 2026-01-27 10:54:17 +0100 | <gentauro> | I really miss the hole eXchange concept :'( |
| 2026-01-27 10:53:56 +0100 | <gentauro> | I was actually there :) |
| 2026-01-27 10:53:29 +0100 | <gentauro> | int-e: and jreicher: I think I found the talk "Simon Peyton Jones - Pattern Match Warnings - How Hard Can It Be?" https://www.youtube.com/watch?v=8hJtTIkDr5U |
| 2026-01-27 10:52:01 +0100 | <int-e> | jreicher: you're still cross-attributing messages from me and gentauro |
| 2026-01-27 10:50:54 +0100 | <jreicher> | I'm just not seeing the problem definition clearly. I freely admit that. |
| 2026-01-27 10:50:45 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds) |
| 2026-01-27 10:50:18 +0100 | <int-e> | and also, in case that wasn't clear, you /can/ translate pattern matching without any blowup if you accept redundant matches |
| 2026-01-27 10:50:18 +0100 | <jreicher> | int-e: I know, which is why I was asking for a more specific definition before, but gentauro just offered "n" as the number of cases. |
| 2026-01-27 10:49:21 +0100 | <int-e> | so it's not analogous to strings at all |
| 2026-01-27 10:49:00 +0100 | <int-e> | jreicher: pattern matching isn't strictly left to right because of wildcard patterns |
| 2026-01-27 10:47:42 +0100 | <jreicher> | Hmm. I thought that would be nlogn. I haven't read the papers yet, but you have max n comparisons of logn length bitstrings |
| 2026-01-27 10:47:33 +0100 | <lambdabot> | [["olleh","lens","world"],["hello","snel","world"],["hello","lens","dlrow"]] |
| 2026-01-27 10:47:32 +0100 | <Axman6> | > map (\x -> peek (reverse (pos x)) x) $ holesOf traverse $ words "hello lens world" |
| 2026-01-27 10:47:10 +0100 | <int-e> | gentauro: an upper bound is not a hardness proof though :P |
| 2026-01-27 10:46:17 +0100 | <gentauro> | rather said, exhaustive PM. |
| 2026-01-27 10:46:05 +0100 | <gentauro> | so PM is a "very difficult" problem to solve |
| 2026-01-27 10:45:54 +0100 | <gentauro> | that's what I recall from the SPJ talk |
| 2026-01-27 10:45:32 +0100 | <gentauro> | jreicher: and int-e if you pm on `case (x_1, x_2, …, x_n) of …` then you will have an upperbound of 2^n cases |
| 2026-01-27 10:43:32 +0100 | oskarw | (~user@user/oskarw) oskarw |
| 2026-01-27 10:42:22 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2026-01-27 10:39:38 +0100 | <tomsmeding> | which is, iirc, polynomially bounded by the collective size of the types it outputs (for all subterms), and thus only exponential if you give it a program that has exponentially large inferred types |
| 2026-01-27 10:38:50 +0100 | <tomsmeding> | ok so the GMTM paper undersells the problem a little bit, because it likens it to the complexity of hindley-milner |
| 2026-01-27 10:38:31 +0100 | <tomsmeding> | ah right |
| 2026-01-27 10:38:17 +0100 | <int-e> | And you can encode 3-SAT if you're checking pattern completeness. |
| 2026-01-27 10:37:58 +0100 | <tomsmeding> | sure, but you can typically turn a computation problem into a decision problem by checking whether the output satisfies some condition |
| 2026-01-27 10:37:28 +0100 | housemate | (~housemate@202.7.248.67) housemate |
| 2026-01-27 10:37:26 +0100 | <jreicher> | tomsmeding: IIRC output size isn't relevant to NP-completeness. That class is only defined for decision problems |
| 2026-01-27 10:36:23 +0100 | <int-e> | ...cases to keep track of. |
| 2026-01-27 10:36:17 +0100 | <int-e> | Where Haskell demands that you match the first argument, then optionally the fourth, then the second, then optionally the fifth, then the third argument, then optionally the sixth... and now if you want to avoid redundant pattern matches, you have to keep track of which of the first 3 arguments were equal to A when tackling the next 3 cases. And you can scale that up to 2*n arguments and 2^n... |
| 2026-01-27 10:35:30 +0100 | <tomsmeding> | Whether this is NP-complete only because the output size may be exponential, or whether it may also be if the output size is small, I don't know |
| 2026-01-27 10:35:07 +0100 | <jreicher> | Ta |
| 2026-01-27 10:34:02 +0100 | <tomsmeding> | (that first paper describes the algorithm in GHC before the newest LYG algorithm; the LYG paper ( https://dl.acm.org/doi/pdf/10.1145/3408989 ) claims it has the same complexity as that) |
| 2026-01-27 10:33:41 +0100 | housemate | (~housemate@202.7.248.67) (Quit: https://ineedsomeacidtocalmmedown.space/) |
| 2026-01-27 10:33:12 +0100 | <int-e> | Something like this should do the trick: https://paste.debian.net/hidden/81e97dc6 |
| 2026-01-27 10:33:00 +0100 | <tomsmeding> | it's pattern match exhaustivity checking |
| 2026-01-27 10:32:48 +0100 | <jreicher> | tomsmeding: but why is that pattern matching? |
| 2026-01-27 10:32:27 +0100 | <tomsmeding> | (citation: section 3.4 of https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/icfp2015.pdf ; cited work: https://epubs.siam.org/doi/abs/10.1137/S0097539793246252 ) |
| 2026-01-27 10:32:15 +0100 | <tomsmeding> | jreicher: > Sekar et al. [25] show that the problem of finding redundant clauses is NP-complete, by encoding the boolean satisfiability (SAT) problem into it. |
| 2026-01-27 10:31:41 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-01-27 10:29:18 +0100 | <int-e> | jreicher: I wasn't answering you anyway, just clarifying what I wrote. |
| 2026-01-27 10:29:04 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2026-01-27 10:28:15 +0100 | <jreicher> | That's still vague. |
| 2026-01-27 10:28:04 +0100 | <jreicher> | tomsmeding: what's the parameter then? What's "n", if you know what I mean? |
| 2026-01-27 10:28:02 +0100 | <int-e> | exponential in the number of cases in the source code |
| 2026-01-27 10:27:33 +0100 | <tomsmeding> | jreicher: exhaustivity checking, I think |
| 2026-01-27 10:27:30 +0100 | <int-e> | gentauro: Doesn't ring a bell but I imagine that if you implement Haskell's pattern matching while avoiding matching the same scrutinee twice, you'll end up with cases that have to keep track of exponentially many cases of what has been matched and what hasn't, and correspondingly, exponentially many code paths. |
| 2026-01-27 10:27:22 +0100 | <jreicher> | Linear is inefficient. I just don't understand why it would be worse than linear. |