2024-04-25 00:00:34 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2024-04-25 00:03:12 +0200 | <haskellbridge> | <irregularsphere> (continuning discussion about exofunctors) by the way, I realized my code snippet's problem is at `<*>` because that does not appear in the traditional definition of a lax monoidal functor, rather only on Haskell (with their `id f a = f a`) |
2024-04-25 00:03:32 +0200 | <haskellbridge> | <irregularsphere> could have realized this sooner, I know |
2024-04-25 00:04:31 +0200 | <haskellbridge> | <irregularsphere> also, I found freelude which is interesting too |
2024-04-25 00:04:59 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
2024-04-25 00:05:08 +0200 | <ncf> | what problem? |
2024-04-25 00:06:27 +0200 | <ncf> | haskell's definition is something like a lax closed functor, which are equivalent to lax monoidal functors between monoidal closed categories |
2024-04-25 00:07:04 +0200 | Lears | (~Leary]@user/Leary/x-0910699) (Ping timeout: 255 seconds) |
2024-04-25 00:08:01 +0200 | <ncf> | but yes it looks like constraining x -> y is a bit random |
2024-04-25 00:08:46 +0200 | <ncf> | i guess you need that because of the precondition thing on FuncOf? |
2024-04-25 00:12:23 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
2024-04-25 00:15:04 +0200 | <ncf> | i guess the issue here is that Eq is not a *closed* subcategory of Hask |
2024-04-25 00:15:30 +0200 | <ncf> | so you can get away with ConsMonoidal but not ConsApplicative |
2024-04-25 00:18:29 +0200 | <haskellbridge> | <irregularsphere> ncf: constraints asking for too much, e.g. `a (x -> y)` |
2024-04-25 00:18:48 +0200 | <haskellbridge> | <irregularsphere> I need the precondition because of `(<*>) = liftA2 id` |
2024-04-25 00:19:14 +0200 | <haskellbridge> | <irregularsphere> and `liftA2 f a = (<*>) fmapC (f a)` |
2024-04-25 00:20:23 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
2024-04-25 00:20:39 +0200 | <haskellbridge> | <irregularsphere> `liftA2 f a = (<*> (fmapC f a))*` |
2024-04-25 00:21:32 +0200 | <haskellbridge> | <irregularsphere> since `f :: x -> y -> z` then `fmapC` implies `a x, a (y -> z)`, thus `(<*>) fs as = liftA2 id` and `id :: (x -> y) -> x -> y` implies `a (x -> y)` |
2024-04-25 00:23:04 +0200 | <haskellbridge> | <irregularsphere> and yes haskell's Applicative is that (I don't know what a lax closed functor is specifically) but after constraining you don't see `a (x -> y)` that much |
2024-04-25 00:23:23 +0200 | cyphase | (~cyphase@user/cyphase) (Quit: cyphase.com) |
2024-04-25 00:24:32 +0200 | <haskellbridge> | <irregularsphere> I realized `<*>`'s type signature is `f (x -> y) -> f x- > f y`, since `f` is assumed to work on values of `a` then `f (x -> y)` does not make much sense either |
2024-04-25 00:24:38 +0200 | <ncf> | https://ncatlab.org/nlab/show/closed+functor |
2024-04-25 00:25:30 +0200 | <haskellbridge> | <irregularsphere> ah |
2024-04-25 00:25:49 +0200 | <haskellbridge> | <irregularsphere> so my code snippet only works on closed subcategories |
2024-04-25 00:27:29 +0200 | <haskellbridge> | <irregularsphere> well then I guess it being specifically a closed subcategory is not good! imagine `Eq (x -> y)` |
2024-04-25 00:29:35 +0200 | cyphase | (~cyphase@user/cyphase) |
2024-04-25 00:31:56 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2024-04-25 00:37:02 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2024-04-25 00:37:06 +0200 | Pixi__ | (~Pixi@user/pixi) (Quit: Leaving) |
2024-04-25 00:37:53 +0200 | Pixi | (~Pixi@user/pixi) |
2024-04-25 00:39:13 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 256 seconds) |
2024-04-25 00:45:40 +0200 | waldo | (~waldo@user/waldo) (Ping timeout: 268 seconds) |
2024-04-25 00:45:45 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2024-04-25 00:46:31 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2024-04-25 00:46:46 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds) |
2024-04-25 00:51:10 +0200 | waldo | (~waldo@user/waldo) |
2024-04-25 00:51:55 +0200 | sroso | (~sroso@user/SrOso) |
2024-04-25 00:52:22 +0200 | sroso | (~sroso@user/SrOso) (Max SendQ exceeded) |
2024-04-25 00:56:10 +0200 | phma_ | (~phma@2001:5b0:210f:7f28:c0a7:813e:87a3:391e) |
2024-04-25 00:56:38 +0200 | phma | (phma@2001:5b0:2172:c758:72f8:9d6a:4a7b:7a0f) (Read error: Connection reset by peer) |
2024-04-25 00:57:48 +0200 | waldo | (~waldo@user/waldo) (Quit: waldo) |
2024-04-25 00:58:02 +0200 | waldo | (~waldo@user/waldo) |
2024-04-25 00:58:10 +0200 | sroso | (~sroso@user/SrOso) |
2024-04-25 01:04:28 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
2024-04-25 01:07:25 +0200 | zwrv | (~yin@user/zero) (Ping timeout: 246 seconds) |
2024-04-25 01:13:29 +0200 | ph88 | (~ph88@91.64.63.48) (Remote host closed the connection) |
2024-04-25 01:13:30 +0200 | chiselfu1e | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2024-04-25 01:14:17 +0200 | zwrv | (~yin@user/zero) |
2024-04-25 01:14:28 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
2024-04-25 01:19:57 +0200 | peterbecich | (~Thunderbi@47.229.123.186) (Ping timeout: 255 seconds) |
2024-04-25 01:24:00 +0200 | mima | (~mmh@aftr-62-216-211-51.dynamic.mnet-online.de) (Ping timeout: 255 seconds) |
2024-04-25 01:40:11 +0200 | philopsos | (~caecilius@user/philopsos) |
2024-04-25 01:49:48 +0200 | trev | (~trev@user/trev) (Ping timeout: 268 seconds) |
2024-04-25 01:51:08 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2024-04-25 01:51:24 +0200 | trev | (~trev@user/trev) |
2024-04-25 01:55:40 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
2024-04-25 01:58:00 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
2024-04-25 02:04:19 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
2024-04-25 02:21:15 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a709:5227:95bf:dd51) (Ping timeout: 268 seconds) |
2024-04-25 02:31:04 +0200 | kilolympus | (~kilolympu@31.205.200.246) |
2024-04-25 02:41:43 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
2024-04-25 02:43:37 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2024-04-25 02:49:28 +0200 | attebregge | (~adam@user/attebregge) |
2024-04-25 02:50:26 +0200 | zwrv | zzz |
2024-04-25 02:51:14 +0200 | zzz | yin |
2024-04-25 02:53:21 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
2024-04-25 02:54:22 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
2024-04-25 02:55:08 +0200 | pastly | (~pastly@gateway/tor-sasl/pastly) |
2024-04-25 02:56:47 +0200 | waldo | (~waldo@user/waldo) (Ping timeout: 260 seconds) |
2024-04-25 03:03:49 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
2024-04-25 03:04:02 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Remote host closed the connection) |
2024-04-25 03:04:08 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
2024-04-25 03:04:25 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
2024-04-25 03:09:08 +0200 | yin | (~yin@user/zero) (Ping timeout: 260 seconds) |
2024-04-25 03:10:48 +0200 | yin | (~yin@user/zero) |
2024-04-25 03:23:34 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2024-04-25 03:27:50 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 245 seconds) |
2024-04-25 03:29:12 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2024-04-25 03:29:14 +0200 | peterbecich | (~Thunderbi@47.229.123.186) |
2024-04-25 03:29:45 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2024-04-25 03:32:08 +0200 | ghost_ | (~ghost@172-105-178-131.ip.linodeusercontent.com) |
2024-04-25 03:35:24 +0200 | otto_s | (~user@p5b0445f5.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2024-04-25 03:37:02 +0200 | otto_s | (~user@p5b04436d.dip0.t-ipconnect.de) |