2024-09-23 00:15:33 +0200 | joeyadams | (~joeyadams@syn-184-054-105-097.res.spectrum.com) (Quit: Leaving) |
2024-09-23 00:17:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 00:18:13 +0200 | <gwern> | anyway so I guess I should file a ubuntu bug for the ghc package asking for the existing ghc.bash to be installed appropriately? |
2024-09-23 00:21:02 +0200 | <sm> | that sounds good, and/or a ghc bug asking for the script to be updated for latest ghc |
2024-09-23 00:21:33 +0200 | gwern | figures that once it is actually enabled rather than buried in the deepest mustiest part of the ghc repo, then people will start filing bugs on its infelicities |
2024-09-23 00:22:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 00:30:21 +0200 | <gwern> | https://bugs.launchpad.net/ubuntu/+source/ghc/+bug/2081666 |
2024-09-23 00:31:13 +0200 | gwern | (~gwern@user/gwern) () |
2024-09-23 00:31:38 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 245 seconds) |
2024-09-23 00:33:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 00:38:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
2024-09-23 00:48:14 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:467:e53f:ae7e:31ca) |
2024-09-23 00:49:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 00:49:31 +0200 | <haskellbridge> | <sm> I love launchpad, haven't seen it for ages |
2024-09-23 00:49:55 +0200 | <geekosaur> | I just saw it again last night (they broke clang++, dammit) |
2024-09-23 00:50:35 +0200 | geekosaur | just upgraded to 24.04. it's a mixed bag, but generally positive because a lot of annoying bugs going back at least to 20.04 have finally been fixed |
2024-09-23 00:52:57 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
2024-09-23 00:54:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
2024-09-23 00:57:04 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2024-09-23 01:00:25 +0200 | <haskellbridge> | <sm> 👀 |
2024-09-23 01:02:12 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
2024-09-23 01:03:28 +0200 | <geekosaur> | first time I logged in a number of programs were behaving oddly, but exiting and restarting them fixed that. ??? |
2024-09-23 01:03:36 +0200 | <geekosaur> | hope that doesn't repeat on reboot |
2024-09-23 01:05:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 01:08:38 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
2024-09-23 01:09:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
2024-09-23 01:11:24 +0200 | pavonia | (~user@user/siracusa) |
2024-09-23 01:15:13 +0200 | Squared | (~Square@user/square) (Quit: Leaving) |
2024-09-23 01:15:30 +0200 | Squared | (~Square@user/square) |
2024-09-23 01:18:34 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb68200a0aaa61168dda.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
2024-09-23 01:18:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 01:21:35 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
2024-09-23 01:23:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
2024-09-23 01:34:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 01:36:59 +0200 | <cheater> | "i love launchpad" there's no way you're not alone on that |
2024-09-23 01:39:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
2024-09-23 01:43:42 +0200 | rekahsoft | (~rekahsoft@76.69.85.220) |
2024-09-23 01:47:24 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2024-09-23 01:50:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 01:51:41 +0200 | Iceland_jack | (~Iceland_j@user/Iceland-jack:62112) (Ping timeout: 256 seconds) |
2024-09-23 01:53:08 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
2024-09-23 01:55:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 02:06:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 02:11:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-23 02:18:43 +0200 | lucy | (~lucy@user/lucy) (Ping timeout: 245 seconds) |
2024-09-23 02:20:20 +0200 | lucy | (~lucy@user/lucy) |
2024-09-23 02:21:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 02:25:10 +0200 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
2024-09-23 02:26:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
2024-09-23 02:26:57 +0200 | rekahsoft | (~rekahsoft@76.69.85.220) (Remote host closed the connection) |
2024-09-23 02:28:02 +0200 | rekahsoft | (~rekahsoft@76.69.85.220) |
2024-09-23 02:29:54 +0200 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2024-09-23 02:32:27 +0200 | CrunchyFlakes | (~CrunchyFl@31.19.233.78) |
2024-09-23 02:32:28 +0200 | lucy | (~lucy@user/lucy) (Ping timeout: 245 seconds) |
2024-09-23 02:34:35 +0200 | lucy | (~lucy@user/lucy) |
2024-09-23 02:37:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 02:42:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 02:47:39 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:467:e53f:ae7e:31ca) (Quit: Client closed) |
2024-09-23 02:53:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 02:58:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
2024-09-23 03:08:16 +0200 | Squared | (~Square@user/square) (Ping timeout: 244 seconds) |
2024-09-23 03:09:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 03:13:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
2024-09-23 03:25:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 03:29:26 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 252 seconds) |
2024-09-23 03:30:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
2024-09-23 03:40:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 03:44:27 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
2024-09-23 03:48:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-23 03:55:35 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
2024-09-23 03:55:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
2024-09-23 03:58:37 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
2024-09-23 03:59:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 04:04:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
2024-09-23 04:15:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 04:19:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
2024-09-23 04:23:29 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
2024-09-23 04:23:39 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
2024-09-23 04:31:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 04:32:54 +0200 | td_ | (~td@i53870907.versanet.de) (Ping timeout: 246 seconds) |
2024-09-23 04:33:07 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
2024-09-23 04:34:52 +0200 | td_ | (~td@i5387092E.versanet.de) |
2024-09-23 04:35:26 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) |
2024-09-23 04:36:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-23 04:41:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
2024-09-23 04:42:47 +0200 | sdrfan123 | (~sdrfan123@2607:fb90:df8d:eacb:9114:fbb3:f19f:2066) (Quit: Client closed) |
2024-09-23 04:46:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 04:47:52 +0200 | hgolden_ | (~hgolden@204.152.216.106) |
2024-09-23 04:49:38 +0200 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) |
2024-09-23 04:50:24 +0200 | hgolden | (~hgolden@static-198-44-129-115.cust.tzulo.com) (Ping timeout: 246 seconds) |
2024-09-23 04:51:17 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
2024-09-23 04:51:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
2024-09-23 04:52:16 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2024-09-23 04:53:54 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
2024-09-23 05:02:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 05:07:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 05:18:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 05:21:16 +0200 | lucy | (~lucy@user/lucy) (Ping timeout: 252 seconds) |
2024-09-23 05:21:39 +0200 | AlexZenon | (~alzenon@178.34.162.53) (Ping timeout: 260 seconds) |
2024-09-23 05:23:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
2024-09-23 05:25:03 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
2024-09-23 05:25:37 +0200 | AlexZenon | (~alzenon@178.34.162.53) |
2024-09-23 05:28:22 +0200 | lucy | (~lucy@user/lucy) |
2024-09-23 05:34:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 05:34:48 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 276 seconds) |
2024-09-23 05:38:42 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
2024-09-23 05:38:53 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2024-09-23 05:39:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
2024-09-23 05:40:17 +0200 | Lord_of_Life_ | Lord_of_Life |
2024-09-23 05:45:09 +0200 | aforemny_ | (~aforemny@2001:9e8:6ced:3000:cd4e:2ae2:6fde:9c58) |
2024-09-23 05:45:34 +0200 | yellowbean | (~yellowbea@awork087050.netvigator.com) |
2024-09-23 05:46:03 +0200 | aforemny | (~aforemny@2001:9e8:6cce:4f00:eba1:7c6c:4b28:5ad7) (Ping timeout: 246 seconds) |
2024-09-23 05:46:20 +0200 | yellowbean | (~yellowbea@awork087050.netvigator.com) (Remote host closed the connection) |
2024-09-23 05:50:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 05:54:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
2024-09-23 05:59:09 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 06:01:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 06:04:03 +0200 | foul_owl | (~kerry@174-21-143-250.tukw.qwest.net) (Ping timeout: 276 seconds) |
2024-09-23 06:06:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-23 06:17:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 06:17:09 +0200 | foul_owl | (~kerry@185.219.141.162) |
2024-09-23 06:21:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 06:22:55 +0200 | son0p | (~ff@186.121.41.9) (Ping timeout: 264 seconds) |
2024-09-23 06:25:16 +0200 | michalz | (~michalz@185.246.207.205) |
2024-09-23 06:32:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 06:37:46 +0200 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Quit: ZNC 1.8.2 - https://znc.in) |
2024-09-23 06:37:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
2024-09-23 06:38:02 +0200 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) |
2024-09-23 06:48:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 06:53:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 06:54:53 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) |
2024-09-23 06:55:19 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
2024-09-23 06:58:38 +0200 | <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? |
2024-09-23 06:59:44 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Ping timeout: 244 seconds) |
2024-09-23 06:59:54 +0200 | billchenchina- | (~billchenc@113.57.152.160) |
2024-09-23 07:02:42 +0200 | <lambdaRule> | I see that "refl = Refl id" so refl expects Refl constructor with a functor like argument. how does "a" fit the expected type? |
2024-09-23 07:02:50 +0200 | euphores | (~SASL_euph@user/euphores) |
2024-09-23 07:03:53 +0200 | <geekosaur> | `a` is the expected type. The `@` indicates a type application https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_applications.html |
2024-09-23 07:04:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 07:04:45 +0200 | <c_wraith> | ah, why did he reuse the constructor name? I don't expect Refl to have an argument! |
2024-09-23 07:09:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
2024-09-23 07:10:28 +0200 | <lambdaRule> | from what I understand, the expected return type is a:=b, so a := b |
2024-09-23 07:10:28 +0200 | <lambdaRule> | Refl _ |
2024-09-23 07:10:29 +0200 | <lambdaRule> | the hole after Refl should be: forall c. c a -> c b |
2024-09-23 07:10:43 +0200 | <lambdaRule> | I don't see why type a would work |
2024-09-23 07:11:03 +0200 | <Axman6> | what's the full type of refl, including forall? |
2024-09-23 07:11:05 +0200 | <c_wraith> | the @a is on a use of refl, not Refl |
2024-09-23 07:11:32 +0200 | <Axman6> | refl :: forall a. a := a, right? |
2024-09-23 07:12:00 +0200 | <lambdaRule> | right |
2024-09-23 07:12:38 +0200 | <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 |
2024-09-23 07:12:57 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 276 seconds) |
2024-09-23 07:13:53 +0200 | <Axman6> | if we had x = Int :~: Int, then toLiebnitz x would become refl @Int |
2024-09-23 07:14:09 +0200 | <Axman6> | toLeibniz even |
2024-09-23 07:15:43 +0200 | <lambdaRule> | ok, how do we get to a := b from this call? |
2024-09-23 07:15:56 +0200 | <Axman6> | (uh, I guess x :: Int :~: Int; x = Refl, but yo uknow what I mean) |
2024-09-23 07:16:17 +0200 | <Axman6> | that's what refl does, it produces something of type a := a |
2024-09-23 07:17:08 +0200 | <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) |
2024-09-23 07:17:21 +0200 | <lambdaRule> | I still don't see how the input (a :~: b) is used anywhere to get to the result |
2024-09-23 07:17:27 +0200 | <Axman6> | (someone please jump in if I'm completely wrong here) |
2024-09-23 07:19:24 +0200 | <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 |
2024-09-23 07:20:20 +0200 | <c_wraith> | Yeah. When you match on Eq.Refl, it adds (a ~ b) to the context |
2024-09-23 07:20:34 +0200 | <c_wraith> | So GHC treats the two type variables as interchangeable |
2024-09-23 07:21:08 +0200 | <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. |
2024-09-23 07:21:35 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |
2024-09-23 07:21:38 +0200 | <lambdaRule> | I see, it's getting clearer... |
2024-09-23 07:22:15 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2024-09-23 07:22:36 +0200 | <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 |
2024-09-23 07:22:52 +0200 | <Axman6> | if* |
2024-09-23 07:23:05 +0200 | <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 |
2024-09-23 07:23:26 +0200 | <c_wraith> | yes, exactly |
2024-09-23 07:23:47 +0200 | <lambdaRule> | so the key is a ~ b is the information bring into the scope by pattern matching the input |
2024-09-23 07:24:07 +0200 | <c_wraith> | yes. Matching specifically that constructor brings that into scope. |
2024-09-23 07:26:50 +0200 | <lambdaRule> | Thanks a lot! c_wraith, Axman6, geekosaur. |
2024-09-23 07:28:16 +0200 | <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 |
2024-09-23 07:28:55 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 265 seconds) |
2024-09-23 07:30:03 +0200 | <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 |
2024-09-23 07:30:08 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2024-09-23 07:30:13 +0200 | <c_wraith> | all the work is being done in the type system with the GADTs |
2024-09-23 07:30:21 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:caad:a8df:b144:6c96) (Ping timeout: 246 seconds) |
2024-09-23 07:30:22 +0200 | euleritian | (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) |
2024-09-23 07:31:24 +0200 | <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 == |
2024-09-23 07:31:48 +0200 | <Axman6> | that would have been better as a paste... |
2024-09-23 07:33:51 +0200 | billchenchina- | (~billchenc@113.57.152.160) (Ping timeout: 246 seconds) |
2024-09-23 07:34:54 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 07:35:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 07:39:35 +0200 | neuroevolutus | (~neuroevol@37.19.200.139) |
2024-09-23 07:41:19 +0200 | kuribas | (~user@ptr-17d51enh08wgcmf553y.18120a2.ip6.access.telenet.be) |
2024-09-23 07:41:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
2024-09-23 07:41:47 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
2024-09-23 07:42:11 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
2024-09-23 07:42:11 +0200 | ChanServ | +v haskellbridge |
2024-09-23 07:47:26 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
2024-09-23 07:47:51 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
2024-09-23 07:47:51 +0200 | ChanServ | +v haskellbridge |
2024-09-23 07:48:03 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv013mevadflg9a0e.ipv6.telus.net) (Quit: Client closed) |
2024-09-23 07:49:58 +0200 | youthlic | (~Thunderbi@user/youthlic) |
2024-09-23 07:51:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 07:53:22 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb6581c435b27e22238d.dip0.t-ipconnect.de) |
2024-09-23 07:55:19 +0200 | euleritian | (~euleritia@dynamic-176-007-153-048.176.7.pool.telefonica.de) (Ping timeout: 264 seconds) |
2024-09-23 07:56:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
2024-09-23 07:57:02 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2024-09-23 08:02:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 08:07:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-23 08:18:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 08:24:00 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2024-09-23 08:24:40 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2024-09-23 08:24:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 08:25:24 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
2024-09-23 08:34:34 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
2024-09-23 08:35:13 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
2024-09-23 08:35:19 +0200 | CiaoSen | (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
2024-09-23 08:35:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 08:36:53 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) |
2024-09-23 08:37:37 +0200 | euleritian | (~euleritia@dynamic-176-000-020-203.176.0.pool.telefonica.de) |
2024-09-23 08:41:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
2024-09-23 08:41:31 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2024-09-23 08:45:30 +0200 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 252 seconds) |
2024-09-23 08:48:08 +0200 | manwithluck | (~manwithlu@194.177.28.139) |
2024-09-23 08:51:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 08:52:37 +0200 | ft | (~ft@p508db65d.dip0.t-ipconnect.de) (Quit: leaving) |
2024-09-23 08:52:39 +0200 | rvalue | (~rvalue@user/rvalue) |
2024-09-23 08:56:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 08:57:03 +0200 | manwithluck | (~manwithlu@194.177.28.139) (Ping timeout: 245 seconds) |
2024-09-23 08:57:17 +0200 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) |
2024-09-23 08:58:15 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2024-09-23 08:59:23 +0200 | CiaoSen | (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) (Quit: CiaoSen) |
2024-09-23 09:00:06 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2024-09-23 09:00:41 +0200 | caconym | (~caconym@user/caconym) |
2024-09-23 09:03:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-23 09:09:46 +0200 | neuroevolutus | (~neuroevol@37.19.200.139) (Quit: Client closed) |
2024-09-23 09:10:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-23 09:12:53 +0200 | lucy | (~lucy@user/lucy) (Ping timeout: 245 seconds) |
2024-09-23 09:14:05 +0200 | sam113101 | (~sam@modemcable220.199-203-24.mc.videotron.ca) (Ping timeout: 252 seconds) |
2024-09-23 09:14:28 +0200 | ThePenguin7 | ThePenguin |
2024-09-23 09:17:08 +0200 | misterfish | (~misterfis@87.215.131.102) |
2024-09-23 09:17:51 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-09-23 09:25:08 +0200 | CiaoSen | (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) |
2024-09-23 09:35:18 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
2024-09-23 09:38:11 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
2024-09-23 09:38:25 +0200 | biberu\ | (~biberu@user/biberu) |
2024-09-23 09:38:51 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
2024-09-23 09:39:50 +0200 | lucy | (~lucy@user/lucy) |
2024-09-23 09:40:03 +0200 | euleritian | (~euleritia@dynamic-176-000-020-203.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
2024-09-23 09:41:22 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2024-09-23 09:41:42 +0200 | biberu | (~biberu@user/biberu) (Ping timeout: 252 seconds) |
2024-09-23 09:41:43 +0200 | biberu\ | biberu |
2024-09-23 09:42:52 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2024-09-23 09:44:50 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
2024-09-23 09:50:59 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
2024-09-23 09:53:07 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Remote host closed the connection) |
2024-09-23 09:53:30 +0200 | lucy | (~lucy@user/lucy) (Ping timeout: 276 seconds) |
2024-09-23 09:53:38 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 09:53:51 +0200 | xff0x | (~xff0x@2405:6580:b080:900:64be:ce6a:a0a8:1563) (Ping timeout: 246 seconds) |
2024-09-23 09:54:14 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
2024-09-23 09:55:07 +0200 | lucy | (~lucy@user/lucy) |
2024-09-23 09:58:40 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2024-09-23 09:58:48 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 09:59:03 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Remote host closed the connection) |
2024-09-23 10:00:00 +0200 | briandaed | (~root@185.234.210.211) |
2024-09-23 10:00:17 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 10:00:18 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Remote host closed the connection) |
2024-09-23 10:03:02 +0200 | xff0x | (~xff0x@2405:6580:b080:900:b584:aeff:cd71:1980) |
2024-09-23 10:07:01 +0200 | <Lears> | A cute addendum to the topic of Leibniz equality: https://gist.github.com/LSLeary/af10f744b591796c988fda05d7dd65fa |
2024-09-23 10:13:19 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
2024-09-23 10:15:04 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 10:19:02 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
2024-09-23 10:19:49 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
2024-09-23 10:20:48 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
2024-09-23 10:21:06 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
2024-09-23 10:21:27 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
2024-09-23 10:21:34 +0200 | turlando | (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
2024-09-23 10:21:50 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
2024-09-23 10:22:44 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
2024-09-23 10:22:49 +0200 | turlando | (~turlando@user/turlando) |
2024-09-23 10:23:22 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
2024-09-23 10:24:04 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
2024-09-23 10:24:08 +0200 | youthlic | (~Thunderbi@user/youthlic) |
2024-09-23 10:25:12 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Max SendQ exceeded) |
2024-09-23 10:25:40 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) |
2024-09-23 10:25:41 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 10:27:56 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2024-09-23 10:31:24 +0200 | billchenchina- | (~billchenc@2409:894d:2246:bb36:be66:edcf:93e:2d1a) (Ping timeout: 260 seconds) |
2024-09-23 10:31:58 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 10:32:33 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-09-23 10:32:52 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Max SendQ exceeded) |
2024-09-23 10:34:14 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 10:35:07 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Max SendQ exceeded) |
2024-09-23 10:36:07 +0200 | billchenchina- | (~billchenc@103.118.42.229) |
2024-09-23 10:37:01 +0200 | billchenchina- | (~billchenc@103.118.42.229) (Max SendQ exceeded) |
2024-09-23 10:37:38 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
2024-09-23 10:41:46 +0200 | gehmehgeh | gmg |
2024-09-23 10:43:59 +0200 | econo_ | (uid147250@2a03:5180:f::2:3f32) (Quit: Connection closed for inactivity) |
2024-09-23 10:44:24 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 272 seconds) |
2024-09-23 10:45:40 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 10:45:57 +0200 | misterfish | (~misterfis@178.225.142.184) |
2024-09-23 10:54:50 +0200 | __monty__ | (~toonn@user/toonn) |
2024-09-23 11:03:55 +0200 | cns | (~Vengeance@2.219.56.221) |
2024-09-23 11:05:47 +0200 | synchromesh | (~john@2406:5a00:241a:5600:8896:32c3:5ddd:3078) (Read error: Connection reset by peer) |
2024-09-23 11:06:18 +0200 | misterfish | (~misterfis@178.225.142.184) (Ping timeout: 276 seconds) |
2024-09-23 11:06:31 +0200 | synchromesh | (~john@2406:5a00:241a:5600:793d:2863:f8b8:724f) |
2024-09-23 11:10:39 +0200 | misterfish | (~misterfis@h239071.upc-h.chello.nl) |
2024-09-23 11:25:29 +0200 | lucy | (~lucy@user/lucy) (Quit: Lost terminal) |
2024-09-23 11:29:53 +0200 | supercode | (~supercode@user/supercode) |
2024-09-23 11:31:01 +0200 | euandreh | (~Thunderbi@189.6.105.228) (Remote host closed the connection) |
2024-09-23 11:31:50 +0200 | euandreh | (~Thunderbi@189.6.105.228) |
2024-09-23 11:32:18 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) (Ping timeout: 276 seconds) |
2024-09-23 11:33:57 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
2024-09-23 11:37:26 +0200 | identity | (~identity@user/ZharMeny) |
2024-09-23 11:37:54 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2024-09-23 11:43:05 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-09-23 11:49:41 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
2024-09-23 11:53:57 +0200 | raym | (~ray@user/raym) (Ping timeout: 252 seconds) |
2024-09-23 11:58:30 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
2024-09-23 11:58:59 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 12:01:06 +0200 | youthlic | (~Thunderbi@user/youthlic) |
2024-09-23 12:02:30 +0200 | CiaoSen | (~Jura@2a05:5800:2eb:500:ca4b:d6ff:fec1:99da) (Ping timeout: 244 seconds) |
2024-09-23 12:02:46 +0200 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 252 seconds) |
2024-09-23 12:03:21 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
2024-09-23 12:03:33 +0200 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) |
2024-09-23 12:04:46 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
2024-09-23 12:07:01 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 12:10:44 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
2024-09-23 12:12:27 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
2024-09-23 12:13:00 +0200 | euleritian | (~euleritia@dynamic-176-006-134-141.176.6.pool.telefonica.de) |
2024-09-23 12:15:47 +0200 | raym | (~ray@user/raym) |
2024-09-23 12:25:22 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Read error: Connection reset by peer) |
2024-09-23 12:26:09 +0200 | merijn | (~merijn@77.242.116.146) |
2024-09-23 12:27:58 +0200 | hiecaq | (~hiecaq@user/hiecaq) |
2024-09-23 12:29:35 +0200 | talisman` | (~user@2601:644:937c:ed10::ae5) |