Newest at the top
| 2026-02-05 12:30:19 +0100 | Enrico63 | (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-02-05 12:30:08 +0100 | oskarw | (~oskarw@user/oskarw) (Ping timeout: 256 seconds) |
| 2026-02-05 12:19:45 +0100 | wickedjargon | (~user@2605:8d80:5431:3c2c:999d:e956:3913:d370) (Remote host closed the connection) |
| 2026-02-05 12:18:45 +0100 | <mesaoptimizer> | jreicher: thanks, I'm already using haskell-mode and eglot, but haskell-mode seems finicky. I'll try haskell-ts-mode too I guess |
| 2026-02-05 12:17:24 +0100 | <mesaoptimizer> | edwardk: why is ARIA doing category theory work in rust? I was under the impression that rust has too much friction to be anywhere useful for anything related to applied category theory |
| 2026-02-05 12:16:56 +0100 | xff0x | (~xff0x@2405:6580:b080:900:e31d:86a4:6d4e:db85) |
| 2026-02-05 12:15:44 +0100 | <mesaoptimizer> | MSR dropped support for GHC? Lol |
| 2026-02-05 12:14:21 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-02-05 12:13:46 +0100 | <haskellbridge> | <loonycyborg> I'm honestly more used to != than to /= |
| 2026-02-05 12:03:29 +0100 | Enrico63 | (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) Enrico63 |
| 2026-02-05 11:55:02 +0100 | <tomsmeding> | \not= |
| 2026-02-05 11:54:58 +0100 | <tomsmeding> | or /not= |
| 2026-02-05 11:54:41 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-05 11:54:27 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-05 11:53:32 +0100 | oskarw | (~oskarw@user/oskarw) oskarw |
| 2026-02-05 11:52:48 +0100 | <gentauro> | tomsmeding: «completeness, /= is ≠» my bad. Yeah, I knew this -> `\neq in LaTeX` :( |
| 2026-02-05 11:51:53 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2026-02-05 11:49:06 +0100 | <tomsmeding> | but if you want to allow '[gap] text [gap]' then it becomes really awkward |
| 2026-02-05 11:48:56 +0100 | <dutchie> | yeah with alternation like that |
| 2026-02-05 11:48:48 +0100 | <dutchie> | I started trying to define some recursive list-like type |
| 2026-02-05 11:48:45 +0100 | <tomsmeding> | if you could require the whole thing to start and end with a Right, you could do an alternation thing |
| 2026-02-05 11:47:58 +0100 | <dutchie> | true |
| 2026-02-05 11:47:05 +0100 | <tomsmeding> | really, having two Rights in a row is useless too, is it? |
| 2026-02-05 11:46:44 +0100 | <dutchie> | and that |
| 2026-02-05 11:46:39 +0100 | <dutchie> | well I'm really using Text anyway |
| 2026-02-05 11:46:32 +0100 | <tomsmeding> | which is unergonomic as f* |
| 2026-02-05 11:46:22 +0100 | tomsmeding | . o O ( NonEmpty Char ) |
| 2026-02-05 11:44:40 +0100 | <dutchie> | (especially since Strings can be empty anyway, which immediately works around the whole point) |
| 2026-02-05 11:44:16 +0100 | <dutchie> | I think I am mostly asking out of interest about how you'd do type construction to enforce something like that |
| 2026-02-05 11:43:43 +0100 | <dutchie> | yeah I was definitely going to use something custom instead of Either |
| 2026-02-05 11:43:24 +0100 | <tomsmeding> | you can also consider a custom data type instead of Either, just to give the constructors more sensible names |
| 2026-02-05 11:42:39 +0100 | <tomsmeding> | possibly |
| 2026-02-05 11:42:29 +0100 | <dutchie> | I guess NonEmpty might be better at the very least |
| 2026-02-05 11:42:28 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-05 11:42:26 +0100 | <tomsmeding> | if you want the edge-case restrictions, impose them from outside |
| 2026-02-05 11:42:19 +0100 | <tomsmeding> | data structures typically work better if they represent a "neat" space of the possibilities without edge-case restrictions |
| 2026-02-05 11:42:16 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-05 11:41:56 +0100 | <tomsmeding> | and no Left the same |
| 2026-02-05 11:41:49 +0100 | <tomsmeding> | no Right just sounds like a stupid cloze to me, not an invalid one |
| 2026-02-05 11:41:46 +0100 | <dutchie> | morally yes, probably practically no |
| 2026-02-05 11:41:33 +0100 | <tomsmeding> | dutchie: do you really need the restrictoin that there's at least one Right and at least one Left? |
| 2026-02-05 11:36:58 +0100 | __monty__ | (~toonn@user/toonn) (Quit: Lost terminal) |
| 2026-02-05 11:32:27 +0100 | <dutchie> | so my example would be [Right "A", Left "ring", Right "is a structure with", Left "compatible addition and multiplication"] |
| 2026-02-05 11:31:28 +0100 | <dutchie> | hmm, how could I encode a cloze deletion thing (i.e. fill-in-the-blanks "a [ring] is structure with [compatible addition and multiplication]") as a Haskell data type. first thought would be [Either String String] where Left is deleted text and Right is plain but that doesn't encode "at least one left and one right in some order" |
| 2026-02-05 11:27:44 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-05 11:27:38 +0100 | bggd_ | (~bgg@2a01:e0a:fd5:f510:45eb:593:20bc:aaf7) |
| 2026-02-05 11:27:31 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-05 11:19:08 +0100 | acidjnk | (~acidjnk@p200300d6e700e57835d41376842fa308.dip0.t-ipconnect.de) acidjnk |
| 2026-02-05 11:17:01 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
| 2026-02-05 11:17:01 +0100 | haritz | (~hrtz@user/haritz) haritz |