Newest at the top
2024-10-06 21:21:02 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2024-10-06 21:20:50 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2024-10-06 21:20:30 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
2024-10-06 21:20:16 +0200 | mud | (~mud@user/kadoban) (Quit: quit) |
2024-10-06 21:18:51 +0200 | <monochrom> | Yeah I'm speaking imprecisely such as "(->) is a monad" :) |
2024-10-06 21:17:56 +0200 | <tomsmeding> | ) |
2024-10-06 21:17:45 +0200 | <tomsmeding> | (well, assuming all of the "encouraged properties" of Eq are indeed laws |
2024-10-06 21:17:43 +0200 | <geekosaur> | I'm tempted to say the real instances are Min (Arg …) and the like; Arg itself is just a helper that's incomplete by itself? |
2024-10-06 21:17:17 +0200 | <tomsmeding> | but yes, assuming extensionality is a law of Eq, then an O(n log n) fmap' for Set would satisfy the functor composition law |
2024-10-06 21:15:49 +0200 | <monochrom> | I think of Arg as a very practical tool that breaks some laws but has just cause. In theoretical discussions, we should count it as non-instances. |
2024-10-06 21:15:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-10-06 21:15:36 +0200 | <tomsmeding> | :D |
2024-10-06 21:15:29 +0200 | <Lears> | cowardly words |
2024-10-06 21:15:17 +0200 | <tomsmeding> | does that make it a law? |
2024-10-06 21:15:11 +0200 | <tomsmeding> | "instances are _encouraged_ to follow these properties:" |
2024-10-06 21:15:08 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
2024-10-06 21:14:54 +0200 | <tomsmeding> | oh hah, yes, the extensionality law |
2024-10-06 21:14:24 +0200 | <Lears> | No, `Arg` is just a lawless convenience. |
2024-10-06 21:14:05 +0200 | <tomsmeding> | if base can do this without a big warning, then surely it's valid? |
2024-10-06 21:13:50 +0200 | <tomsmeding> | Arg is a data type in base whose Eq instance ignores a significant amount of information |
2024-10-06 21:13:14 +0200 | <Lears> | aaron: `Eq` has extensionality. |
2024-10-06 21:12:42 +0200 | tomsmeding | . o O ( https://hackage.haskell.org/package/base-4.14.1.0/docs/src/Data.Semigroup.html#line-298 ) |
2024-10-06 21:12:37 +0200 | <haskellbridge> | <aaron> So really the function doesn't need to be monotonic, it just needs to respect "(==)" |
2024-10-06 21:11:44 +0200 | <tomsmeding> | so the fmapped function may distinguish between elements in the "in-between" state that Set cannot distinguish between, and thus eliminates |
2024-10-06 21:11:41 +0200 | AlexNoo | (~AlexNoo@178.34.162.53) (Ping timeout: 255 seconds) |
2024-10-06 21:11:28 +0200 | <haskellbridge> | <aaron> Lears: what tomsmeding said. "(==)" is only equivalence |
2024-10-06 21:11:04 +0200 | AlexZenon | (~alzenon@178.34.162.53) (Ping timeout: 265 seconds) |
2024-10-06 21:11:03 +0200 | <tomsmeding> | Lears: I guess (==) does not imply actual equality? |
2024-10-06 21:10:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
2024-10-06 21:10:31 +0200 | <Lears> | aaron: Can you demonstrate composition breaking for `Functor' Set`? |
2024-10-06 21:09:51 +0200 | <tomsmeding> | at the very least it's not easy |
2024-10-06 21:09:43 +0200 | <tomsmeding> | probably :p |
2024-10-06 21:09:38 +0200 | <haskellbridge> | <aaron> I think you may be wrong, but idk |
2024-10-06 21:08:48 +0200 | <tomsmeding> | (but I may be wrong there) |
2024-10-06 21:08:38 +0200 | <tomsmeding> | I can imagine, iirc the language that QuantifiedConstraints creates cannot be fully inferred decidably |
2024-10-06 21:08:25 +0200 | AlexNoo_ | (~AlexNoo@178.34.151.120) |
2024-10-06 21:08:07 +0200 | <haskellbridge> | <aaron> In theory QuantifiedConstraints would solve that, but last I checked it had various limitations/bugs which made it not good enough for this |
2024-10-06 21:07:42 +0200 | <haskellbridge> | <aaron> yes |
2024-10-06 21:07:16 +0200 | <tomsmeding> | aaron: in the generalisation to arbitrary categories, you mean? |
2024-10-06 21:06:47 +0200 | <haskellbridge> | <aaron> Also functor requires a quantified constraint "forall a. Ob a => Ob (f a)", and you end up needing to manually help the constraint solver |
2024-10-06 21:06:27 +0200 | <tomsmeding> | acme-dont vibes |
2024-10-06 21:06:04 +0200 | _d0t | (~{-d0t-}@user/-d0t-/x-7915216) {-d0t-} |
2024-10-06 21:06:03 +0200 | <monochrom> | newtype MonotonicFunction a b = It'sMonotonicIPromise (a -> b) |
2024-10-06 21:04:23 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
2024-10-06 21:04:00 +0200 | <tomsmeding> | er, s/data constructor/type constructor of a data type/ |
2024-10-06 21:04:00 +0200 | <haskellbridge> | <aaron> Right, you can't define "Identity :: k -> k" as a newtype. There are ways to work around this, but they're not pretty |
2024-10-06 21:03:41 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Read error: Connection reset by peer) |
2024-10-06 21:03:19 +0200 | <tomsmeding> | because the "result kind" of the kind of a data constructor must be Type (or more precisely TYPE r for some RuntimeRep r)? |
2024-10-06 21:02:23 +0200 | <haskellbridge> | <aaron> It's painful to try to define things like the identity functor "Identity :: k -> k" in haskell |
2024-10-06 21:01:45 +0200 | <haskellbridge> | <aaron> The problem with generalizing functor more has to do with polykinds |