Logs on 2024-09-05 (liberachat/#haskell)
| 00:03:56 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 00:04:09 | → | Sciencentistguy joins (~sciencent@hacksoc/ordinary-member) |
| 00:04:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:04:36 | → | neuroevolutus joins (~neuroevol@146.70.211.24) |
| 00:05:18 | → | weary-traveler joins (~user@user/user363627) |
| 00:16:19 | <EvanR> | dependent linear haskell is something else |
| 00:16:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 00:16:59 | <EvanR> | idris diverges from haskellness heavily in the area of type classes |
| 00:17:19 | <EvanR> | see "type classes vs the world" |
| 00:17:41 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 00:18:23 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:22:00 | → | weary-traveler joins (~user@user/user363627) |
| 00:23:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 00:33:50 | <haskellbridge> | <thirdofmay18081814goya> can system f\omega model haskell? |
| 00:34:07 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:34:54 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 00:37:16 | <justsomeguy> | ! |
| 00:39:17 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 00:41:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 00:42:14 | → | weary-traveler joins (~user@user/user363627) |
| 00:44:11 | × | athan_ quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 00:47:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 00:47:38 | → | weary-traveler joins (~user@user/user363627) |
| 00:48:19 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 00:48:32 | <d34df00d> | EvanR: oh that's funny, I'm writing a post for my blog about idris interfaces vs haskell classes. |
| 00:48:51 | <d34df00d> | Idris' interfaces are basically a syntactic sugar for `auto` implicit arguments. |
| 00:49:23 | <d34df00d> | That is, a function/interface constraint is this sugar. |
| 00:49:42 | <d34df00d> | The interface itself is just a type [constructor], which makes lots of Haskell extensions ranging from ConstraintKinds to QuantifiedConstraints redundant. |
| 00:49:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:50:05 | <d34df00d> | The cost is that Idris has no coherence of interfaces, and even the usage of (==) in a context like (Eq a, Ord a) => ... is ambiguous. |
| 00:50:27 | → | troydm joins (~troydm@user/troydm) |
| 00:50:58 | <d34df00d> | That is, because there are actually two `Eq a` in scope — the explicit one and the Ord's superclass one. |
| 00:51:55 | <d34df00d> | Also, `C1 a => C2 a => t` and `(C1 a, C2 a) => t` and `C2 a => C1 a => t` are three distinct types that don't unify. |
| 00:52:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 00:52:54 | → | weary-traveler joins (~user@user/user363627) |
| 00:53:06 | <d34df00d> | Also, re linear types, it kinda sucks that linear-base doesn't have unboxed linear mutable vectors. Boxed ones are slooooow. |
| 00:54:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 01:00:16 | <justsomeguy> | As a beginner with Haskell I've had a hard time working with arrays in general. |
| 01:03:06 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya F omega is a superset of Haskell (Core is system FC, an extension of system F), tho it lacks many of the familiar features (typeclasses and type families, mainly) |
| 01:04:47 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: thanks a lot! |
| 01:04:59 | × | lockywolf quits (~lockywolf@public.lockywolf.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:05:27 | × | neuroevolutus quits (~neuroevol@146.70.211.24) (Ping timeout: 256 seconds) |
| 01:05:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:06:05 | <Axman6> | justsomeguy: what are you trying to do with them? They're not a particularly common structure in most Haskell programs, unless you need a) random access and b) don't need to update them much (though we have a lot of good support for mutable arrays too) |
| 01:06:49 | → | lockywolf joins (~lockywolf@public.lockywolf.net) |
| 01:07:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:08:14 | → | weary-traveler joins (~user@user/user363627) |
| 01:08:40 | <d34df00d> | I'm also curious if the instances of the form `MArray (STUArray s) Ty (ST s)` should better be replaced by `s ~ s' => MArray (STUArray s') Int16 (ST s)` to guide type inference in contexts like `foo <- unsafeNewArray_ @(STUArray _) ...` |
| 01:09:24 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 01:09:28 | <d34df00d> | (read that Int16 as Ty, of course) |
| 01:10:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 01:13:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:13:36 | → | weary-traveler joins (~user@user/user363627) |
| 01:15:49 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 01:18:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:18:54 | → | weary-traveler joins (~user@user/user363627) |
| 01:21:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:23:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:24:14 | → | weary-traveler joins (~user@user/user363627) |
| 01:26:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:28:22 | <monochrom> | BTW what does System FC add to System F? |
| 01:29:11 | <haskellbridge> | <thirdofmay18081814goya> monochrom: "type equalities and coercions", am trying to understand what this means |
| 01:29:19 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:29:34 | → | weary-traveler joins (~user@user/user363627) |
| 01:29:55 | <haskellbridge> | <thirdofmay18081814goya> "coercions serve as evidence for type equalities" |
| 01:31:41 | <probie> | monochrom: C |
| 01:32:17 | <Axman6> | nah clearly they're multiplied, that'd be F+C |
| 01:32:53 | <Axman6> | it adds FC-F |
| 01:33:19 | × | vglfr quits (~vglfr@2601:14d:4e01:1370:919a:c941:4142:9778) (Ping timeout: 260 seconds) |
| 01:33:28 | → | vglfr joins (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) |
| 01:34:38 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 01:34:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:34:54 | → | weary-traveler joins (~user@user/user363627) |
| 01:37:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:39:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:40:15 | → | weary-traveler joins (~user@user/user363627) |
| 01:42:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 01:45:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:45:35 | → | weary-traveler joins (~user@user/user363627) |
| 01:53:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:55:09 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 01:55:44 | <monochrom> | :( :) |
| 01:58:31 | <d34df00d> | FC really stands for Football Club. |
| 01:58:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 01:58:37 | <monochrom> | If https://www.systemf.com.au/ wants to form a football team, what would they call the team? Answer: System FC. >:) |
| 02:00:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:00:54 | → | weary-traveler joins (~user@user/user363627) |
| 02:01:21 | × | cross quits (~cross@spitfire.i.gajendra.net) (Ping timeout: 244 seconds) |
| 02:05:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:06:14 | → | weary-traveler joins (~user@user/user363627) |
| 02:08:50 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:11:19 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:11:40 | → | weary-traveler joins (~user@user/user363627) |
| 02:13:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 02:16:21 | × | czy quits (~user@2a00:23c6:54a8:6301:5024:a70a:b7d6:6a68) (Ping timeout: 265 seconds) |
| 02:16:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:16:45 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 02:16:54 | → | weary-traveler joins (~user@user/user363627) |
| 02:17:31 | → | cross joins (~cross@spitfire.i.gajendra.net) |
| 02:21:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:22:14 | → | weary-traveler joins (~user@user/user363627) |
| 02:24:37 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:27:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:27:34 | → | weary-traveler joins (~user@user/user363627) |
| 02:28:33 | → | uli-fem joins (~user@user/uli-fem) |
| 02:32:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 02:32:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:32:54 | → | weary-traveler joins (~user@user/user363627) |
| 02:33:25 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 02:33:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:35:45 | × | uli-fem quits (~user@user/uli-fem) (Read error: Connection reset by peer) |
| 02:37:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:38:14 | → | weary-traveler joins (~user@user/user363627) |
| 02:38:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 02:43:19 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:43:34 | → | weary-traveler joins (~user@user/user363627) |
| 02:48:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:48:57 | → | weary-traveler joins (~user@user/user363627) |
| 02:49:25 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:54:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 02:54:24 | × | td_ quits (~td@i5387092A.versanet.de) (Ping timeout: 260 seconds) |
| 02:56:16 | → | td_ joins (~td@i53870939.versanet.de) |
| 02:58:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 02:59:14 | → | weary-traveler joins (~user@user/user363627) |
| 03:04:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:04:34 | → | weary-traveler joins (~user@user/user363627) |
| 03:05:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:09:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:09:54 | → | weary-traveler joins (~user@user/user363627) |
| 03:10:14 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:14:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:15:14 | → | weary-traveler joins (~user@user/user363627) |
| 03:18:37 | → | Axman6 joins (~Axman6@user/axman6) |
| 03:19:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:20:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:20:34 | → | weary-traveler joins (~user@user/user363627) |
| 03:24:05 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 03:25:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:25:54 | → | weary-traveler joins (~user@user/user363627) |
| 03:27:13 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 248 seconds) |
| 03:27:56 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 03:28:15 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 03:30:16 | → | Axma92047 joins (~Axman6@user/axman6) |
| 03:30:59 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:31:14 | → | weary-traveler joins (~user@user/user363627) |
| 03:32:09 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 03:34:50 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:36:48 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 03:40:05 | × | aforemny quits (~aforemny@i59F516D7.versanet.de) (Ping timeout: 248 seconds) |
| 03:40:20 | → | aforemny_ joins (~aforemny@i59F516F7.versanet.de) |
| 03:40:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 03:45:35 | Axma92047 | is now known as Axman6 |
| 03:46:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:46:34 | → | weary-traveler joins (~user@user/user363627) |
| 03:51:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:51:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:51:54 | → | weary-traveler joins (~user@user/user363627) |
| 03:56:34 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 03:56:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 03:57:14 | → | weary-traveler joins (~user@user/user363627) |
| 04:02:11 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 04:02:19 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:02:34 | → | weary-traveler joins (~user@user/user363627) |
| 04:06:54 | → | rosco joins (~rosco@175.136.158.234) |
| 04:07:27 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:07:39 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:07:54 | → | weary-traveler joins (~user@user/user363627) |
| 04:08:32 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 04:12:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 04:12:58 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:13:14 | → | weary-traveler joins (~user@user/user363627) |
| 04:18:19 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:18:34 | → | weary-traveler joins (~user@user/user363627) |
| 04:21:38 | × | pounce quits (~pounce@user/cute/pounce) (Ping timeout: 248 seconds) |
| 04:23:13 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:23:38 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:23:54 | → | weary-traveler joins (~user@user/user363627) |
| 04:28:59 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:29:14 | → | weary-traveler joins (~user@user/user363627) |
| 04:32:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 04:34:17 | → | uli-fem joins (~uli-fem@120.18.170.208) |
| 04:34:18 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 04:34:36 | → | weary-traveler joins (~user@user/user363627) |
| 04:34:50 | × | uli-fem quits (~uli-fem@120.18.170.208) (Changing host) |
| 04:34:50 | → | uli-fem joins (~uli-fem@user/uli-fem) |
| 04:35:51 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:36:43 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 04:40:52 | × | sp1ff quits (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Write error: Connection reset by peer) |
| 04:41:06 | → | sp1ff joins (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 04:43:41 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:47:57 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 04:48:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 04:58:21 | → | michalz joins (~michalz@185.246.207.205) |
| 04:59:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:04:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 05:06:56 | × | zlqrvx quits (~zlqrvx@user/zlqrvx) (Quit: %quit%) |
| 05:07:19 | → | zlqrvx joins (~zlqrvx@user/zlqrvx) |
| 05:09:34 | × | uli-fem quits (~uli-fem@user/uli-fem) (Quit: uli-fem) |
| 05:11:57 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 05:12:34 | → | berberman joins (~berberman@user/berberman) |
| 05:15:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:17:23 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 255 seconds) |
| 05:21:18 | × | mud quits (~mud@user/kadoban) (Quit: quit) |
| 05:22:28 | × | jle` quits (~jle`@2603:8001:3b02:84d4:cf52:aad8:ec6d:eddd) (Ping timeout: 245 seconds) |
| 05:23:47 | → | jle` joins (~jle`@2603:8001:3b02:84d4:2fca:bfe0:41f4:4c2b) |
| 05:24:17 | × | rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 05:24:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 05:24:29 | → | euphores joins (~SASL_euph@user/euphores) |
| 05:25:03 | → | mud joins (~mud@user/kadoban) |
| 05:25:32 | → | crvs joins (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) |
| 05:25:40 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 05:26:22 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 05:30:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:33:09 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 05:34:57 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 05:35:51 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:35:56 | → | euleritian joins (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 05:41:43 | BA_Dragon | is now known as A_Dragon |
| 05:42:06 | × | Artea quits (~Lufia@2001:41d0:404:200::2d7) (Remote host closed the connection) |
| 05:44:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 05:56:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:01:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 06:02:09 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 06:03:14 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:07:46 | → | pounce joins (~pounce@user/cute/pounce) |
| 06:10:31 | → | rosco joins (~rosco@175.136.158.234) |
| 06:11:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:16:35 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 06:18:54 | → | acidjnk_new joins (~acidjnk@p200300d6e72cfb86616a3f2ff56a8996.dip0.t-ipconnect.de) |
| 06:21:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:25:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 06:26:15 | → | ubert joins (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) |
| 06:30:36 | × | ubert quits (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 246 seconds) |
| 06:31:35 | → | hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 06:32:38 | → | ubert joins (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) |
| 06:36:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:36:54 | × | ubert quits (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 246 seconds) |
| 06:37:52 | → | Axman6 joins (~Axman6@user/axman6) |
| 06:39:23 | × | euleritian quits (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:39:41 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:41:27 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 06:43:35 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:45:51 | × | mikess quits (~mikess@user/mikess) (Ping timeout: 276 seconds) |
| 06:46:14 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:48:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 06:52:31 | → | Axman3650 joins (~Axman6@user/axman6) |
| 06:54:31 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 06:57:41 | → | misterfish joins (~misterfis@87.215.131.102) |
| 06:57:54 | × | ft quits (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:58:59 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 06:59:18 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:00:42 | → | euleritian joins (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 07:04:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 07:09:09 | → | ash3en joins (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 07:10:51 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 07:15:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:18:09 | × | riatre quits (~quassel@2001:310:6000:f::5198:1) (Ping timeout: 248 seconds) |
| 07:20:22 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 07:30:12 | × | ash3en quits (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 07:34:42 | → | ash3en joins (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 07:39:45 | → | Guest84 joins (~Guest37@159.146.64.69) |
| 07:42:25 | × | Guest84 quits (~Guest37@159.146.64.69) (Client Quit) |
| 07:48:59 | × | fn_lumi quits (3d621153a5@2a03:6000:1812:100::df7) (Ping timeout: 260 seconds) |
| 07:49:34 | × | flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 260 seconds) |
| 07:49:34 | × | shawwwn quits (sid6132@id-6132.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 07:49:34 | × | edwardk quits (sid47016@haskell/developer/edwardk) (Ping timeout: 260 seconds) |
| 07:49:56 | → | flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 07:50:09 | × | [exa] quits (~exa@user/exa/x-3587197) (Ping timeout: 260 seconds) |
| 07:50:09 | × | rembo10 quits (~rembo10@main.remulis.com) (Ping timeout: 260 seconds) |
| 07:50:09 | × | liskin quits (~liskin@xmonad/liskin) (Ping timeout: 260 seconds) |
| 07:50:31 | → | [exa] joins (~exa@2001:15e8:110:7d00::117) |
| 07:50:35 | → | rembo10 joins (~rembo10@main.remulis.com) |
| 07:50:44 | × | degraafk quits (sid71464@id-71464.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 07:50:44 | × | delyan_ quits (sid523379@id-523379.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 07:50:44 | × | kitaleth quits (23bd17ddc6@sourcehut/user/alethkit) (Ping timeout: 260 seconds) |
| 07:50:44 | × | aniketd quits (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 260 seconds) |
| 07:50:44 | × | caasih quits (sid13241@id-13241.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 07:50:44 | × | bjs quits (sid190364@user/bjs) (Ping timeout: 260 seconds) |
| 07:50:44 | × | jackdk quits (sid373013@cssa/jackdk) (Ping timeout: 260 seconds) |
| 07:51:43 | → | liskin joins (~liskin@xmonad/liskin) |
| 07:51:53 | → | aniketd joins (32aa4844cd@2a03:6000:1812:100::dcb) |
| 07:52:27 | → | edwardk joins (sid47016@haskell/developer/edwardk) |
| 07:52:32 | → | shawwwn joins (sid6132@helmsley.irccloud.com) |
| 07:52:54 | → | jackdk joins (sid373013@cssa/jackdk) |
| 07:53:19 | → | caasih joins (sid13241@id-13241.ilkley.irccloud.com) |
| 07:53:40 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 07:53:52 | → | delyan_ joins (sid523379@id-523379.hampstead.irccloud.com) |
| 07:53:56 | → | degraafk joins (sid71464@id-71464.lymington.irccloud.com) |
| 07:54:38 | → | bjs joins (sid190364@user/bjs) |
| 07:55:11 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 07:55:24 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 07:55:40 | × | [exa] quits (~exa@2001:15e8:110:7d00::117) (Changing host) |
| 07:55:40 | → | [exa] joins (~exa@user/exa/x-3587197) |
| 07:57:48 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 07:58:14 | → | ubert joins (~Thunderbi@2001:871:263:9b13:379:6815:ba4a:300c) |
| 08:00:58 | → | merijn joins (~merijn@77.242.116.146) |
| 08:03:16 | → | kitaleth joins (23bd17ddc6@sourcehut/user/alethkit) |
| 08:06:37 | → | uli-fem joins (~lambdapin@user/uli-fem) |
| 08:07:42 | → | fn_lumi joins (3d621153a5@2a03:6000:1812:100::df7) |
| 08:09:04 | → | Artea joins (~Lufia@vps.artea.ovh) |
| 08:13:08 | → | benjaminl_ joins (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) |
| 08:14:04 | × | benjaminl quits (~benjaminl@user/benjaminl) (Ping timeout: 260 seconds) |
| 08:17:43 | → | gmg joins (~user@user/gehmehgeh) |
| 08:22:16 | × | gmg quits (~user@user/gehmehgeh) (Client Quit) |
| 08:24:12 | × | euleritian quits (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 08:24:29 | → | euleritian joins (~euleritia@77.22.252.56) |
| 08:30:22 | × | mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Quit: mesaoptimizer) |
| 08:30:30 | → | mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet) |
| 08:42:49 | → | gmg joins (~user@user/gehmehgeh) |
| 08:46:32 | × | Luj9 quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 08:47:10 | → | __monty__ joins (~toonn@user/toonn) |
| 08:47:14 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:47:17 | → | Luj9 joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 08:51:53 | → | chele joins (~chele@user/chele) |
| 08:51:58 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 08:52:35 | → | merijn joins (~merijn@77.242.116.146) |
| 08:57:36 | × | Square2 quits (~Square4@user/square) (Ping timeout: 246 seconds) |
| 09:07:00 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 09:11:16 | → | srazkvt joins (~sarah@user/srazkvt) |
| 09:12:11 | → | merijn joins (~merijn@77.242.116.146) |
| 09:18:49 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
| 09:21:19 | → | euleritian joins (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 09:23:45 | × | euleritian quits (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 09:24:02 | → | euleritian joins (~euleritia@77.22.252.56) |
| 09:44:24 | <yin> | SSFFC - Sport System F Football Club |
| 09:45:02 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 09:45:17 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:46:25 | × | ash3en quits (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Ping timeout: 248 seconds) |
| 09:48:36 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 09:59:06 | → | comerijn joins (~merijn@77.242.116.146) |
| 10:01:14 | × | ubert quits (~Thunderbi@2001:871:263:9b13:379:6815:ba4a:300c) (Ping timeout: 272 seconds) |
| 10:01:59 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 10:04:44 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: nyaa~) |
| 10:07:49 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 248 seconds) |
| 10:14:30 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 10:20:44 | → | EarlPitts joins (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) |
| 10:21:15 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 246 seconds) |
| 10:21:40 | → | ubert joins (~Thunderbi@2001:871:263:9b13:239d:e071:1867:e9a4) |
| 10:25:51 | → | merijn joins (~merijn@77.242.116.146) |
| 10:30:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 10:33:21 | → | alexherbo2 joins (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 10:36:58 | → | merijn joins (~merijn@77.242.116.146) |
| 10:38:48 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 10:43:35 | <apache2> | 40 |
| 10:46:08 | <ski> | 65 |
| 10:46:39 | <Rembane> | 90 |
| 10:51:31 | <Maxdamantus> | That's numberwang. |
| 10:54:44 | → | laxmik joins (~laxmik@85-193-3-200.rib.o2.cz) |
| 10:57:21 | × | laxmik quits (~laxmik@85-193-3-200.rib.o2.cz) (Client Quit) |
| 10:57:44 | × | uli-fem quits (~lambdapin@user/uli-fem) (Ping timeout: 252 seconds) |
| 11:04:33 | × | poscat0x04 quits (~poscat@user/poscat) (Quit: Bye) |
| 11:08:51 | → | poscat joins (~poscat@user/poscat) |
| 11:42:53 | × | CrunchyFlakes quits (~CrunchyFl@31.18.102.35) (Quit: ZNC 1.8.2 - https://znc.in) |
| 11:47:00 | → | CrunchyFlakes joins (~CrunchyFl@31.18.102.35) |
| 12:06:36 | × | ubert quits (~Thunderbi@2001:871:263:9b13:239d:e071:1867:e9a4) (Ping timeout: 246 seconds) |
| 12:06:37 | × | alexherbo2 quits (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 12:06:57 | → | alexherbo2 joins (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 12:12:19 | <albet70> | is there a function can get the most matched item from a list, like f [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] == [1,2,3,5]? |
| 12:18:40 | <Leary> | > (find . isSubsequenceOf) [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] |
| 12:18:41 | <lambdabot> | Just [1,2,3,5] |
| 12:18:56 | <mauke> | define "most matched"? |
| 12:20:05 | <albet70> | have the most common elements |
| 12:20:18 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:20:52 | <albet70> | find the sublist within a list of sublists that has the most elements in common with a given list |
| 12:21:26 | <mauke> | are all sublists sorted? |
| 12:21:37 | <albet70> | no |
| 12:22:36 | <Rembane> | It sounds a bit like this problem: https://en.wikipedia.org/wiki/Longest_common_substring |
| 12:22:52 | <mauke> | oh, does the order of elements matter? |
| 12:24:33 | <albet70> | no |
| 12:25:35 | <mauke> | then it might be easiest to just convert everything to sets |
| 12:26:39 | × | solution quits (~Solution@78-131-74-26.pool.digikabel.hu) (Ping timeout: 260 seconds) |
| 12:27:38 | → | ash3en joins (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 12:27:58 | → | solution joins (~Solution@78-131-74-9.pool.digikabel.hu) |
| 12:29:25 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in foo [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] |
| 12:29:26 | <lambdabot> | [1,2,3,5] |
| 12:30:13 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in "celery" (words "the quick brown fox jumps over the lazy dog") |
| 12:30:15 | <lambdabot> | error: |
| 12:30:15 | <lambdabot> | • Couldn't match expected type ‘[String] -> t’ |
| 12:30:15 | <lambdabot> | with actual type ‘[Char]’ |
| 12:30:23 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in foo "celery" (words "the quick brown fox jumps over the lazy dog") |
| 12:30:24 | <lambdabot> | "lazy" |
| 12:39:28 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 12:39:50 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 12:41:03 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 12:43:24 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:57:34 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 12:57:55 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:03:19 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 13:12:27 | → | quack joins (~quack@209.60-130-109.adsl-dyn.isp.belgacom.be) |
| 13:13:55 | → | weary-traveler joins (~user@user/user363627) |
| 13:14:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 13:15:16 | <quack> | Hello, I'm trying to understand better what the exact rules are for evaluating thunks, e.g. consider: |
| 13:15:17 | <quack> | f (0, 1) = 0 |
| 13:15:18 | <quack> | f (x, 2) = 1 |
| 13:15:38 | <quack> | If you then evaluate f (undefined, 2) you get an exception |
| 13:15:51 | <quack> | but if you have: |
| 13:15:53 | <quack> | g (1, 0) = 0 |
| 13:15:54 | <quack> | g (2, x) = 1 |
| 13:16:28 | <quack> | Then g (2, undefined) gives 2, which implies that pattern matching runs from left to right, but I'm not sure if that is accurate? |
| 13:17:25 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 13:21:00 | <EvanR> | > let f (x, 2) = 1 in f (undefined, 2) |
| 13:21:02 | <lambdabot> | 1 |
| 13:21:05 | <EvanR> | no exception |
| 13:21:45 | <EvanR> | you might be thinking of |
| 13:22:02 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 13:22:25 | <EvanR> | > let f (False, False) = 2 in f (error "A", error "B") |
| 13:22:27 | <lambdabot> | *Exception: A |
| 13:22:28 | <ski> | matching `undefied' with `0' doesn't succeed |
| 13:22:32 | <ncf> | > let f (0, 1) = 0; f (x, 2) = 1 in f (undefined, 2) |
| 13:22:34 | <lambdabot> | *Exception: Prelude.undefined |
| 13:22:40 | <ncf> | you need both lines |
| 13:22:49 | <ski> | and yes, matching constructor components from left to right |
| 13:22:53 | <EvanR> | in this case, the error you get is technically arbitrary, not left to right |
| 13:22:54 | × | ash3en quits (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Ping timeout: 246 seconds) |
| 13:23:14 | <quack> | ski: matching left from right is guaranteed? |
| 13:23:22 | <EvanR> | no? |
| 13:23:22 | <quack> | *from left to right |
| 13:23:41 | <EvanR> | in the absence of competing exceptions, you can't tell |
| 13:23:41 | <ncf> | > The matching process itself occurs "top-down, left-to-right." |
| 13:23:43 | <lambdabot> | error: |
| 13:23:43 | <lambdabot> | Data constructor not in scope: |
| 13:23:43 | <lambdabot> | The |
| 13:23:43 | <ncf> | seems like it |
| 13:23:53 | <quack> | > let g (1, 0) = 0; g (2, x) = 1 in g (2, undefined) |
| 13:23:54 | <lambdabot> | 1 |
| 13:24:08 | ← | ncf parts (~n@monade.li) (Fairfarren.) |
| 13:24:09 | <ski> | pretty sure you get the appearance of that. the implementation may decide to do a different order in actuality, if it can show it gives the same result |
| 13:24:12 | → | ncf joins (~n@monade.li) |
| 13:24:17 | <ncf> | ≫ For example, if [1,2] is matched against [0,bot], then 1 fails to match 0, so the result is a failed match. (Recall that bot, defined earlier, is a variable bound to _|_.) But if [1,2] is matched against [bot,0], then matching 1 against bot causes divergence (i.e. _|_). |
| 13:24:21 | <EvanR> | the compiler will rearrange your high level code into something hard to recognize, and it can choose which order to match in as long as the semantics are respected |
| 13:25:00 | <[exa]> | quack: this might be an interesting read, IIRC the order is specified there: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17 |
| 13:25:18 | <dminuoso> | top-to-bottom, left-to-right is indeed a good first approximation of case-of expressions. |
| 13:25:20 | <[exa]> | (section 3.17.2, list item 5, bullet 1) |
| 13:26:02 | <dminuoso> | It of course becomes more complicated since it depends on whether patterns are refutable or not, lazy or not, strictness annotations |
| 13:26:21 | <ncf> | EvanR: this sounds like the exact kind of thing the compiler isn't allowed to do if it changes the semantics |
| 13:26:31 | → | ystael joins (~ystael@user/ystael) |
| 13:26:33 | <ncf> | do you have an example? |
| 13:26:36 | <dminuoso> | (Note that case-of is valid since the haskell report specifies that multiple-function-definitions are equivalent/desugared into case-of |
| 13:26:43 | <EvanR> | ncf, what semantics are being changed? |
| 13:26:52 | <EvanR> | which competing exception wins? |
| 13:26:55 | <EvanR> | that's undefined |
| 13:27:04 | <ncf> | there are no competing exceptions here |
| 13:27:05 | <dminuoso> | ncf: They explicitly said "as long as the semantics are respected" |
| 13:27:05 | × | alexherbo2 quits (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 13:27:22 | <dminuoso> | I mean compilers generally live under the as-if rule. If you cant tell differently, it does not matter. :p |
| 13:27:23 | <ncf> | well changing the order of the pattern matching wouldn't respect the semantics! |
| 13:27:24 | → | alexherbo2 joins (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 13:27:24 | <EvanR> | otherwise you can't observe the order that things are pattern matched in |
| 13:27:32 | <dminuoso> | ncf: depends on whether you can tell or not. |
| 13:27:35 | <ski> | having `True || _ = True; _ || True = True; _ || _ = False' give you both `True || undefined' and `undefined || True' evaluating to `True' is called "parallel OR", is a common non-sequential example in denotational semantics |
| 13:28:21 | <quack> | [exa]: thanks, I missed that on my first skim |
| 13:29:09 | <EvanR> | other than exceptions, the only reason you want to "know" the order (as if the code you wrote is literally being executed as written), is to game the performance. But that seems hard for a complex pattern |
| 13:29:19 | <EvanR> | the answers come out the same |
| 13:29:48 | → | zmt01 joins (~zmt00@user/zmt00) |
| 13:29:53 | <dminuoso> | EvanR: Not necessarily, given infinite data structures it may be necessary to understand evaluation order. |
| 13:30:06 | <quack> | EvanR: it's not for performance but to know whether evaluation will throw an exception. Right now f throws and g succeeds, but if the order were right to left then f would succeed and g throw |
| 13:30:09 | <dminuoso> | Especially with recursive structure. |
| 13:30:36 | × | EarlPitts quits (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) (Remote host closed the connection) |
| 13:30:48 | <ski> | (or TyingTheKnot) |
| 13:30:57 | → | EarlPitts joins (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) |
| 13:31:12 | <EvanR> | how do you have an infinite pattern |
| 13:31:39 | <EvanR> | quack, yes so back to your original question, you were mistaken about f throwing an exception at all |
| 13:31:45 | <EvanR> | it doesn't |
| 13:32:02 | <quack> | It does? ncf showed it |
| 13:32:03 | <quack> | > let f (0, 1) = 0; f (x, 2) = 1 in f (undefined, 2) |
| 13:32:05 | <lambdabot> | *Exception: Prelude.undefined |
| 13:32:14 | <EvanR> | oh |
| 13:32:23 | <EvanR> | yes the first definition will be pattern matched first, that's true |
| 13:32:29 | <ncf> | ...yes |
| 13:32:42 | <EvanR> | I was arguing about whether x or 2 is matched first |
| 13:32:49 | <ski> | (strictly speaking, the argument `undefined' is to be blamed for throwing, not `f' itself) |
| 13:33:24 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 276 seconds) |
| 13:33:55 | <ski> | (Racket has a blame-tracking system, with contracts, to determine who's to blame, especially re higher-order procedures (so accepting callbacks), when a contract is broken) |
| 13:37:52 | <fr33domlover> | o/ I defined a type named Schema, and now I'd like to write a typeclass @Message@, where for a given @m@ there's a type family @FromSchema (s :: Schema) :: m@ and a type family @ToSchema (x :: m) :: (Maybe Schema)@ |
| 13:38:17 | <fr33domlover> | How do I do that? It seems like I need type-level type-families, which don't exist (yet)? |
| 13:39:34 | × | quack quits (~quack@209.60-130-109.adsl-dyn.isp.belgacom.be) (Quit: Client closed) |
| 13:40:32 | <EvanR> | fromSchema :: Schema -> m, toSchema :: m -> Maybe Schema, as methods on the type class? |
| 13:41:17 | <fr33domlover> | But that's value level :) I have an idea for a workaround /me tries in GHCi 1 sec |
| 13:45:07 | → | ubert joins (~Thunderbi@2001:871:263:9b13:c5fe:c84e:4781:2c20) |
| 13:46:23 | <fr33domlover> | Here's code and error from GHC: http://paste.debian.net/1328521/ |
| 13:46:43 | <fr33domlover> | Workaround is failing :p |
| 13:47:44 | × | benjaminl_ quits (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) (Ping timeout: 260 seconds) |
| 13:48:54 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 13:48:55 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 13:49:37 | <EvanR> | type Msg c just by itself with no annotation or definition? |
| 13:50:40 | <ski> | fr33domlover : wondering whether breaking into a super- and sub- class would help |
| 13:58:24 | <fr33domlover> | ski: It helped but there's a new error http://paste.debian.net/1328524/ |
| 13:58:30 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 14:00:08 | <fr33domlover> | I tried adding (Msg X ~ Msgx) as a constraint to the instance, but got same errors |
| 14:05:02 | <ski> | fr33domlover : tried injectivity on `Msg' ? |
| 14:06:05 | <ski> | (dunno if it's what it's complaining about, but it's what i could think to try) |
| 14:12:00 | <fr33domlover> | Yes, it didn't help. But I just tried moving the FromPat case-handling into an external type family and the code builds now ^_^ |
| 14:17:12 | × | alexherbo2 quits (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 14:17:28 | <fr33domlover> | It's sooo weird, moving just FromPat is enough for GHCi to accept the code; but if FromPat and ToPat are in different typeclasses, they both need to use helper standalone families |
| 14:17:39 | <fr33domlover> | Oh well at least I found a way to make it work |
| 14:18:23 | → | alexherbo2 joins (~alexherbo@2a02-8440-321a-7a79-241e-13ab-7d87-53f9.rev.sfr.net) |
| 14:18:57 | → | lol_ joins (~lol@2603:3016:1e01:b960:4840:2ad9:7736:e7f5) |
| 14:21:51 | × | alexherbo2 quits (~alexherbo@2a02-8440-321a-7a79-241e-13ab-7d87-53f9.rev.sfr.net) (Remote host closed the connection) |
| 14:22:54 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b960:f4ac:a003:2d11:ead1) (Ping timeout: 260 seconds) |
| 14:22:56 | → | ash3en joins (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 14:30:56 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 14:32:39 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:36:22 | lol_ | is now known as jcarpenter2 |
| 14:40:28 | → | athan joins (~athan@2600:382:2d15:de3c:7342:aa0b:1e24:3f2d) |
| 14:42:18 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 14:45:04 | <haskellbridge> | <thirdofmay18081814goya> "data NatOrBool = Nat | Bool" |
| 14:45:25 | <haskellbridge> | <thirdofmay18081814goya> system F can't model this, wasn't a model able to model this? |
| 14:45:35 | <haskellbridge> | <thirdofmay18081814goya> what's a model able to model this* |
| 14:47:14 | <ski> | presumably you're looking for some kind of subtyping |
| 14:52:38 | × | ubert quits (~Thunderbi@2001:871:263:9b13:c5fe:c84e:4781:2c20) (Quit: ubert) |
| 14:56:00 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 246 seconds) |
| 14:57:56 | <tomsmeding> | typescript has union types |
| 14:58:06 | <tomsmeding> | python also does |
| 14:58:14 | <tomsmeding> | to the extent that python "has types" |
| 15:00:50 | <dminuoso> | tomsmeding: The one part that always makes me smile, is that python has "types" but comes with no type checker. |
| 15:01:15 | <tomsmeding> | and multiple exist, and they are incompatible :) |
| 15:01:34 | <dminuoso> | tomsmeding: At least that makes then true syntactic constructs in the sense of TaPL! |
| 15:04:30 | <EvanR> | thirdofmay: an enum type? |
| 15:05:48 | → | comerijn joins (~merijn@77.242.116.146) |
| 15:07:25 | <tomsmeding> | fr33domlover: odd, it works if Msg is a closed type family but not if it's an open one (and an associated type family is always open) |
| 15:08:06 | <tomsmeding> | https://play.haskell.org/saved/pSxMC6lR |
| 15:08:15 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 15:09:10 | × | EarlPitts quits (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) (Remote host closed the connection) |
| 15:09:24 | <tomsmeding> | _wat_ |
| 15:09:38 | <tomsmeding> | ok this is a ghc bug |
| 15:09:56 | <EvanR> | vlad_, I swear by this, https://www.haskell.org/tutorial/ |
| 15:10:50 | → | mikess joins (~mikess@user/mikess) |
| 15:11:12 | <tomsmeding> | fr33domlover: https://play.haskell.org/saved/ruULajDX |
| 15:11:15 | <weary-traveler> | when multiple exist, they're usually not compatible. see also erlang type checkers |
| 15:12:28 | <haskellbridge> | <thirdofmay18081814goya> hm typescript and python have them but they're really different to system F and derivatives |
| 15:12:54 | <haskellbridge> | <thirdofmay18081814goya> I'm looking for something that could approximate the behaviour of "data NatOrBool = Nat | Bool" in haskell |
| 15:13:01 | <haskellbridge> | <thirdofmay18081814goya> formally |
| 15:13:08 | <EvanR> | that is just an enum type |
| 15:13:18 | <EvanR> | equivalent to data Bool = True | False |
| 15:13:33 | <EvanR> | which you can emulate using church encoding |
| 15:13:50 | <[exa]> | I think it was more of `type NatOrBool = Bool | Nat` with some magickal | |
| 15:14:11 | <haskellbridge> | <thirdofmay18081814goya> EvanR: wow i had totally misunderstood how that worked in haskell |
| 15:14:17 | <haskellbridge> | <thirdofmay18081814goya> right ok, ty |
| 15:14:18 | <EvanR> | \o/ |
| 15:14:47 | <glguy> | tomsmeding: (yes, it's still a bug) You can define type Id a = a; and then Id (Msg X) works |
| 15:15:39 | <tomsmeding> | glguy: where precisely? |
| 15:15:49 | <tomsmeding> | my latest reduction is https://play.haskell.org/saved/VibtX2ah |
| 15:16:10 | <tomsmeding> | surely the _location_ of the definition of X should not matter? |
| 15:16:17 | <tomsmeding> | there's no TH here |
| 15:17:39 | <glguy> | tomsmeding: Id (Msg X) in the type ascription - seemed to trick GHC into evaluating the expression |
| 15:17:47 | <glguy> | yeah, location shouldn't matter |
| 15:18:09 | × | Axman3650 quits (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 15:18:24 | <tomsmeding> | oh I see |
| 15:18:39 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:18:44 | <tomsmeding> | glguy: do you happen to know if there's already an open issue about this? |
| 15:19:10 | <glguy> | I don't |
| 15:20:38 | <fr33domlover> | Feels like the boundaries where normal rules of physics cease to exist... :p |
| 15:20:43 | × | srazkvt quits (~sarah@user/srazkvt) (Remote host closed the connection) |
| 15:21:02 | → | srazkvt joins (~sarah@user/srazkvt) |
| 15:22:36 | → | Axman6 joins (~Axman6@user/axman6) |
| 15:23:34 | <tomsmeding> | fr33domlover: mind if I mention your IRC nick in the GHC issue? |
| 15:27:13 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 15:27:29 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 15:28:55 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 15:29:03 | <fr33domlover> | tomsmeding: Go ahead (and of course feel free to paste my code too! So that if anyone has questions it will remind me what I was trying to do :P) |
| 15:29:15 | <tomsmeding> | I did change some of the names |
| 15:29:21 | <tomsmeding> | (in the code) |
| 15:30:38 | <fr33domlover> | Cool. Soon I'll probably have the actual working code with more meaningful names (I'm implementing a type-level schema for parsing and encoding Preserves, a data model a bit like json/protobuf/etc. https://preserves.dev/ |
| 15:30:39 | → | merijn joins (~merijn@77.242.116.146) |
| 15:33:04 | <tomsmeding> | fr33domlover glguy: https://gitlab.haskell.org/ghc/ghc/-/issues/25238 |
| 15:34:08 | <vlad_> | ooh :help works in ghci |
| 15:34:27 | <tomsmeding> | vlad_: https://downloads.haskell.org/ghc/latest/docs/users_guide/ghci.html#ghci-commands :p |
| 15:35:40 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 15:36:28 | <vlad_> | how do i examine a variable? |
| 15:36:37 | <tomsmeding> | examine in what way? |
| 15:36:42 | <vlad_> | like its type |
| 15:36:45 | <tomsmeding> | :t |
| 15:36:48 | <tomsmeding> | :t print |
| 15:36:49 | <lambdabot> | Show a => a -> IO () |
| 15:37:26 | <tomsmeding> | vlad_: there is also :i, which shows more info |
| 15:37:49 | <tomsmeding> | (but :i works on individual names only, while :t takes an expression) |
| 15:39:06 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 15:40:55 | → | Guest38 joins (~Guest38@194.183.191.121) |
| 15:41:37 | × | Guest38 quits (~Guest38@194.183.191.121) (Client Quit) |
| 15:46:22 | × | rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 15:53:11 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 15:53:24 | × | nadja quits (~dequbed@banana-new.kilobyte22.de) (Quit: bye!) |
| 15:55:53 | <EvanR> | information on an arbitrary expression would be interesting ngl |
| 15:58:33 | → | nadja joins (~dequbed@banana-new.kilobyte22.de) |
| 16:00:44 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 16:00:58 | × | son0p quits (~ff@191.104.26.195) (Ping timeout: 252 seconds) |
| 16:04:08 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 16:05:02 | <tomsmeding> | EvanR: what kind of info would you like :p |
| 16:05:19 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 16:06:53 | <EvanR> | the structure diagram with highlighted pieces showing the type or something |
| 16:09:01 | → | Square joins (~Square@user/square) |
| 16:10:18 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 16:18:27 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 16:18:49 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 16:19:06 | → | ft joins (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 16:21:53 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:22:03 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:22:53 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 16:28:28 | → | misterfish joins (~misterfis@84.53.85.146) |
| 16:28:40 | → | srazkvt joins (~sarah@user/srazkvt) |
| 16:29:17 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 16:35:26 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 16:39:53 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 16:44:58 | × | alanz quits (sid110616@uxbridge.irccloud.com) (Ping timeout: 252 seconds) |
| 16:48:45 | → | alanz joins (sid110616@id-110616.uxbridge.irccloud.com) |
| 16:58:10 | × | NemesisD quits (sid24071@lymington.irccloud.com) (Ping timeout: 252 seconds) |
| 16:59:16 | × | SrPx quits (sid108780@uxbridge.irccloud.com) (Ping timeout: 252 seconds) |
| 17:00:29 | → | NemesisD joins (sid24071@id-24071.lymington.irccloud.com) |
| 17:02:34 | × | Pent quits (sid313808@lymington.irccloud.com) (Ping timeout: 252 seconds) |
| 17:02:38 | → | SrPx joins (sid108780@id-108780.uxbridge.irccloud.com) |
| 17:02:56 | <haskellbridge> | <thirdofmay18081814goya> woah we have explicit big lambda in ghc 9.10 now |
| 17:02:58 | <haskellbridge> | <thirdofmay18081814goya> neato |
| 17:03:24 | <haskellbridge> | <thirdofmay18081814goya> TypeAbstractions |
| 17:05:13 | → | Pent joins (sid313808@id-313808.lymington.irccloud.com) |
| 17:05:49 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 17:05:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:09:21 | × | vglfr quits (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 246 seconds) |
| 17:09:32 | → | vglfr joins (~vglfr@2607:fb91:1420:4418:ac39:6af1:e1c8:8bec) |
| 17:10:16 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 252 seconds) |
| 17:12:26 | <haskellbridge> | <thirdofmay18081814goya> what are some possible semantics for typeclasses? |
| 17:13:48 | <ncf> | do you mean instance search? typeclasses themselves are just record types (cf dictionary passing implementations) |
| 17:14:27 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 17:14:31 | → | oo_miguel1 joins (~Thunderbi@78.10.207.45) |
| 17:14:39 | <justsomeguy> | What is the purpose of the Reader monad? Why not just use a closure? |
| 17:15:04 | <haskellbridge> | <thirdofmay18081814goya> ncf: will look these up, thank you! |
| 17:15:42 | <haskellbridge> | <thirdofmay18081814goya> by instance search do you mean typeclass inference? |
| 17:15:44 | <ncf> | justsomeguy: closures are implementation details that are mostly irrelevant to haskell. do you mean what's the point of the Reader newtype as opposed to just using the native ((->) r) instance? |
| 17:16:04 | <ncf> | goya: yes, sorry, that's what Agda calls it |
| 17:16:17 | <justsomeguy> | I mean, conceptually, what problem is the reader monad intended to solve? |
| 17:16:18 | <ncf> | (and it's a better name IMO) |
| 17:16:29 | × | oo_miguel quits (~Thunderbi@78.10.207.45) (Ping timeout: 255 seconds) |
| 17:16:29 | oo_miguel1 | is now known as oo_miguel |
| 17:16:41 | <ncf> | justsomeguy: repeatedly applying functions to global arguments |
| 17:16:47 | → | poscat joins (~poscat@user/poscat) |
| 17:16:49 | <haskellbridge> | <thirdofmay18081814goya> ncf: ty! |
| 17:17:23 | <ncf> | try to implement a basic type checker and when you're done you should wish you had a reader monad to stuff your environment into |
| 17:17:58 | <EvanR> | reader monad = passing the environment around to anything that needs it, only it's implicit so you don't have to |
| 17:18:06 | <EvanR> | while also being type safe |
| 17:18:22 | <EvanR> | that being said you might just want to pass the environment around anyway |
| 17:18:52 | <EvanR> | also the asks function is pretty nifty |
| 17:18:53 | <EvanR> | :t asks |
| 17:18:55 | <lambdabot> | MonadReader r m => (r -> a) -> m a |
| 17:19:17 | <ncf> | :t local |
| 17:19:18 | <lambdabot> | MonadReader r m => (r -> r) -> m a -> m a |
| 17:20:00 | <EvanR> | also cool |
| 17:20:23 | <ncf> | local is a very useful abstraction that lets you say "run this part of the computation in a modified context". for example, if your typechecker encounters something like λx.e, you'll probably want to go on typechecking e in an extended context where x is a bound variable |
| 17:21:07 | <monochrom> | I wrote my type checker with the reader monad. Then I wished I just used "Env ->". |
| 17:21:17 | <ncf> | eh, that's a reader monad :p |
| 17:21:24 | <ncf> | just not the Reader monad |
| 17:21:27 | <EvanR> | just pass the environment around |
| 17:21:53 | <monochrom> | But it also means I don't bother with "local" and the other method I forgot the name of. |
| 17:23:00 | <justsomeguy> | So when does the record (environment) get defined? As part of the instance declaration? |
| 17:23:20 | <monochrom> | I'm bivalent about this. I have done both ways. Each way has something to like and something to dislike. At the end, I wish something else writes the code for me. :) |
| 17:24:57 | <ncf> | justsomeguy: yeah, `class Foo where` is basically `data Foo = ...` and `instance Foo where` is basically `foo :: Foo; foo = ...` |
| 17:25:22 | <monochrom> | I recognize that if I'm writing "infer env foo" five times in a row, then Reader[T] reduces that repetition of "env". |
| 17:26:50 | <monochrom> | But "env <- ask; local (f env) (infer bar)" is noisier than "infer (f env) bar" |
| 17:27:36 | <EvanR> | justsomeguy, it is passed in to runReader |
| 17:27:36 | <ncf> | i mean in a serious typechecker you'd have a whole stack of effects and "accessing and updating the environment" would only be one of them. so then the question becomes "why do you use reader for that instead of state or something else" |
| 17:27:42 | <EvanR> | :t runReader |
| 17:27:42 | <mauke> | did you mean: local f (infer bar) |
| 17:27:43 | <lambdabot> | Reader r a -> r -> a |
| 17:28:07 | <monochrom> | Ah yeah, local f (infer bar) |
| 17:28:08 | <ncf> | EvanR: wrong conversation |
| 17:28:24 | <EvanR> | huh |
| 17:28:26 | <ncf> | oh wait no it's me who am confused |
| 17:31:01 | <monochrom> | I actually teach my answer to that, albeit for an interpreter (or semantic model) rather than a checker. https://www.cs.utoronto.ca/~trebla/CSCC24-2024-Summer/10-semantics-2.html#model |
| 17:33:01 | <justsomeguy> | Sometimes I feel like these abstractions are just obstacles in my way, instead of a useful tool to address a problem. |
| 17:33:19 | <monochrom> | I used to have a longer, much expanded version of that, completely fleshed out with "lets make it all state" and coded up, to show what would go wrong, or at least hard to fix and error-prone. But eventually, "in the interest of saving time", I deleted it. |
| 17:33:39 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 17:34:21 | <ncf> | justsomeguy: if you feel like that, then probably don't use them |
| 17:35:14 | × | vglfr quits (~vglfr@2607:fb91:1420:4418:ac39:6af1:e1c8:8bec) (Ping timeout: 260 seconds) |
| 17:35:29 | <EvanR> | justsomeguy, don't fall into the trap of seeing a feature that exists, and assuming you have to use to for something, or go looking for some reason to use it |
| 17:35:32 | → | vglfr joins (~vglfr@2607:fb90:eaac:5d4:ad3:f757:81b5:4809) |
| 17:35:38 | <EvanR> | use it* |
| 17:36:00 | <EvanR> | wait until a good reason to use it comes up (if ever) |
| 17:36:54 | <EvanR> | Reader's scope is so narrow it's easy to judge if you need it |
| 17:36:54 | <justsomeguy> | For context, I'm going through a book in order, and this is the next chapter. I think if I wasn't commited to finishing this thing I probably wouldn't come across Reader until I had a good use case for it. |
| 17:37:40 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 17:37:49 | <EvanR> | ok then finish the chapter and return to reasonable afterward |
| 17:38:09 | × | Square quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 17:38:26 | <justsomeguy> | :D |
| 17:38:54 | justsomeguy | has a little post-it note on his mirror that says "Finsih HPFP before you dit" |
| 17:39:02 | <justsomeguy> | *die |
| 17:40:49 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 17:40:57 | <int-e> | tomsmeding: re: #25238 ...the difference appears to be that the later `data X` pulls the FromPat and Msg type families into the same group, and that causes the Msg X = MsgDef type instance to be added to the environment (addLocalFamInst) much later, *after* `Msg X` has been subjected to its first simplification. And it looks like that is never retried. That doesn't explain why `Id (Msg X)` works... |
| 17:41:03 | <int-e> | ...of course. But at least it's an observable difference in --ddump-tc-trace. |
| 17:42:17 | <tomsmeding> | int-e: interesting! |
| 17:42:24 | <tomsmeding> | I know very little about how the type checker actually works :) |
| 17:42:42 | <tomsmeding> | I just found it funny that apparently this issue has existed since at least 8.4 |
| 17:43:07 | <tomsmeding> | it does explain how ordering gets into the problem, though |
| 17:43:27 | <tomsmeding> | int-e: though that does beg the question: why are these "groups" a thing in the first place? |
| 17:44:04 | <tomsmeding> | I know that mutually recursive groups have to be handled specially in the case of functions (I recall that from the haskell report), and I expect the same holds for type families, for analogous reasons |
| 17:44:21 | <tomsmeding> | but whether things are mutually recursive has little to do with whether they are lexically adjacent in the source file |
| 17:45:03 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 17:45:59 | <int-e> | I'd guess that adding instances early makes simplification more efficient. But I don't know. I suspect I don't know more about the type checker than you do. Something constraint handling rules something. It has also changed a lot over time. |
| 17:46:58 | <tomsmeding> | but then why not add everything early? :p |
| 17:47:16 | <int-e> | because it might fail to typecheck |
| 17:47:53 | <tomsmeding> | and it's less efficient to through everything in one group to be typechecked simultaneously? |
| 17:47:57 | <tomsmeding> | *to throw |
| 17:52:56 | <int-e> | It's a guess; I don't know. Rewriting feels cheaper than tracking additional constraints. |
| 17:54:32 | <int-e> | The reference to "addLocalFamInst" above is there not because I looked at any code but because it's a label that comes up in the type-checker trace. (I did look at code but I can't say that I understood any of it :P) |
| 17:54:41 | <tomsmeding> | :) |
| 17:57:46 | × | Fijxu quits (~Fijxu@user/fijxu) (Quit: XD!!) |
| 17:57:47 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 18:01:45 | → | Fijxu joins (~Fijxu@user/fijxu) |
| 18:02:03 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 18:02:30 | <dmj`> | tomsmeding: the HM(x) paper is a good place to start |
| 18:03:11 | <dmj`> | this sdiehl implementation is a good micro implementation of HM(x), HM w/o any extensions. https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs |
| 18:03:32 | <dmj`> | but once you add type classes it just explodes in complexity |
| 18:04:24 | <tomsmeding> | dmj`: is that the same as "OutsideIn(X)", that I vaguely recall hearing of? |
| 18:04:42 | <tomsmeding> | ah seems to be different |
| 18:06:04 | <tomsmeding> | apparently OutsideIn(X) is an extension of HM(X?) |
| 18:06:24 | × | athan quits (~athan@2600:382:2d15:de3c:7342:aa0b:1e24:3f2d) (Ping timeout: 276 seconds) |
| 18:06:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:07:46 | <dmj`> | tomsmeding: yea, OutsideIn(x) is how they refactored the type checker to be a constraint solver, like HM(x), but why they had to sacrifice let generalization to do so |
| 18:08:04 | <tomsmeding> | HM(X) is not from the GHC people? |
| 18:08:08 | <dmj`> | HM(x) is just a general framework for doing type checking as constraint solving |
| 18:08:44 | <dmj`> | tomsmeding: I don't think so, I think its Remy and Pottier (could be wrong), but its the "French approach", because they are two french guys |
| 18:08:47 | <tomsmeding> | I should read that OutsideIn(x) paper at some point |
| 18:08:50 | <tomsmeding> | ah I see |
| 18:10:02 | <dmj`> | yea I'm trying to figure out how to recover the entailment property when doing type inference w/ classes using the HM(x) approach |
| 18:10:34 | → | son0p joins (~ff@186.121.49.191) |
| 18:11:00 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 18:11:45 | <mauke> | https://www.krook.dev/papers/partitioningHaskell2024.pdf - disappointed that the second co-author's name is Hammersberg, not Hooke |
| 18:12:31 | → | rvalue- joins (~rvalue@user/rvalue) |
| 18:13:08 | <mauke> | then I could say it is a paper by Hooke and by Krook |
| 18:13:21 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 265 seconds) |
| 18:15:39 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 18:16:36 | rvalue- | is now known as rvalue |
| 18:17:04 | <monochrom> | heh |
| 18:22:23 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:23:36 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 18:26:28 | × | Fijxu quits (~Fijxu@user/fijxu) (Quit: XD!!) |
| 18:26:30 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 18:28:02 | → | CiaoSen joins (~Jura@2a05:5800:2e8:9e00:ca4b:d6ff:fec1:99da) |
| 18:30:57 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 18:34:22 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 18:40:51 | × | gawen quits (~gawen@user/gawen) (Quit: cya) |
| 18:42:13 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 18:42:14 | → | gawen joins (~gawen@user/gawen) |
| 18:44:11 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:47:04 | × | ash3en quits (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 18:52:50 | → | CAT_S joins (~apic@ppp-46-244-252-175.dynamic.mnet-online.de) |
| 18:53:34 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 18:58:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 18:58:24 | × | vglfr quits (~vglfr@2607:fb90:eaac:5d4:ad3:f757:81b5:4809) (Ping timeout: 276 seconds) |
| 18:58:27 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 18:58:48 | → | vglfr joins (~vglfr@2601:14d:4e01:1370:71d6:bfd8:becf:12cb) |
| 19:01:30 | → | Square2 joins (~Square4@user/square) |
| 19:02:41 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 19:02:51 | → | Square joins (~Square@user/square) |
| 19:05:22 | × | gawen quits (~gawen@user/gawen) (Read error: error:0A000119:SSL routines::decryption failed or bad record mac) |
| 19:06:15 | × | Square2 quits (~Square4@user/square) (Ping timeout: 246 seconds) |
| 19:07:36 | → | gawen joins (~gawen@user/gawen) |
| 19:11:19 | → | RedFlamingos joins (~RedFlamin@user/RedFlamingos) |
| 19:15:10 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 19:18:11 | → | Fijxu joins (~Fijxu@user/fijxu) |
| 19:19:41 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 19:25:25 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:26:33 | × | CAT_S quits (~apic@ppp-46-244-252-175.dynamic.mnet-online.de) (Ping timeout: 246 seconds) |
| 19:32:48 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 19:34:06 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 19:37:15 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 19:39:42 | → | hugo joins (~hugo@quicksilver.lysator.liu.se) |
| 19:39:45 | → | CAT_S joins (~apic@ppp-46-244-252-202.dynamic.mnet-online.de) |
| 19:43:14 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 19:45:00 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 19:46:40 | × | hugo quits (~hugo@quicksilver.lysator.liu.se) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 19:48:46 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 19:51:21 | → | gmg joins (~user@user/gehmehgeh) |
| 19:56:16 | → | srazkvt joins (~sarah@user/srazkvt) |
| 20:00:16 | → | athan joins (~athan@2600:382:3a29:3ae2:2541:beb:5d67:8d9c) |
| 20:02:10 | → | ash3en joins (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 20:03:35 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 20:04:34 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
| 20:06:05 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 20:06:20 | → | euleritian joins (~euleritia@dynamic-176-006-132-001.176.6.pool.telefonica.de) |
| 20:10:41 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 20:18:15 | → | weary-traveler joins (~user@user/user363627) |
| 20:20:57 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 20:23:43 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 20:23:58 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 20:25:12 | → | christiaanb joins (uid84827@id-84827.lymington.irccloud.com) |
| 20:28:15 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 20:38:52 | × | ash3en quits (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 20:39:14 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 20:40:18 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 20:44:41 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 20:55:38 | × | Inst quits (~Inst@user/Inst) (Remote host closed the connection) |
| 20:56:17 | → | Inst joins (~Inst@user/Inst) |
| 21:05:15 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 246 seconds) |
| 21:05:48 | × | CiaoSen quits (~Jura@2a05:5800:2e8:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 245 seconds) |
| 21:07:06 | × | itaipu quits (~itaipu@168.121.99.142) (Ping timeout: 276 seconds) |
| 21:13:29 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 21:18:07 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 21:19:14 | × | michalz quits (~michalz@185.246.207.205) (Remote host closed the connection) |
| 21:21:04 | → | itaipu joins (~itaipu@168.121.99.143) |
| 21:26:09 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds) |
| 21:28:59 | → | WarmHeart joins (~WarmHeart@2605:6440:300a:5001:4a94:d13c:dbb0:ec9b) |
| 21:30:55 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 21:31:25 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:35:07 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 21:36:28 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 21:36:38 | → | Square2 joins (~Square4@user/square) |
| 21:38:40 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:39:12 | × | Square quits (~Square@user/square) (Ping timeout: 246 seconds) |
| 21:40:23 | × | CAT_S quits (~apic@ppp-46-244-252-202.dynamic.mnet-online.de) (Ping timeout: 245 seconds) |
| 21:42:13 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 21:43:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 21:45:54 | × | WarmHeart quits (~WarmHeart@2605:6440:300a:5001:4a94:d13c:dbb0:ec9b) (Quit: Client closed) |
| 21:47:49 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 21:47:49 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Ping timeout: 260 seconds) |
| 21:48:24 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 21:52:41 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 21:54:27 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:55:22 | <haskellbridge> | <eldritchcookie> wow Linear types error messages suck, please point where i use more than once orif it is'nt used. |
| 21:59:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 22:00:12 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 22:00:23 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:01:14 | × | oo_miguel quits (~Thunderbi@78.10.207.45) (Ping timeout: 260 seconds) |
| 22:02:24 | × | athan quits (~athan@2600:382:3a29:3ae2:2541:beb:5d67:8d9c) (Ping timeout: 260 seconds) |
| 22:05:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:08:26 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 22:10:45 | × | Yumemi quits (~Yumemi@2001:bc8:47a0:1b14::1) (Quit: .) |
| 22:10:49 | × | yahb2 quits (~yahb2@user/tomsmeding/bot/yahb2) (Ping timeout: 245 seconds) |
| 22:11:05 | → | Yumemi joins (~Yumemi@chamoin.net) |
| 22:11:58 | × | piele quits (~piele@tbonesteak.creativeserver.net) (Remote host closed the connection) |
| 22:13:11 | → | piele joins (~piele@tbonesteak.creativeserver.net) |
| 22:16:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:16:20 | → | yahb2 joins (~yahb2@user/tomsmeding/bot/yahb2) |
| 22:16:20 | ChanServ | sets mode +v yahb2 |
| 22:18:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:18:53 | × | krei-se quits (~krei-se@p57af29f0.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 22:18:53 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 22:21:08 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 22:21:23 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 22:22:52 | → | pavonia joins (~user@user/siracusa) |
| 22:23:17 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 22:24:24 | × | mikess quits (~mikess@user/mikess) (Quit: mikess) |
| 22:31:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:33:28 | × | Fischmiep quits (~Fischmiep@user/Fischmiep) (Remote host closed the connection) |
| 22:33:52 | → | Fischmiep joins (~Fischmiep@user/Fischmiep) |
| 22:34:46 | × | christiaanb quits (uid84827@id-84827.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:36:38 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 22:36:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 22:40:51 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 22:41:21 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 22:47:40 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:49:42 | × | euleritian quits (~euleritia@dynamic-176-006-132-001.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 22:49:59 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 22:50:46 | → | krei-se joins (~krei-se@p57af29f0.dip0.t-ipconnect.de) |
| 22:52:15 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 22:52:28 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 22:56:43 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 22:59:24 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:03:27 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:08:08 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:08:33 | → | uli-fem joins (~uli-fem@120.18.170.208) |
| 23:09:09 | × | uli-fem quits (~uli-fem@120.18.170.208) (Changing host) |
| 23:09:09 | → | uli-fem joins (~uli-fem@user/uli-fem) |
| 23:12:12 | → | mml joins (~mml@157-131-53-74.fiber.dynamic.sonic.net) |
| 23:19:14 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:20:43 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 23:23:51 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 23:31:05 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 23:35:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:38:18 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb86616a3f2ff56a8996.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 23:39:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 23:42:57 | → | EarlPitts joins (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 23:47:09 | × | EarlPitts quits (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 23:47:56 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 23:49:03 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 23:50:47 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:55:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 23:58:54 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
All times are in UTC on 2024-09-05.