Newest at the top
2025-06-04 13:58:20 +0200 | Taneb | (~Taneb@runciman.hacksoc.org) (Client Quit) |
2025-06-04 13:56:51 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:56:29 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:53:43 +0200 | Taneb | (~Taneb@runciman.hacksoc.org) Taneb |
2025-06-04 13:52:37 +0200 | fp | (~Thunderbi@wireless-86-50-140-9.open.aalto.fi) fp |
2025-06-04 13:51:55 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:51:32 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-06-04 13:50:13 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 248 seconds) |
2025-06-04 13:49:58 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
2025-06-04 13:47:10 +0200 | entangledprime | (~entangled@176.223.172.171) (Ping timeout: 252 seconds) |
2025-06-04 13:46:51 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:46:26 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:39:27 +0200 | laurapigeon | (~laurapige@user/laurapigeon) laurapigeon |
2025-06-04 13:38:47 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:38:20 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-06-04 13:33:38 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
2025-06-04 13:31:27 +0200 | tromp | (~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2025-06-04 13:29:38 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
2025-06-04 13:29:29 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:29:16 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
2025-06-04 13:29:04 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:27:42 +0200 | bionade24 | (~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!) |
2025-06-04 13:21:53 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:21:28 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:20:43 +0200 | tromp | (~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) |
2025-06-04 13:17:34 +0200 | tromp | (~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2025-06-04 13:15:41 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:15:18 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:14:17 +0200 | GoldsteinQ | (~goldstein@goldstein.rs) |
2025-06-04 13:13:51 +0200 | GoldsteinQ | (~goldstein@goldstein.rs) (Quit: ZNC 1.8.2 - https://znc.in) |
2025-06-04 13:12:19 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
2025-06-04 13:09:29 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2025-06-04 13:08:31 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-04 13:08:07 +0200 | sabathan2 | (~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 +0200 | GoldsteinQ | (~goldstein@goldstein.rs) |
2025-06-04 13:05:38 +0200 | GoldsteinQ | (~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 +0200 | trickard | (~trickard@cpe-57-98-47-163.wireline.com.au) |
2025-06-04 13:04:55 +0200 | trickard | (~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 +0200 | tromp | (~textual@2001:1c00:3487:1b00:fdb0:a3b6:295:d798) |
2025-06-04 13:02:29 +0200 | sabathan2 | (~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 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-04 13:01:51 +0200 | jespada | (~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 +0200 | merijn | (~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? |