IRCBrowse

2024/09/25

2024-09-25 00:00:08 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2024-09-25 00:00:09 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
2024-09-25 00:01:25 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-09-25 00:09:41 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2024-09-25 00:09:59 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-09-25 00:11:18 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2024-09-25 00:12:30 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 00:13:55 +0200itaipu(~itaipu@168.121.98.63) (Ping timeout: 264 seconds)
2024-09-25 00:15:06 +0200demcgovern(~demcgover@216.106.58.132.reverse.socket.net) (Quit: Client closed)
2024-09-25 00:22:19 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-09-25 00:23:18 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 00:27:03 +0200itaipu(~itaipu@168.121.99.42) itaipu
2024-09-25 00:28:03 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-09-25 00:29:03 +0200lucy(~lucy@user/lucy) lucy
2024-09-25 00:38:03 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 00:39:00 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 00:43:52 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-09-25 00:44:36 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds)
2024-09-25 00:46:14 +0200athan(~athan@108.147.188.33) (Ping timeout: 260 seconds)
2024-09-25 00:50:49 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik
2024-09-25 00:54:47 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 01:00:00 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-09-25 01:03:07 +0200marcux(~marcux@177.139.77.85)
2024-09-25 01:03:35 +0200marcux(~marcux@177.139.77.85) (Changing host)
2024-09-25 01:03:35 +0200marcux(~marcux@user/marcux) marcux
2024-09-25 01:08:24 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 01:10:34 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 01:13:32 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 272 seconds)
2024-09-25 01:14:08 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2024-09-25 01:15:29 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-09-25 01:16:56 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2024-09-25 01:16:56 +0200ljdarj1ljdarj
2024-09-25 01:17:35 +0200acidjnk(~acidjnk@p200300d6e72cfb5784448b270f7e5b02.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2024-09-25 01:20:50 +0200marcux(~marcux@user/marcux) (Remote host closed the connection)
2024-09-25 01:20:52 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2024-09-25 01:21:37 +0200ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)
2024-09-25 01:23:46 +0200xff0x_(~xff0x@2405:6580:b080:900:3e09:7111:c63e:2d47)
2024-09-25 01:25:21 +0200xff0x(~xff0x@2405:6580:b080:900:dc1b:498c:28de:28be) (Ping timeout: 276 seconds)
2024-09-25 01:26:21 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 01:28:49 +0200pavonia(~user@user/siracusa) siracusa
2024-09-25 01:30:28 +0200krei-se-(~krei-se@p57af2362.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2024-09-25 01:31:03 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-09-25 01:32:40 +0200krei-se(~krei-se@p57af2362.dip0.t-ipconnect.de) krei-se
2024-09-25 01:36:24 +0200cyphase(~cyphase@user/cyphase) (Ping timeout: 276 seconds)
2024-09-25 01:39:35 +0200sourcetarius(~sourcetar@user/sourcetarius) sourcetarius
2024-09-25 01:40:20 +0200euandreh(~Thunderbi@189.6.105.228) (Ping timeout: 255 seconds)
2024-09-25 01:40:53 +0200cyphase(~cyphase@user/cyphase) cyphase
2024-09-25 01:42:08 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 01:42:36 +0200euandreh(~Thunderbi@189.6.105.228) euandreh
2024-09-25 01:42:52 +0200krei-se(~krei-se@p57af2362.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2024-09-25 01:44:35 +0200krei-se(~krei-se@p57af2362.dip0.t-ipconnect.de) krei-se
2024-09-25 01:45:21 +0200 <raehik> Is there a way to force a type variable to be inferred, in a `data` declaration?
2024-09-25 01:45:59 +0200 <raehik> I have `data Magic (a :: k) = Magic`, which is fine, but `:t Magic` gives `Magic :: forall k (a :: k). Magic a`
2024-09-25 01:47:03 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-09-25 01:47:18 +0200 <raehik> Alternatively, can I do what I want with a pattern synonym?
2024-09-25 01:47:33 +0200 <geekosaur> I'm not even sure what you want
2024-09-25 01:47:35 +0200 <Lears> What /do/ you want, though?
2024-09-25 01:47:50 +0200 <geekosaur> ^5
2024-09-25 01:48:14 +0200 <raehik> I want `Magic :: forall {k} (a :: k). Magic a`
2024-09-25 01:48:36 +0200 <raehik> I want to force `k` to be inferred (because for my uses it will be)
2024-09-25 01:48:45 +0200 <Lears> Perhaps GADTSyntax will allow it?
2024-09-25 01:49:39 +0200 <raehik> hmm not sure how I would write it with GADT syntax (I don't use them much)
2024-09-25 01:50:11 +0200 <Lears> `data Magic a where Magic :: forall {k} (a :: k). Magic a`
2024-09-25 01:50:39 +0200lucy(~lucy@user/lucy) (Ping timeout: 246 seconds)
2024-09-25 01:50:44 +0200 <geekosaur> https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_applications.html#manually-def… which confirms it's only supported with GADTSyntax
2024-09-25 01:52:06 +0200 <geekosaur> and gives an example thereof
2024-09-25 01:52:33 +0200lucy(~lucy@user/lucy) lucy
2024-09-25 01:53:38 +0200 <raehik> thank you very much Lears , geekosaur ! I simply never knew that and didn't find it with my googling
2024-09-25 01:54:46 +0200 <geekosaur> it is kinda unfortunate that this isn't what one normally thinks of with "inferred" (type inference being the usual thing)
2024-09-25 01:55:20 +0200 <raehik> the pattern synonym worked as well, I didn't know they were fine with foralls
2024-09-25 01:55:40 +0200 <geekosaur> I personally think more of "visibility" than "inference" here
2024-09-25 01:55:41 +0200 <raehik> but the GADT is perfect
2024-09-25 01:55:57 +0200 <raehik> geekosaur: Yeah, agreed. I went by the name in the docs
2024-09-25 01:57:22 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-09-25 01:57:55 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 01:58:35 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-09-25 01:58:59 +0200lucy(~lucy@user/lucy) (Ping timeout: 265 seconds)
2024-09-25 02:00:50 +0200lucy(~lucy@user/lucy) lucy
2024-09-25 02:03:57 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-09-25 02:05:16 +0200sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 265 seconds)
2024-09-25 02:06:35 +0200Guest93(~Guest93@5.195.226.142)
2024-09-25 02:08:14 +0200lucy(~lucy@user/lucy) (Ping timeout: 255 seconds)
2024-09-25 02:10:08 +0200lucy(~lucy@user/lucy) lucy
2024-09-25 02:10:20 +0200Guest93(~Guest93@5.195.226.142) (Client Quit)
2024-09-25 02:13:51 +0200ubert1(~Thunderbi@178.165.177.214.wireless.dyn.drei.com) ubert
2024-09-25 02:14:27 +0200ubert(~Thunderbi@77.119.174.223.wireless.dyn.drei.com) (Ping timeout: 265 seconds)
2024-09-25 02:14:28 +0200ubert1ubert
2024-09-25 02:15:01 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 02:19:56 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-09-25 02:28:02 +0200synchromesh(~john@2406:5a00:241a:5600:b8f8:7fb4:fdd7:b64d) (Read error: Connection reset by peer)
2024-09-25 02:28:08 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!)
2024-09-25 02:28:48 +0200xff0x_(~xff0x@2405:6580:b080:900:3e09:7111:c63e:2d47) (Ping timeout: 246 seconds)
2024-09-25 02:29:28 +0200synchromesh(~john@2406:5a00:241a:5600:b8f8:7fb4:fdd7:b64d) synchromesh
2024-09-25 02:30:48 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 02:35:33 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-09-25 02:46:36 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 02:49:46 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 02:51:28 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-09-25 02:52:15 +0200machinedgod(~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 246 seconds)
2024-09-25 03:00:33 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2024-09-25 03:00:55 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643) finn_elija
2024-09-25 03:01:42 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2024-09-25 03:02:24 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 03:07:15 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection)
2024-09-25 03:07:30 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-09-25 03:07:47 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 03:11:11 +0200 <EvanR> 1 = abb⁻¹a⁻¹ (obviously)
2024-09-25 03:11:14 +0200 <EvanR> (ab)⁻¹ = b⁻¹a⁻¹
2024-09-25 03:11:17 +0200 <EvanR> QED
2024-09-25 03:11:36 +0200 <EvanR> this is a theorem about groups, but does it only work for groups?
2024-09-25 03:11:49 +0200 <EvanR> i.e. is group laws too specific
2024-09-25 03:16:39 +0200 <Lears> Groups are pretty general; they only have a few laws. You're already using identity, invertibility and associativity---that's all of them. I suppose you could weaken associativity to `(w * x) * (y * z) = w * ((x * y) * z)`, but I doubt that gives you anything of interest.
2024-09-25 03:17:05 +0200 <monochrom> You have used identity, inverse, associativity. So I say yes, you pretty much need a group.
2024-09-25 03:18:10 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 03:19:08 +0200 <Lears> Ah, no; with identity that's not even a weakening: a * (b * c) = (1 * a) * (b * c) = 1 * ((a * b) * c) = (a * b) * c
2024-09-25 03:20:12 +0200 <EvanR> that's cool
2024-09-25 03:22:04 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2024-09-25 03:23:00 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-09-25 03:26:42 +0200 <EvanR> that formula makes way more sense now, ignoring the mathematical proof of it, after thinking of it like invertible functions. If you want to invert "do b, then do a to the product of that", you have to first undo a then undo b
2024-09-25 03:27:49 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection)
2024-09-25 03:27:53 +0200 <EvanR> waaaaaaaaait
2024-09-25 03:28:00 +0200 <EvanR> I know how it's too specific
2024-09-25 03:28:21 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 03:28:23 +0200 <EvanR> a group is like a groupoid where all the objects are the same
2024-09-25 03:28:36 +0200 <monochrom> Right, without commutativity, the undo of "put on socks, put on shoes" is not "take off socks, take off shoes".
2024-09-25 03:28:37 +0200 <EvanR> shouldn't the same theorem apply to groupoids
2024-09-25 03:29:33 +0200 <haskellbridge> <Bowuigi> It does tho
2024-09-25 03:29:46 +0200 <EvanR> \o/
2024-09-25 03:30:11 +0200 <haskellbridge> <Bowuigi> The socks example was an example of a groupoid rather than a group
2024-09-25 03:30:33 +0200 <haskellbridge> <Bowuigi> Unless you are used to putting socks on top of your shoes
2024-09-25 03:30:40 +0200 <monochrom> :(
2024-09-25 03:30:42 +0200 <EvanR> lol
2024-09-25 03:30:47 +0200 <monochrom> OK fine! :)
2024-09-25 03:31:02 +0200 <monochrom> I think some people do that.
2024-09-25 03:31:22 +0200 <EvanR> not even people who wear sandals and socks do that
2024-09-25 03:31:32 +0200 <monochrom> mom used to advise "it's winter, put on two pants". (I declined.)
2024-09-25 03:31:43 +0200 <EvanR> two pants
2024-09-25 03:31:50 +0200 <EvanR> left leg and right leg
2024-09-25 03:31:55 +0200 <haskellbridge> <Bowuigi> You could use two shirts as an example instead
2024-09-25 03:32:01 +0200geekosaurwonders where overshoes fit here 😛
2024-09-25 03:32:37 +0200 <monochrom> I don't suppose you would put on two layers of overshoes?
2024-09-25 03:33:09 +0200 <monochrom> The "VHS, UHS, HD, UHD, VVVVUUUUHD" progression applies.
2024-09-25 03:33:57 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 03:33:57 +0200 <EvanR> highspeed CMOS
2024-09-25 03:34:05 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection)
2024-09-25 03:34:05 +0200 <monochrom> I mean, if you start having two layers of overshoes, the outer layer would have to be called something like "ultrashoes" or something ridiculous and soon you will run out of superlatives.
2024-09-25 03:34:27 +0200 <EvanR> that's why the layers are indexed by an ordinal
2024-09-25 03:34:54 +0200 <geekosaur> overshoe_{\omega}
2024-09-25 03:35:32 +0200 <monochrom> haha
2024-09-25 03:35:49 +0200ystael(~ystael@user/ystael) (Ping timeout: 248 seconds)
2024-09-25 03:36:16 +0200 <monochrom> Err, s/HS/HF/ # VHF, UHF
2024-09-25 03:37:09 +0200 <geekosaur> that made perfect sense until they figured out how to generate and control microwave frequencies
2024-09-25 03:37:41 +0200 <geekosaur> then they just gave up and switched to Greek suffixes
2024-09-25 03:37:46 +0200 <geekosaur> err, prefixes
2024-09-25 03:38:45 +0200 <EvanR> microwaves, nanowaves, picowaves
2024-09-25 03:38:50 +0200Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2024-09-25 03:39:15 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-09-25 03:39:47 +0200 <geekosaur> I think you're up to X-rays before you need picowaves? maybe even soft gammas
2024-09-25 03:39:56 +0200geekosauris too tired to work out the math
2024-09-25 03:41:21 +0200euandreh(~Thunderbi@189.6.105.228) (Remote host closed the connection)
2024-09-25 03:41:41 +0200euandreh(~Thunderbi@189.6.105.228) euandreh
2024-09-25 03:42:11 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2024-09-25 03:43:28 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 03:47:44 +0200 <c_wraith> according to wikipedia, that's in the gamma range
2024-09-25 03:48:02 +0200athan(~athan@syn-098-153-145-140.biz.spectrum.com) athan
2024-09-25 03:49:00 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-09-25 03:50:22 +0200 <EvanR> HULK SMASH
2024-09-25 03:51:05 +0200 <geekosaur> remember how high that dial got turneed up, those might have been femtos
2024-09-25 03:51:16 +0200 <c_wraith> I have a friend who has both physics training and reads a lot of comics. He claims that Hulks powers come from GAMMA rays, not gamma rays. Whatever that capitalization means.
2024-09-25 03:51:38 +0200 <geekosaur> beats me
2024-09-25 03:52:45 +0200 <EvanR> lol
2024-09-25 03:53:06 +0200 <EvanR> it means he's nucular
2024-09-25 03:54:13 +0200 <monochrom> Would it also be Ray with upper R?
2024-09-25 03:54:29 +0200CrunchyFlakes(~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-09-25 03:54:30 +0200 <c_wraith> No, Ray claims to have been somewhere else at the time
2024-09-25 03:56:45 +0200morb(~morb@pool-108-41-100-120.nycmny.fios.verizon.net)
2024-09-25 03:56:54 +0200CrunchyFlakes(~CrunchyFl@31.19.233.78)
2024-09-25 03:59:13 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn
2024-09-25 04:08:33 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-09-25 04:08:41 +0200 <monochrom> haha
2024-09-25 04:09:14 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2024-09-25 04:11:12 +0200nadja(~dequbed@banana-new.kilobyte22.de) (Ping timeout: 244 seconds)
2024-09-25 04:12:31 +0200nadja(~dequbed@banana-new.kilobyte22.de) dequbed
2024-09-25 04:12:47 +0200sourcetarius_(~sourcetar@user/sourcetarius) sourcetarius
2024-09-25 04:13:08 +0200sourcetarius(~sourcetar@user/sourcetarius) (Read error: Connection reset by peer)
2024-09-25 04:14:47 +0200youthlic(~Thunderbi@user/youthlic) youthlic
2024-09-25 04:17:24 +0200td_(~td@i53870915.versanet.de) (Ping timeout: 260 seconds)
2024-09-25 04:18:51 +0200td_(~td@i5387090E.versanet.de) td_
2024-09-25 04:19:34 +0200merijn(~merijn@204-220-045-062.dynamic.caiway.nl) merijn