Newest at the top
2025-03-21 16:36:10 +0100 | <absence> | Proving things with singletons sounds like it will quickly escalate into "not worth it". :p |
2025-03-21 16:34:24 +0100 | <tomsmeding> | we're in #haskell, not in #agda ;) |
2025-03-21 16:34:04 +0100 | <EvanR> | type O |
2025-03-21 16:34:00 +0100 | <EvanR> | er |
2025-03-21 16:33:58 +0100 | <EvanR> | oh was reading : as "type off" |
2025-03-21 16:33:57 +0100 | <tomsmeding> | seems so |
2025-03-21 16:33:55 +0100 | <lambdabot> | True |
2025-03-21 16:33:54 +0100 | <tomsmeding> | > x == x |
2025-03-21 16:33:35 +0100 | <EvanR> | x = x ? |
2025-03-21 16:33:18 +0100 | <tomsmeding> | Now, even the implication `Subset a b => Subset (x:a) (x:b)` is not directly inferrable from the given instances, but you could prove it perhaps, given singletons for those lists |
2025-03-21 16:32:49 +0100 | <absence> | Oh right, that makes sense. |
2025-03-21 16:32:01 +0100 | <tomsmeding> | [1,1] is a subset of [1,2], but [1] is not a subset of [2] |
2025-03-21 16:31:36 +0100 | <tomsmeding> | absence: sure, Subset a b implies Subset (x:a) (x:b). But the other way round does not hold |
2025-03-21 16:31:12 +0100 | <absence> | I'm not sure I see how adding an x to both of them breaks the subset relationship... |
2025-03-21 16:30:27 +0100 | as___ | (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
2025-03-21 16:28:31 +0100 | berzerk | (~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
2025-03-21 16:26:47 +0100 | aristid | (sid1599@id-1599.uxbridge.irccloud.com) |
2025-03-21 16:25:56 +0100 | jackdk | (sid373013@cssa/jackdk) jackdk |
2025-03-21 16:25:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-03-21 16:24:44 +0100 | <tomsmeding> | that |
2025-03-21 16:24:37 +0100 | <tomsmeding> | absence: Note that `Subset (x : list1) (x : list2)` is NOT equivalent to `Subset list1 list2`: the former allows elements of list1 to be equal to x, whereas the latter only allows that if x is in list2 |
2025-03-21 16:24:29 +0100 | <int-e> | Looks like Subset (x : list1) (x : list2) should simplify to Subset list1 (x : list2), but there's nothing that ensures that list1 doesn't contain another x... |
2025-03-21 16:23:43 +0100 | aristid | (sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 268 seconds) |
2025-03-21 16:23:42 +0100 | jackdk | (sid373013@cssa/jackdk) (Ping timeout: 244 seconds) |
2025-03-21 16:23:29 +0100 | <absence> | Speaking of vibes, it feels vaguely similar to "(Monad (t m), Monad m, MonadTrans t) =>", so maybe something something QuantifiedConstraints...? |
2025-03-21 16:22:57 +0100 | taktoa[c] | (sid282096@id-282096.tinside.irccloud.com) taktoa[c] |
2025-03-21 16:22:45 +0100 | <tomsmeding> | ah, so `Subset list1 list2 => Subset (x : list1) (x : list2)` itself isn't even directly derivable |
2025-03-21 16:21:38 +0100 | taktoa[c] | (sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 244 seconds) |
2025-03-21 16:21:17 +0100 | <absence> | Here's the constraint by the way: https://hackage.haskell.org/package/effectful-core-2.5.1.0/docs/src/Effectful.Internal.Effect.html… |
2025-03-21 16:20:54 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-03-21 16:20:50 +0100 | <tomsmeding> | I'm not 100% sure this is what you are running into, but it has a similar "vibe" :p |
2025-03-21 16:20:33 +0100 | <tomsmeding> | you have to modify the class |
2025-03-21 16:20:29 +0100 | <tomsmeding> | no |
2025-03-21 16:20:11 +0100 | <absence> | Can I do that if the constraint and the function that needs it are defined in a third-party library? |
2025-03-21 16:19:58 +0100 | <tomsmeding> | if you don't know what I'm talking about, or don't know how it applies to your case, you'll have to share the definition of that Subset thing |
2025-03-21 16:19:35 +0100 | <tomsmeding> | the latter is normally _not_ what GHC does |
2025-03-21 16:19:26 +0100 | <tomsmeding> | that allows ghc to, given an `instance C A => C T` not only infer `C T` from `C A`, but furthermore conclude from evidence of `C T` that `C A` must also hold |
2025-03-21 16:18:44 +0100 | <tomsmeding> | absence: I have a feeling that this is an X-Y problem, and that the answer is a common-ish trick that I don't know a name for: define an associated type family to your class where the right-hand sides are precisely the instance contexts, then add that type family as a _superclass_ constraint to the class |
2025-03-21 16:17:53 +0100 | wildsalander | (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
2025-03-21 16:16:55 +0100 | <absence> | When using a constraint called Subset, which takes two type-level lists, I find myself having to use "Subset (x : list1) (x : list2) => ..." instead of just "Subset list1 list2". Is there a way to convince the type checker that the x is superfluous? |
2025-03-21 16:16:48 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2025-03-21 16:15:31 +0100 | bsima | (~bsima@143.198.118.179) bsima |
2025-03-21 16:15:06 +0100 | bsima | (~bsima@143.198.118.179) (Quit: ZNC 1.8.2 - https://znc.in) |
2025-03-21 16:14:20 +0100 | berzerk | (~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) |
2025-03-21 16:12:25 +0100 | as___ | (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) |
2025-03-21 16:11:49 +0100 | as__ | (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 244 seconds) |
2025-03-21 16:08:17 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
2025-03-21 16:07:58 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2025-03-21 16:07:07 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
2025-03-21 16:06:48 +0100 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |