Newest at the top
| 2025-12-01 23:58:52 +0100 | <ski> | zoil : i would not call `WhichNE' a singleton, since it does not reflect the structure of the type index in the value (you can't recover the structure of the index, by pattern-matching on the value) |
| 2025-12-01 23:58:32 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-01 23:57:47 +0100 | <haskellbridge> | <zoil> bah, what a waste of time |
| 2025-12-01 23:53:56 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-01 23:48:00 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-12-01 23:47:39 +0100 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-12-01 23:42:20 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-01 23:36:13 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-01 23:34:57 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2025-12-01 23:34:46 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2025-12-01 23:33:40 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-01 23:32:09 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 250 seconds) |
| 2025-12-01 23:30:06 +0100 | st_aldini | (~Thunderbi@2605:a601:a07c:7400:6e26:f360:f11d:472c) st_aldini |
| 2025-12-01 23:27:38 +0100 | <haskellbridge> | <zoil> :-( |
| 2025-12-01 23:27:32 +0100 | <haskellbridge> | <zoil> this defies the whole point |
| 2025-12-01 23:27:24 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2025-12-01 23:27:20 +0100 | <haskellbridge> | <zoil> but now im not going to be able to assert the exhaustive coverage of the singletons! |
| 2025-12-01 23:26:50 +0100 | <haskellbridge> | <zoil> like, i provide 2 instances which might help match in consequent instances |
| 2025-12-01 23:26:05 +0100 | <haskellbridge> | <zoil> i think im still going to end up picking up a constraint... |
| 2025-12-01 23:25:45 +0100 | <haskellbridge> | <zoil> so these whichNE are like type witnesses? |
| 2025-12-01 23:24:55 +0100 | <haskellbridge> | <zoil> https://play.haskell.org/saved/GwyPOlmo |
| 2025-12-01 23:24:52 +0100 | <haskellbridge> | <zoil> here |
| 2025-12-01 23:24:51 +0100 | <haskellbridge> | <zoil> sory the paste didnt update |
| 2025-12-01 23:24:45 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-01 23:24:31 +0100 | trickard | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-01 23:20:48 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2025-12-01 23:20:26 +0100 | <haskellbridge> | <zoil> idk what im supposed to do next |
| 2025-12-01 23:19:52 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-12-01 23:15:47 +0100 | <haskellbridge> | <zoil> i got to take a break for a bit now, that kind of used up my available programming energy |
| 2025-12-01 23:15:19 +0100 | <haskellbridge> | <zoil> glguy also put this which might help; https://paste.tomsmeding.com/UEfrQUiN |
| 2025-12-01 23:14:06 +0100 | <haskellbridge> | https://play.haskell.org/saved/9XWoHwsD |
| 2025-12-01 23:14:06 +0100 | <haskellbridge> | <zoil> i put the extra bit for the refactoring; |
| 2025-12-01 23:13:38 +0100 | <merijn> | tomsmeding: Yeah, I got it working, just need to figure out which stupid linters to turn on |
| 2025-12-01 23:12:59 +0100 | <tomsmeding> | assuming you're using the nvim builtin LSP client and not something else |
| 2025-12-01 23:12:39 +0100 | <tomsmeding> | (lua) |
| 2025-12-01 23:12:27 +0100 | <tomsmeding> | merijn: possibly add vim.lsp.enable('hls') afterwards |
| 2025-12-01 23:10:24 +0100 | <tomsmeding> | merijn: https://paste.tomsmeding.com/iS6vrndp |
| 2025-12-01 23:03:57 +0100 | <haskellbridge> | https://play.haskell.org/saved/9XWoHwsD |
| 2025-12-01 23:03:57 +0100 | <haskellbridge> | <zoil> i think this version should be interactive |
| 2025-12-01 23:02:27 +0100 | michalz | (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-12-01 23:02:06 +0100 | <haskellbridge> | <zoil> i thought the ide would allow to share and edit and compile, but it makes it readonly |
| 2025-12-01 23:02:00 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-01 23:01:47 +0100 | <haskellbridge> | <zoil> so WhichNE is a singleton datatype? and it acts as a type witness allowing the instances to have just one class instance, and then it wont require the constraint? |
| 2025-12-01 23:01:47 +0100 | <ski> | fgarcia : well, these are (somewhat) standard formal (meta-)notation, when talking about abstract syntax of programming languages, logics, specification languages, &c. |
| 2025-12-01 23:00:37 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/vssawUkriMdYrWhgxHeCbFgP/6JDVkeGWpLw (3 lines) |
| 2025-12-01 23:00:37 +0100 | <haskellbridge> | <zoil> data Transfers (xs :: Nonempty *) where |
| 2025-12-01 22:59:54 +0100 | <ski> | zoil : so the `KnownNE xs', when pattern-matching on the value of `knownNE', will inform the type-checker that either `xs = Cons x ys' or `xs = Last x' (for some unknown `x',`ys'), and then presumably that helps with `read' (ought to be `readsPrec', really) knowing what to expect (presumably `Transfers' is a GADT) |
| 2025-12-01 22:59:36 +0100 | <haskellbridge> | <zoil> https://kf8nh.com/_heisenbridge/media/matrix.org/GPGBChpFvPQwIjAnsVOZLpwr/D5DpfDeh0w0/image.png |
| 2025-12-01 22:58:03 +0100 | <merijn> | bad new, it's giving me stupid refactor instructions >.> |
| 2025-12-01 22:57:59 +0100 | <haskellbridge> | <zoil> so, on line 96 there is this terrifying constraint |
