Logs on 2024-09-23 (liberachat/#haskell)
| 00:06:06 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:11:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 00:18:43 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 245 seconds) |
| 00:20:20 | → | lucy joins (~lucy@user/lucy) |
| 00:21:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:25:10 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 00:26:50 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 00:26:57 | × | rekahsoft quits (~rekahsoft@76.69.85.220) (Remote host closed the connection) |
| 00:28:02 | → | rekahsoft joins (~rekahsoft@76.69.85.220) |
| 00:29:54 | × | CrunchyFlakes quits (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 00:32:27 | → | CrunchyFlakes joins (~CrunchyFl@31.19.233.78) |
| 00:32:28 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 245 seconds) |
| 00:34:35 | → | lucy joins (~lucy@user/lucy) |
| 00:37:41 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:42:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:47:39 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:467:e53f:ae7e:31ca) (Quit: Client closed) |
| 00:53:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:58:29 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 01:08:16 | × | Squared quits (~Square@user/square) (Ping timeout: 244 seconds) |
| 01:09:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:13:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 01:25:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:29:26 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 252 seconds) |
| 01:30:07 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 01:40:50 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:44:27 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 01:48:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:55:35 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 01:55:40 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 01:58:37 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
| 01:59:34 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:04:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 02:15:22 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:19:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 02:23:29 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
| 02:23:39 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
| 02:31:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:32:54 | × | td_ quits (~td@i53870907.versanet.de) (Ping timeout: 246 seconds) |
| 02:33:07 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
| 02:34:52 | → | td_ joins (~td@i5387092E.versanet.de) |
| 02:35:26 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
| 02:36:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:41:12 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 02:42:47 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
| 02:46:55 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:47:52 | → | hgolden_ joins (~hgolden@204.152.216.106) |
| 02:49:38 | → | robobub joins (uid248673@id-248673.uxbridge.irccloud.com) |
| 02:50:24 | × | hgolden quits (~hgolden@static-198-44-129-115.cust.tzulo.com) (Ping timeout: 246 seconds) |
| 02:51:17 | × | identity quits (~identity@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 02:51:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 02:52:16 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:53:54 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 03:02:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:07:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:18:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:21:16 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 252 seconds) |
| 03:21:39 | × | AlexZenon quits (~alzenon@178.34.162.53) (Ping timeout: 260 seconds) |
| 03:23:18 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 03:25:03 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 03:25:37 | → | AlexZenon joins (~alzenon@178.34.162.53) |
| 03:28:22 | → | lucy joins (~lucy@user/lucy) |
| 03:34:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:34:48 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 03:38:42 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 03:38:53 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 03:39:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 03:40:17 | Lord_of_Life_ | is now known as Lord_of_Life |
| 03:45:09 | → | aforemny_ joins (~aforemny@2001:9e8:6ced:3000:cd4e:2ae2:6fde:9c58) |
| 03:45:34 | → | yellowbean joins (~yellowbea@awork087050.netvigator.com) |
| 03:46:03 | × | aforemny quits (~aforemny@2001:9e8:6cce:4f00:eba1:7c6c:4b28:5ad7) (Ping timeout: 246 seconds) |
| 03:46:20 | × | yellowbean quits (~yellowbea@awork087050.netvigator.com) (Remote host closed the connection) |
| 03:50:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:54:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 03:59:09 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 04:01:15 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:04:03 | × | foul_owl quits (~kerry@174-21-143-250.tukw.qwest.net) (Ping timeout: 276 seconds) |
| 04:06:34 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 04:17:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:17:09 | → | foul_owl joins (~kerry@185.219.141.162) |
| 04:21:46 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 04:22:55 | × | son0p quits (~ff@186.121.41.9) (Ping timeout: 264 seconds) |
| 04:25:16 | → | michalz joins (~michalz@185.246.207.205) |
| 04:32:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:37:46 | × | doyougnu quits (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:37:47 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 04:38:02 | → | doyougnu joins (~doyougnu@syn-045-046-170-068.res.spectrum.com) |
| 04:48:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:53:40 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 04:54:53 | → | lambdaRule joins (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) |
| 04:55:19 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 04:58:38 | <lambdaRule> | Hi, I am confused in this piece of code: "toLeibniz Eq.Refl = refl @a" in the section "Equivalence of Leibniz and propositional equality" (https://ryanglscott.github.io/2021/08/22/leibniz-equality-in-haskell-part-1/), how does it work on the right hand side? |
| 04:59:44 | × | billchenchina- quits (~billchenc@103.118.42.229) (Ping timeout: 244 seconds) |
| 04:59:54 | → | billchenchina- joins (~billchenc@113.57.152.160) |
| 05:02:42 | <lambdaRule> | I see that "refl = Refl id" so refl expects Refl constructor with a functor like argument. how does "a" fit the expected type? |
| 05:02:50 | → | euphores joins (~SASL_euph@user/euphores) |
| 05:03:53 | <geekosaur> | `a` is the expected type. The `@` indicates a type application https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_applications.html |
| 05:04:24 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:04:45 | <c_wraith> | ah, why did he reuse the constructor name? I don't expect Refl to have an argument! |
| 05:09:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 05:10:28 | <lambdaRule> | from what I understand, the expected return type is a:=b, so a := b |
| 05:10:28 | <lambdaRule> | Refl _ |
| 05:10:29 | <lambdaRule> | the hole after Refl should be: forall c. c a -> c b |
| 05:10:43 | <lambdaRule> | I don't see why type a would work |
| 05:11:03 | <Axman6> | what's the full type of refl, including forall? |
| 05:11:05 | <c_wraith> | the @a is on a use of refl, not Refl |
| 05:11:32 | <Axman6> | refl :: forall a. a := a, right? |
| 05:12:00 | <lambdaRule> | right |
| 05:12:38 | <Axman6> | so in toLeibniz :: forall a b. (a :~: b) -> (a := b) when we use refl @a, we're specifically saying we want to call refl with a being _the same `a`_ as our call to toLeibniz |
| 05:12:57 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 276 seconds) |
| 05:13:53 | <Axman6> | if we had x = Int :~: Int, then toLiebnitz x would become refl @Int |
| 05:14:09 | <Axman6> | toLeibniz even |
| 05:15:43 | <lambdaRule> | ok, how do we get to a := b from this call? |
| 05:15:56 | <Axman6> | (uh, I guess x :: Int :~: Int; x = Refl, but yo uknow what I mean) |
| 05:16:17 | <Axman6> | that's what refl does, it produces something of type a := a |
| 05:17:08 | <Axman6> | but we're being specific about which a, it's the same a that the argument to toLeibniz had (and :~: is evidence that a ~ b, so we can produce a := b, a.k.a a := a) |
| 05:17:21 | <lambdaRule> | I still don't see how the input (a :~: b) is used anywhere to get to the result |
| 05:17:27 | <Axman6> | (someone please jump in if I'm completely wrong here) |
| 05:19:24 | <Axman6> | it's not, it's all happening at the type system. But we know that if we received _anything_ of type a :~: b, then it could only have been a value of Refl, which requires that a ~ b, so we've been given evidence that those types are the same. Then we call refl at the type a to produce a := a. The argument is unused, but its type is used |
| 05:20:20 | <c_wraith> | Yeah. When you match on Eq.Refl, it adds (a ~ b) to the context |
| 05:20:34 | <c_wraith> | So GHC treats the two type variables as interchangeable |
| 05:21:08 | <c_wraith> | That's one of the main feature of GADTs, and not really in scope for that post. I think it expect you to know what they do already. |
| 05:21:35 | → | libertyprime joins (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |
| 05:21:38 | <lambdaRule> | I see, it's getting clearer... |
| 05:22:15 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:22:36 | <Axman6> | Notice the definition of :~:: data a :~: b where Refl :: a :~: a -- you can only produce values of type a :~: b is a is equal to b |
| 05:22:52 | <Axman6> | if* |
| 05:23:05 | <lambdaRule> | so the refl call with type a then compiler see that the expected type is a := b but since a ~ b so refl works |
| 05:23:26 | <c_wraith> | yes, exactly |
| 05:23:47 | <lambdaRule> | so the key is a ~ b is the information bring into the scope by pattern matching the input |
| 05:24:07 | <c_wraith> | yes. Matching specifically that constructor brings that into scope. |
| 05:26:50 | <lambdaRule> | Thanks a lot! c_wraith, Axman6, geekosaur. |
| 05:28:16 | <Axman6> | :~: is probably one of the more confusing common uses of GADTs, seeing the usual example of a simple expression tree is useful for understanding how each constructor carries some typoe information which gets exposed by pattern matching |
| 05:28:55 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 265 seconds) |
| 05:30:03 | <c_wraith> | It's really funny looking at everything in Data.Type.Equality with a definition like foo Refl = Refl or bar Refl Refl = Refl |
| 05:30:08 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:30:13 | <c_wraith> | all the work is being done in the type system with the GADTs |
| 05:30:21 | × | jle` quits (~jle`@2603:8001:3b02:84d4:caad:a8df:b144:6c96) (Ping timeout: 246 seconds) |
| 05:30:22 | → | euleritian joins (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) |
| 05:31:24 | <Axman6> | like data Expr a where Num :: Int -> Expr Int; Bool' :: Bool -> Expr Bool; Plus :: Expr a -> Expr a -> Expr a; Eq :: Eq a => Expr a -> Expr a -> Expr Bool. When you pattern match on eval :: Expr a -> a; eval e = case e of Eq a b -> eval a == eval b; ...; we've brought into scope that the two expressions represent something of the same type, and that those types have an Eq constraint so we can use == |
| 05:31:48 | <Axman6> | that would have been better as a paste... |
| 05:33:51 | × | billchenchina- quits (~billchenc@113.57.152.160) (Ping timeout: 246 seconds) |
| 05:34:54 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 05:35:58 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:39:35 | → | neuroevolutus joins (~neuroevol@37.19.200.139) |
| 05:41:19 | → | kuribas joins (~user@ptr-17d51enh08wgcmf553y.18120a2.ip6.access.telenet.be) |
| 05:41:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 05:41:47 | × | haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 05:42:11 | → | haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 05:42:11 | ChanServ | sets mode +v haskellbridge |
| 05:47:26 | × | haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 05:47:51 | → | haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 05:47:51 | ChanServ | sets mode +v haskellbridge |
| 05:48:03 | × | lambdaRule quits (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) (Quit: Client closed) |
| 05:49:58 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:51:44 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:53:22 | → | acidjnk joins (~acidjnk@p200300d6e72cfb6581c435b27e22238d.dip0.t-ipconnect.de) |
| 05:55:19 | × | euleritian quits (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 05:56:32 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 05:57:02 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:02:14 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:07:29 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 06:18:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:24:00 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 06:24:40 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:24:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:25:24 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 06:34:34 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 06:35:13 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:35:19 | → | CiaoSen joins (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
| 06:35:46 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:36:53 | → | jle` joins (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) |
| 06:37:37 | → | euleritian joins (~euleritia@dynamic-176-000-020-203.176.0.pool.telefonica.de) |
| 06:41:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 06:41:31 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 06:45:30 | × | manwithluck quits (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 252 seconds) |
| 06:48:08 | → | manwithluck joins (~manwithlu@194.177.28.139) |
| 06:51:33 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:52:37 | × | ft quits (~ft@p508db65d.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:52:39 | → | rvalue joins (~rvalue@user/rvalue) |
| 06:56:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:57:03 | × | manwithluck quits (~manwithlu@194.177.28.139) (Ping timeout: 245 seconds) |
| 06:57:17 | → | manwithluck joins (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 06:58:15 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:59:23 | × | CiaoSen quits (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) (Quit: CiaoSen) |
| 07:00:06 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:41 | → | caconym joins (~caconym@user/caconym) |
| 07:03:15 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:09:46 | × | neuroevolutus quits (~neuroevol@37.19.200.139) (Quit: Client closed) |
| 07:10:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 07:12:53 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 245 seconds) |
| 07:14:05 | × | sam113101 quits (~sam@modemcable220.199-203-24.mc.videotron.ca) (Ping timeout: 252 seconds) |
| 07:14:28 | ThePenguin7 | is now known as ThePenguin |
| 07:17:08 | → | misterfish joins (~misterfis@87.215.131.102) |
| 07:17:51 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:25:08 | → | CiaoSen joins (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
| 07:35:18 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 07:38:11 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 07:38:25 | → | biberu\ joins (~biberu@user/biberu) |
| 07:38:51 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 07:39:50 | → | lucy joins (~lucy@user/lucy) |
| 07:40:03 | × | euleritian quits (~euleritia@dynamic-176-000-020-203.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:41:22 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:41:42 | × | biberu quits (~biberu@user/biberu) (Ping timeout: 252 seconds) |
| 07:41:43 | biberu\ | is now known as biberu |
| 07:42:52 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 07:44:50 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 07:50:59 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 07:53:07 | × | billchenchina- quits (~billchenc@103.118.42.229) (Remote host closed the connection) |
| 07:53:30 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 276 seconds) |
| 07:53:38 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 07:53:51 | × | xff0x quits (~xff0x@2405:6580:b080:900:64be:ce6a:a0a8:1563) (Ping timeout: 246 seconds) |
| 07:54:14 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 07:55:07 | → | lucy joins (~lucy@user/lucy) |
| 07:58:40 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 07:58:48 | → | merijn joins (~merijn@77.242.116.146) |
| 07:59:03 | × | billchenchina- quits (~billchenc@103.118.42.229) (Remote host closed the connection) |
| 08:00:00 | → | briandaed joins (~root@185.234.210.211) |
| 08:00:17 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 08:00:18 | × | billchenchina- quits (~billchenc@103.118.42.229) (Remote host closed the connection) |
| 08:03:02 | → | xff0x joins (~xff0x@2405:6580:b080:900:b584:aeff:cd71:1980) |
| 08:07:01 | <Lears> | A cute addendum to the topic of Leibniz equality: https://gist.github.com/LSLeary/af10f744b591796c988fda05d7dd65fa |
| 08:13:19 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 08:15:04 | → | merijn joins (~merijn@77.242.116.146) |
| 08:19:02 | → | billchenchina- joins (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
| 08:19:49 | × | billchenchina- quits (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
| 08:20:48 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 08:21:06 | → | billchenchina- joins (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
| 08:21:27 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 08:21:34 | × | turlando quits (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 08:21:50 | × | billchenchina- quits (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
| 08:22:44 | → | billchenchina- joins (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
| 08:22:49 | → | turlando joins (~turlando@user/turlando) |
| 08:23:22 | × | billchenchina- quits (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
| 08:24:04 | → | billchenchina- joins (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
| 08:24:08 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 08:25:12 | × | billchenchina- quits (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
| 08:25:40 | → | billchenchina- joins (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
| 08:25:41 | → | merijn joins (~merijn@77.242.116.146) |
| 08:27:56 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:31:24 | × | billchenchina- quits (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Ping timeout: 260 seconds) |
| 08:31:58 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 08:32:33 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:32:52 | × | billchenchina- quits (~billchenc@103.118.42.229) (Max SendQ exceeded) |
| 08:34:14 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 08:35:07 | × | billchenchina- quits (~billchenc@103.118.42.229) (Max SendQ exceeded) |
| 08:36:07 | → | billchenchina- joins (~billchenc@103.118.42.229) |
| 08:37:01 | × | billchenchina- quits (~billchenc@103.118.42.229) (Max SendQ exceeded) |
| 08:37:38 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 08:41:46 | gehmehgeh | is now known as gmg |
| 08:43:59 | × | econo_ quits (uid147250@2a03:5180:f::2:3f32) (Quit: Connection closed for inactivity) |
| 08:44:24 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 272 seconds) |
| 08:45:40 | → | merijn joins (~merijn@77.242.116.146) |
| 08:45:57 | → | misterfish joins (~misterfis@178.225.142.184) |
| 08:54:50 | → | __monty__ joins (~toonn@user/toonn) |
| 09:03:55 | → | cns joins (~Vengeance@2.219.56.221) |
| 09:05:47 | × | synchromesh quits (~john@2406:5a00:241a:5600:8896:32c3:5ddd:3078) (Read error: Connection reset by peer) |
| 09:06:18 | × | misterfish quits (~misterfis@178.225.142.184) (Ping timeout: 276 seconds) |
| 09:06:31 | → | synchromesh joins (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) |
| 09:10:39 | → | misterfish joins (~misterfis@h239071.upc-h.chello.nl) |
| 09:25:29 | × | lucy quits (~lucy@user/lucy) (Quit: Lost terminal) |
| 09:29:53 | → | supercode joins (~supercode@user/supercode) |
| 09:31:01 | × | euandreh quits (~Thunderbi@189.6.105.228) (Remote host closed the connection) |
| 09:31:50 | → | euandreh joins (~Thunderbi@189.6.105.228) |
| 09:32:18 | × | jle` quits (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) (Ping timeout: 276 seconds) |
| 09:33:57 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
| 09:37:26 | → | identity joins (~identity@user/ZharMeny) |
| 09:37:54 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 09:43:05 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:49:41 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 09:53:57 | × | raym quits (~ray@user/raym) (Ping timeout: 252 seconds) |
| 09:58:30 | × | youthlic quits (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 09:58:59 | → | merijn joins (~merijn@77.242.116.146) |
| 10:01:06 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 10:02:30 | × | CiaoSen quits (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) (Ping timeout: 244 seconds) |
| 10:02:46 | × | manwithluck quits (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 252 seconds) |
| 10:03:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 10:03:33 | → | manwithluck joins (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 10:04:46 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 10:07:01 | → | merijn joins (~merijn@77.242.116.146) |
| 10:10:44 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 10:12:27 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 10:13:00 | → | euleritian joins (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) |
| 10:15:47 | → | raym joins (~ray@user/raym) |
| 10:25:22 | × | hiecaq quits (~hiecaq@user/hiecaq) (Read error: Connection reset by peer) |
| 10:26:09 | → | merijn joins (~merijn@77.242.116.146) |
| 10:27:58 | → | hiecaq joins (~hiecaq@user/hiecaq) |
| 10:29:35 | → | talisman` joins (~user@2601:644:937c:ed10::ae5) |
| 10:31:34 | × | talismanick quits (~user@2601:644:937c:ed10::ae5) (Ping timeout: 260 seconds) |
| 10:34:55 | × | misterfish quits (~misterfis@h239071.upc-h.chello.nl) (Ping timeout: 264 seconds) |
| 10:38:14 | → | misterfish joins (~misterfis@87.215.131.102) |
| 10:42:03 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 10:43:50 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:50:54 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 10:55:30 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 11:07:44 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 11:12:50 | → | merijn joins (~merijn@77.242.116.146) |
| 11:14:18 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:21:19 | → | polyphem joins (~rod@p3ee3fee2.dip0.t-ipconnect.de) |
| 11:26:56 | → | CiaoSen joins (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
| 11:31:24 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 11:34:34 | → | sam113101 joins (~sam@modemcable220.199-203-24.mc.videotron.ca) |
| 11:35:09 | × | CiaoSen quits (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds) |
| 11:39:36 | × | libertyprime quits (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Remote host closed the connection) |
| 11:42:40 | → | Square2 joins (~Square4@user/square) |
| 11:44:27 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 11:45:19 | × | polyphem quits (~rod@p3ee3fee2.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 11:48:53 | × | euleritian quits (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 11:49:11 | → | euleritian joins (~euleritia@77.22.252.56) |
| 12:09:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:10:03 | → | lucy joins (~lucy@user/lucy) |
| 12:13:18 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 12:17:53 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 12:20:58 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:40:39 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
| 12:43:57 | → | euleritian joins (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) |
| 12:47:48 | → | srazkvt joins (~sarah@user/srazkvt) |
| 12:51:01 | × | tt123109783243 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: Ping timeout (120 seconds)) |
| 12:51:26 | → | tt123109783243 joins (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) |
| 13:05:08 | → | Guest61 joins (~Guest57@129.227.235.110) |
| 13:08:49 | × | Guest61 quits (~Guest57@129.227.235.110) (Client Quit) |
| 13:13:48 | × | synchromesh quits (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) (Read error: Connection reset by peer) |
| 13:15:07 | → | synchromesh joins (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) |
| 13:17:52 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:59e2:a84b:249b:3618) |
| 13:22:02 | × | euleritian quits (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:22:19 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 13:28:15 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:59e2:a84b:249b:3618) (Ping timeout: 256 seconds) |
| 13:35:32 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 13:36:55 | → | euleritian joins (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) |
| 13:50:07 | × | euleritian quits (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:50:26 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 13:51:45 | kimiamania208 | is now known as kimiamania |
| 13:55:21 | → | weary-traveler joins (~user@user/user363627) |
| 14:03:24 | → | rosco joins (~rosco@175.136.158.234) |
| 14:07:45 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 14:09:54 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 14:23:23 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 14:27:50 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 265 seconds) |
| 14:29:29 | <raehik> | I want to check two Word64# s for equality, but in the event of inequality, I want to see which byte failed first (from left to right). I could do this with `and64#` and checking the output. Would this be any slower than using `eqWord64#`? |
| 14:31:26 | <merijn> | raehik: Probably not in any sensible manner :p |
| 14:31:30 | <raehik> | In my head, I can make up some assembly where both are the same number of instructions (assuming 8-byte instructions). But it would rely on doing a conditional jump on the boolean op result, which I don't know how to control |
| 14:31:36 | <raehik> | (actually probably I want xor not and but w/e) |
| 14:32:51 | <raehik> | merijn: ok thx just going by feel here. think I do both and compare output assembly |
| 14:33:47 | × | rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 14:35:12 | <raehik> | atrociously pointless optimization for the error case which should not happen much xd |
| 14:35:44 | <merijn> | I mean, that doesn't tell you much either |
| 14:36:01 | <merijn> | Less instructions is not the same as faster |
| 14:36:41 | <raehik> | merijn: that's true, but I figured I could google for general case comparing XOR with whatever gets used for `eqX` |
| 14:36:44 | <merijn> | Like, we're talking performance differences that would probably take you weeks of micro-benchmark writing to determine |
| 14:37:39 | <raehik> | oh. I was most interested in instruction count. I figured that would tell me enough |
| 14:39:06 | <raehik> | I figure I could benchmark the instructions themselves with C if I wanted, but I assume there's some programmer knowledge out there like "your average ALU will do all these operations at the same speed" |
| 14:40:50 | <merijn> | raehik: I mean, benchmarking that accurately in C would still take you weeks of benchmark writing :p |
| 14:40:58 | <merijn> | because micro-benchmarking is HAAAAAAARD |
| 14:41:44 | <raehik> | merijn: thanks I admittedly don't know much about micro-benchmarking! |
| 14:42:35 | <raehik> | thinking more about it, I'm sure the equality check should be faster by an instruction in some way |
| 14:48:24 | → | athan joins (~athan@2600:382:2d0c:946e:ee6b:c0a7:dbf9:e4ec) |
| 14:54:09 | → | supercode joins (~supercode@user/supercode) |
| 15:14:53 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 15:16:07 | <raehik> | merijn: you're right it's much more complex than I thought and I can't find definite answers online for x86(-64) or ARM! I was right thinking that XOR _should_ be faster than "default" equality checks via CMP/SUB, but modern processors & ISAs are clever and weird |
| 15:17:05 | <raehik> | in any case I should still use XOR in the failure case so I will be writing both, so might do some unscientific benchmarking |
| 15:21:03 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 15:23:46 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 15:24:26 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:30:16 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 15:32:09 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 15:32:33 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 248 seconds) |
| 15:32:44 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 15:34:27 | → | lucy joins (~lucy@user/lucy) |
| 15:42:43 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 15:43:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:49:37 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 15:52:12 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 15:53:27 | → | euleritian joins (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) |
| 15:54:44 | → | sabino joins (~sabino@user/sabino) |
| 15:56:02 | × | paddymahoney quits (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 248 seconds) |
| 15:57:03 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Quit: Client closed) |
| 15:59:32 | → | paddymahoney joins (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) |
| 16:00:38 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 16:07:09 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 16:13:18 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 245 seconds) |
| 16:13:49 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 16:15:03 | × | youthlic quits (~Thunderbi@user/youthlic) (Ping timeout: 246 seconds) |
| 16:16:19 | × | myxos quits (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 264 seconds) |
| 16:17:56 | × | euleritian quits (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:18:14 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:25:47 | × | yahb2 quits (~yahb2@user/tomsmeding/bot/yahb2) (Remote host closed the connection) |
| 16:26:43 | → | yahb2 joins (~yahb2@user/tomsmeding/bot/yahb2) |
| 16:26:43 | ChanServ | sets mode +v yahb2 |
| 16:28:45 | × | tomsmeding quits (~tomsmedin@2a01:4f8:c0c:5e5e::2) (Quit: ZNC 1.9.1 - https://znc.in) |
| 16:29:43 | → | tomsmeding joins (~tomsmedin@2a01:4f8:c0c:5e5e::2) |
| 16:30:43 | × | lockywolf quits (~lockywolf@public.lockywolf.net) (Ping timeout: 264 seconds) |
| 16:36:13 | → | ircbrowse_tom joins (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 16:36:14 | Server | sets mode +Cnt |
| 16:40:14 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:40:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:42:46 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:51:03 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 16:51:08 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:51:49 | → | euleritian joins (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) |
| 16:56:13 | × | euleritian quits (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:58:32 | → | ircbrowse_tom joins (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 16:58:33 | Server | sets mode +Cnt |
| 17:00:15 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:02:24 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 17:04:55 | × | Square2 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 17:06:54 | → | ircbrowse_tom joins (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 17:06:56 | Server | sets mode +Cnt |
| 17:14:03 | <probie> | raehik: Can't you just calculate msb(xor(a, b))? It involves no branching, so should be pipeline friendly and (not sure if this is of value in this case) easily vectorisable |
| 17:14:25 | <probie> | s/easily/is easily/ |
| 17:15:32 | <apache2> | Ranhir: CMP/SUB is unlikely to be slower than XOR |
| 17:16:21 | <apache2> | depends a little bit on instruction encoding, but they all add contention on CF |
| 17:16:25 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Quit: Client closed) |
| 17:16:45 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 17:17:12 | → | Squared joins (~Square@user/square) |
| 17:17:40 | <apache2> | anything involving JMP is going to set you back miles compared to those |
| 17:18:40 | <apache2> | sorry Ranhir, meant to highlight raehik |
| 17:18:45 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Client Quit) |
| 17:20:18 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Ping timeout: 276 seconds) |
| 17:22:25 | → | ft joins (~ft@p508db65d.dip0.t-ipconnect.de) |
| 17:22:39 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 17:22:58 | <tomsmeding> | probie raehik: for msb() read 'countLeadingZeros x `div` 8' |
| 17:23:45 | × | synchromesh quits (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) (Read error: Connection reset by peer) |
| 17:24:41 | → | synchromesh joins (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) |
| 17:25:18 | <probie> | oh right, which "byte" not "bit". Are we doing little endian or big endian? |
| 17:28:40 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 17:30:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:31:57 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:36:34 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 17:37:00 | → | myxos joins (~myxos@syn-065-028-251-121.res.spectrum.com) |
| 17:39:54 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 17:40:50 | → | euleritian joins (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) |
| 17:40:59 | <probie> | For little endian, left to right, I end up with `(71## `minusWord#` clz64# (a `xor64#` b)) `uncheckedShiftRL#` 3#` |
| 17:42:52 | <probie> | (with 0## being returned on equality) |
| 17:45:48 | <tomsmeding> | is there someone around who is knowledgeable around asynchronous exceptions? In the FFI chapter of the GHC user guide, there is a code example for allowing C code to wake up a Haskell thread via a put to an MVar: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/ffi.html#waking-up-haskell-threads-from-c |
| 17:45:59 | <probie> | Oh, that doesn't quite work. It returns the _last_ byte |
| 17:46:27 | <tomsmeding> | the code snippet (`import GHC.Conc ...`) takes care to handle asynchronous exceptions that cancel the takeMVar -- but this is all happening inside `mask_`! |
| 17:46:35 | <tomsmeding> | How can there be exceptions in the first place if everything is masked? |
| 17:47:52 | <tomsmeding> | or is takeMVar always interruptible, regardless of the mask context? If so, why is this not mentioned in big screaming letters in the haddocks? |
| 17:48:02 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 17:48:21 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 17:49:27 | <tomsmeding> | oh it's in the fine print here https://hackage.haskell.org/package/base-4.19.0.0/docs/Control-Exception.html#g:13 |
| 17:49:53 | <probie> | If you change it to `ctz#` it returns the first, but numbered backwards (e.g 8 for the first byte, 7 for the second byte etc.) |
| 17:51:19 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 17:51:58 | <tomsmeding> | ok that answers my question. Thank you for rubber ducking :) |
| 17:54:28 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 17:54:40 | <probie> | (9## `minusWord#` ((71## `minusWord#` ctz64# (a `xor64#` b)) `uncheckedShiftRL#` 3#)) `remWord#` 9## -- but now it contains rem, I'm not sure it's worth it |
| 17:58:03 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 18:02:39 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 18:03:54 | × | athan quits (~athan@2600:382:2d0c:946e:ee6b:c0a7:dbf9:e4ec) (Ping timeout: 246 seconds) |
| 18:08:32 | → | Kaya-Sem joins (~Kaya-Sem@231.33-245-81.adsl-dyn.isp.belgacom.be) |
| 18:11:43 | ← | Kaya-Sem parts (~Kaya-Sem@231.33-245-81.adsl-dyn.isp.belgacom.be) () |
| 18:14:49 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:16:04 | × | aforemny_ quits (~aforemny@2001:9e8:6ced:3000:cd4e:2ae2:6fde:9c58) (Ping timeout: 260 seconds) |
| 18:16:06 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 18:16:17 | × | lucy quits (~lucy@user/lucy) (Ping timeout: 248 seconds) |
| 18:16:58 | → | misterfish joins (~misterfis@84.53.85.146) |
| 18:16:59 | → | aforemny joins (~aforemny@2001:9e8:6cf3:8b00:cb2b:3044:3ef3:939f) |
| 18:18:10 | → | lucy joins (~lucy@user/lucy) |
| 18:18:19 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 18:18:41 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 18:24:24 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 18:24:58 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 18:27:46 | → | jinsun joins (~jinsun@user/jinsun) |
| 18:29:14 | × | sabino quits (~sabino@user/sabino) (Quit: Lambda _ -> x) |
| 18:37:41 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds) |
| 18:45:20 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:48:55 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 18:50:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 18:53:27 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 18:58:47 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 19:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:38 | → | caconym joins (~caconym@user/caconym) |
| 19:01:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:02:35 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 19:04:53 | → | jle` joins (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) |
| 19:06:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 19:09:21 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:12:21 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:16:30 | × | euleritian quits (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:16:35 | × | haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 19:17:30 | → | haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 19:17:30 | ChanServ | sets mode +v haskellbridge |
| 19:17:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 19:18:40 | → | euleritian joins (~euleritia@ip5f5ad3f0.dynamic.kabel-deutschland.de) |
| 19:18:56 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 19:21:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:22:42 | × | benjaminl quits (~benjaminl@user/benjaminl) (Read error: Connection reset by peer) |
| 19:22:58 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 19:24:01 | × | kuribas quits (~user@ptr-17d51enh08wgcmf553y.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 19:27:03 | → | weary-traveler joins (~user@user/user363627) |
| 19:28:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:30:07 | × | target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 264 seconds) |
| 19:31:25 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:35:14 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:41:33 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 246 seconds) |
| 19:45:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:48:24 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds) |
| 19:50:39 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 19:54:07 | × | haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 19:54:16 | × | weary-traveler quits (~user@user/user363627) (Read error: Connection reset by peer) |
| 19:54:31 | → | weary-traveler joins (~user@user/user363627) |
| 19:54:40 | → | haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 19:54:40 | ChanServ | sets mode +v haskellbridge |
| 19:54:53 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:54:57 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 19:57:46 | → | weary-traveler joins (~user@user/user363627) |
| 20:01:41 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:06:39 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:17:29 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:22:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 20:23:04 | × | euleritian quits (~euleritia@ip5f5ad3f0.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 20:23:50 | → | euleritian joins (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) |
| 20:33:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:36:21 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 20:38:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:38:21 | → | son0p joins (~ff@191.104.21.8) |
| 20:39:00 | → | Digitteknohippie joins (~user@user/digit) |
| 20:39:18 | × | Digit quits (~user@user/digit) (Ping timeout: 252 seconds) |
| 20:39:43 | → | yobabyk joins (~yobabyk@146-241-13-94.dyn.eolo.it) |
| 20:39:56 | ← | yobabyk parts (~yobabyk@146-241-13-94.dyn.eolo.it) () |
| 20:49:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:53:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 20:54:05 | → | Square2 joins (~Square4@user/square) |
| 20:55:59 | Digitteknohippie | is now known as Digit |
| 20:56:54 | × | Squared quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 20:59:53 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:04:18 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 21:06:25 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 21:09:56 | → | athan joins (~athan@2600:381:e917:4f47:c94d:35e0:82e:9afa) |
| 21:10:31 | → | Pixi` joins (~Pixi@user/pixi) |
| 21:11:12 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 21:12:03 | → | Pixi joins (~Pixi@user/pixi) |
| 21:12:59 | × | Pixi quits (~Pixi@user/pixi) (Client Quit) |
| 21:15:13 | × | Pixi` quits (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 21:20:30 | × | michalz quits (~michalz@185.246.207.205) (Remote host closed the connection) |
| 21:20:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:23:37 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Quit: Client closed) |
| 21:28:49 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 21:36:00 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:37:17 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:39:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:40:34 | → | neuroevolutus joins (~neuroevol@146.70.138.238) |
| 21:44:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 21:46:55 | × | neuroevolutus quits (~neuroevol@146.70.138.238) (Ping timeout: 256 seconds) |
| 21:51:50 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 21:55:26 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:57:41 | × | aforemny quits (~aforemny@2001:9e8:6cf3:8b00:cb2b:3044:3ef3:939f) (Ping timeout: 248 seconds) |
| 21:58:25 | → | aforemny joins (~aforemny@2001:9e8:6cf4:c300:4f5a:3b5d:ebdb:6aa8) |
| 21:58:44 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 22:00:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:02:38 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 22:04:19 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 22:04:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:04:37 | × | euleritian quits (~euleritia@dynamic-176-002-006-097.176.2.pool.telefonica.de) (Read error: Connection reset by peer) |
| 22:04:54 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 22:05:20 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 22:08:23 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:10:43 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Ping timeout: 256 seconds) |
| 22:11:13 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:13:18 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:16:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 22:27:00 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:30:13 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 22:30:25 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 22:31:51 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:33:40 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) |
| 22:38:05 | × | athan quits (~athan@2600:381:e917:4f47:c94d:35e0:82e:9afa) (Ping timeout: 252 seconds) |
| 22:41:40 | × | acidjnk quits (~acidjnk@p200300d6e72cfb6581c435b27e22238d.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 22:42:48 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:43:15 | × | st_aldini quits (~Thunderbi@136.48.22.91) (Remote host closed the connection) |
| 22:49:58 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 22:51:21 | → | st_aldini joins (~Thunderbi@136.48.22.91) |
| 23:01:48 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:05:14 | × | raym quits (~ray@user/raym) (Ping timeout: 260 seconds) |
| 23:06:45 | → | raym joins (~ray@user/raym) |
| 23:10:32 | → | pavonia joins (~user@user/siracusa) |
| 23:11:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 23:11:26 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:1ce7:a140:b870:c72c) (Quit: Client closed) |
| 23:11:36 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 23:14:03 | → | gmg joins (~user@user/gehmehgeh) |
| 23:21:24 | <sm> | @where+ hfd https://www.youtube.com/playlist?list=PLu6SHDdOToSe7ZOw-mR55j2GEjkNTQgrd Haskell for Dilettantes beginner video lessons |
| 23:21:57 | <geekosaur> | were the control chars deliberate? |
| 23:22:14 | <sm> | definitely not.. |
| 23:22:15 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:22:19 | <sm> | I used an irc client and everything |
| 23:22:22 | <sm> | @where+ hfd https://www.youtube.com/playlist?list=PLu6SHDdOToSe7ZOw-mR55j2GEjkNTQgrd Haskell for Dilettantes beginner video lessons |
| 23:22:22 | <lambdabot> | Nice! |
| 23:22:36 | <sm> | These are very very good |
| 23:24:02 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:28fb:ea27:7e6a:7c22) |
| 23:26:58 | → | sdrfan18 joins (~sdrfan123@2607:fb90:df8d:eacb:beef:beef:beef:0) |
| 23:27:13 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:29:29 | → | sdrfan46 joins (~sdrfan123@2607:fb90:df8d:eacb:4a2:2773:db9f:f92f) |
| 23:29:44 | × | td_ quits (~td@i5387092E.versanet.de) (Ping timeout: 260 seconds) |
| 23:30:55 | × | sdrfan46 quits (~sdrfan123@2607:fb90:df8d:eacb:4a2:2773:db9f:f92f) (Client Quit) |
| 23:31:07 | → | sdrfan13 joins (~sdrfan123@2607:fb90:df8d:eacb:beef:15:f00d:abcd) |
| 23:31:11 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:28fb:ea27:7e6a:7c22) (Ping timeout: 256 seconds) |
| 23:32:39 | × | sdrfan13 quits (~sdrfan123@2607:fb90:df8d:eacb:beef:15:f00d:abcd) (Client Quit) |
| 23:32:52 | → | sdrfan123 joins (~sdrfan123@2607:fb90:df8d:eacb:f58b:d898:4d6f:bff4) |
| 23:33:27 | × | sdrfan18 quits (~sdrfan123@2607:fb90:df8d:eacb:beef:beef:beef:0) (Ping timeout: 256 seconds) |
| 23:38:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:42:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 23:48:54 | × | sdrfan123 quits (~sdrfan123@2607:fb90:df8d:eacb:f58b:d898:4d6f:bff4) (Quit: Client closed) |
| 23:51:35 | → | td_ joins (~td@i5387093C.versanet.de) |
| 23:51:38 | → | TonyStone joins (~TonyStone@user/TonyStone) |
| 23:56:51 | × | talisman` quits (~user@2601:644:937c:ed10::ae5) (Ping timeout: 252 seconds) |
All times are in UTC on 2024-09-23.