2025/06/04

Newest at the top

2025-06-04 13:58:20 +0200Taneb(~Taneb@runciman.hacksoc.org) (Client Quit)
2025-06-04 13:56:51 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:56:29 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:53:43 +0200Taneb(~Taneb@runciman.hacksoc.org) Taneb
2025-06-04 13:52:37 +0200fp(~Thunderbi@wireless-86-50-140-9.open.aalto.fi) fp
2025-06-04 13:51:55 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:51:32 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-06-04 13:50:13 +0200fp(~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 248 seconds)
2025-06-04 13:49:58 +0200Lycurgus(~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org))
2025-06-04 13:47:10 +0200entangledprime(~entangled@176.223.172.171) (Ping timeout: 252 seconds)
2025-06-04 13:46:51 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:46:26 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:39:27 +0200laurapigeon(~laurapige@user/laurapigeon) laurapigeon
2025-06-04 13:38:47 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:38:20 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-06-04 13:33:38 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds)
2025-06-04 13:31:27 +0200tromp(~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-06-04 13:29:38 +0200humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
2025-06-04 13:29:29 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:29:16 +0200Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal)
2025-06-04 13:29:04 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:27:42 +0200bionade24(~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!)
2025-06-04 13:21:53 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:21:28 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:20:43 +0200tromp(~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798)
2025-06-04 13:17:34 +0200tromp(~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-06-04 13:15:41 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:15:18 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:14:17 +0200GoldsteinQ(~goldstein@goldstein.rs)
2025-06-04 13:13:51 +0200GoldsteinQ(~goldstein@goldstein.rs) (Quit: ZNC 1.8.2 - https://znc.in)
2025-06-04 13:12:19 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
2025-06-04 13:09:29 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2025-06-04 13:08:31 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:08:07 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:06:35 +0200 <Square2> Leary, sweet
2025-06-04 13:06:03 +0200GoldsteinQ(~goldstein@goldstein.rs)
2025-06-04 13:05:38 +0200GoldsteinQ(~goldstein@goldstein.rs) (Quit: ZNC 1.8.2 - https://znc.in)
2025-06-04 13:05:24 +0200 <Leary> Square2: If you impose `Generic a`, you can write a type family taking `Rep a` mapping sums to `Unsatisfiable` and all else to the empty constraint `()`.
2025-06-04 13:05:16 +0200trickard(~trickard@cpe-57-98-47-163.wireline.com.au)
2025-06-04 13:04:55 +0200trickard(~trickard@cpe-57-98-47-163.wireline.com.au) (Ping timeout: 260 seconds)
2025-06-04 13:04:38 +0200 <Square2> Really I only want to accept*
2025-06-04 13:04:13 +0200 <Square2> ski, that would be (a) then. Really I to accept only data types on the form "data Foo = FooConst" (name of type and constructor not important)
2025-06-04 13:03:15 +0200tromp(~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798)
2025-06-04 13:02:29 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-04 13:02:16 +0200 <ski> do you mean (a) a constraint expressing that the constrained type (is a data type and) has only one data constructor; or (b) ensuring that some parameter of a data type will have some particular constraint; or (c) perhaps something else ?
2025-06-04 13:02:05 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-04 13:01:51 +0200jespada(~jespada@r179-25-2-231.dialup.adsl.anteldata.net.uy) jespada
2025-06-04 12:59:39 +0200 <ski> what type constraint ?
2025-06-04 12:57:49 +0200merijn(~merijn@77.242.116.146) merijn
2025-06-04 12:56:51 +0200 <Square2> Another question, I tried to google and chatgpt. Can I express a type constraint on a data type such that it only has one constructor?