2025/12/03

Newest at the top

2025-12-03 20:58:24 +0100 <tomsmeding> (credit doesn't go to me though)
2025-12-03 20:58:12 +0100 <tomsmeding> Leary: it turns out `NOINLINE [0]` yields the desired behaviour, at least on 9.8, 9.10, 9.12 and the 9.14 RC
2025-12-03 20:55:48 +0100spew(~spew@user/spew) (Quit: WeeChat 4.7.2)
2025-12-03 20:47:17 +0100trickard_trickard
2025-12-03 20:44:57 +0100Googulator(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 20:44:09 +0100Googulator(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed)
2025-12-03 20:35:47 +0100Googulator(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 20:35:40 +0100Googulator(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed)
2025-12-03 20:34:58 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-12-03 20:31:12 +0100 <haskellbridge> <Zemyla> I'm not sure, but I think it'd even mean that liftA2 coerce = coerce (<*>).
2025-12-03 20:29:15 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds)
2025-12-03 20:29:11 +0100 <yin> grinds my gears
2025-12-03 20:28:20 +0100 <EvanR> yes
2025-12-03 20:28:07 +0100 <yin> the inner ones
2025-12-03 20:27:54 +0100 <yin> aren't those parenthesis redundant?
2025-12-03 20:27:43 +0100 <lambdabot> Monad ((->) w) => (w -> (w -> a)) -> w -> a
2025-12-03 20:27:39 +0100 <yin> @type join @((->) _)
2025-12-03 20:26:10 +0100 <haskellbridge> <Zemyla> Okay, so it is true.
2025-12-03 20:23:24 +0100ft(~ft@p508db844.dip0.t-ipconnect.de) ft
2025-12-03 20:16:41 +0100Googulator(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 20:13:44 +0100 <Leary> Boiling down to `fmap coerce = coerce`.
2025-12-03 20:13:04 +0100 <Leary> Let g = k = coerce @a @b; h = f = id @a. This satisfies the precondition, giving us: fmap (coerce @a @b) . liftCoercion (coerce @a @a) = coerce @(F a) @(F b) . fmap (id @a)
2025-12-03 20:12:24 +0100 <lambdabot> g . h = k . f => $map_F g . liftCoercion h = liftCoercion k . $map_F f
2025-12-03 20:12:24 +0100 <Leary> @free liftCoercion :: (a -> b) -> F a -> F b
2025-12-03 20:12:11 +0100 <Leary> Zemyla: Say we have `Functor F` with `type role F representational`. That means we have `forall a b. Coercible a b => Coercible (F a) (F b)`. `Coercible` can be modeled as an implicit `->` restricted to canonical no-ops, so (ignoring the other direction) this corresponds to a `liftCoercion :: (a -> b) -> F a -> F b` function operating on the restricted domain.
2025-12-03 20:10:19 +0100lambda_gibbon(~lambda_gi@208.83.175.39) (Ping timeout: 260 seconds)
2025-12-03 20:07:41 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au)
2025-12-03 20:07:28 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-12-03 20:03:15 +0100ljdarj1ljdarj
2025-12-03 20:03:15 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 240 seconds)
2025-12-03 20:01:45 +0100ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-12-03 19:49:56 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-12-03 19:49:01 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-12-03 19:48:48 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
2025-12-03 19:47:48 +0100 <tomsmeding> which sounds like it _ought_ to be true, but I don't know what to conclude that from
2025-12-03 19:46:11 +0100euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2025-12-03 19:45:33 +0100 <tomsmeding> so it sounds like you're asking: if f's argument is representational, do we have `fmap coerce x = coerce x` for `x :: f (a -> b)`
2025-12-03 19:44:24 +0100 <tomsmeding> well, `liftA2 f x y = f <$> x <*> y` is a law
2025-12-03 19:42:46 +0100 <haskellbridge> <Zemyla> If f is representational and Applicative, then does that necessarily imply that liftA2 coerce a b = coerce a <*> b?
2025-12-03 19:37:36 +0100ouilemur(~jgmerritt@user/ouilemur) ouilemur
2025-12-03 19:34:22 +0100skum(~skum@user/skum) skum
2025-12-03 19:33:59 +0100skum(~skum@user/skum) (Quit: WeeChat 4.7.2)
2025-12-03 19:31:52 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-12-03 19:31:25 +0100Anarchos(~Anarchos@91-161-254-16.subs.proxad.net) ()
2025-12-03 19:27:33 +0100target_i(~target_i@user/target-i/x-6023099) target_i
2025-12-03 19:25:53 +0100 <__monty__> tomsmeding: That part of the structure is necessary. Ordering of the elements is significant.
2025-12-03 19:23:52 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au)
2025-12-03 19:23:46 +0100machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod
2025-12-03 19:23:38 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-12-03 19:18:11 +0100mulk(~mulk@pd9514972.dip0.t-ipconnect.de) mulk