Newest at the top
| 2025-10-23 14:54:18 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 256 seconds) |
| 2025-10-23 14:54:05 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-10-23 14:51:48 +0200 | <tomsmeding> | I figured that the answer would be no |
| 2025-10-23 14:51:42 +0200 | <tomsmeding> | thank you for trying though! |
| 2025-10-23 14:51:33 +0200 | <tomsmeding> | but yeah, this won't fly :p |
| 2025-10-23 14:51:28 +0200 | <tomsmeding> | Leary: the l12 can still be replaced by (Append l1 l2) in the body |
| 2025-10-23 14:49:39 +0200 | <Leary> | You might have to give up on this one. |
| 2025-10-23 14:49:24 +0200 | <Leary> | This is the best I was able to do (lol): https://play.haskell.org/saved/IIKMopeT |
| 2025-10-23 14:48:16 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) |
| 2025-10-23 14:48:03 +0200 | trickard | (~trickard@cpe-55-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-23 14:46:12 +0200 | <tomsmeding> | (hole-driven development becomes more useful if GHC can actually derive what the type of a hole should be) |
| 2025-10-23 14:45:36 +0200 | <tomsmeding> | this is not _necessary_ to be able to write my code but it would be good for developer ergonomics in my case |
| 2025-10-23 14:43:55 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-10-23 14:41:52 +0200 | <tomsmeding> | but foo2 does not because the semi-injectivity is not used |
| 2025-10-23 14:41:43 +0200 | <tomsmeding> | note that foo1 typechecks because with the first list literal, Append reduces and the list~list equality resolves to a l2~_ equality |
| 2025-10-23 14:41:10 +0200 | <tomsmeding> | Leary: I think this is a faithful abstraction/simplification of the behaviour that I'm looking for: https://play.haskell.org/saved/UAIlXBxX |
| 2025-10-23 14:38:32 +0200 | <mauke> | proposal: every language pragma should have an associated unicode character/emoji. then you could say {-# LANGUAGE ðŦð ðĪĄððŊðïļâðĻïļððŦĶð§âðĶē #-} |
| 2025-10-23 14:37:23 +0200 | <tomsmeding> | Leary: that works and the rest of my code compiles (after some messing around to let Append's kind be linked to the kind of the arguments), but it doesn't seem to help in practice |
| 2025-10-23 14:33:05 +0200 | <tomsmeding> | let me try that |
| 2025-10-23 14:32:52 +0200 | <tomsmeding> | yes I know you can merge LANGUAGE pragmata :) |
| 2025-10-23 14:32:30 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2025-10-23 14:31:35 +0200 | <Leary> | (see also, the style I've recently adopted for too many LANGUAGE pragmata) |
| 2025-10-23 14:31:17 +0200 | <Leary> | I'm not sure what the error message is actually complaining about (and I can't be bothered reading the manual to find out), but GHC will at least accept the first dependency with `UndecidableInstances`: https://play.haskell.org/saved/5T5D4ys5 |
| 2025-10-23 14:28:02 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-10-23 14:25:50 +0200 | Googulator56 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-23 14:25:41 +0200 | Googulator56 | (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-23 14:24:33 +0200 | Square2 | (~Square@user/square) (Ping timeout: 256 seconds) |
| 2025-10-23 14:24:16 +0200 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-10-23 14:22:18 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-10-23 14:11:45 +0200 | jreicher | (~user@user/jreicher) (Quit: In transit) |
| 2025-10-23 14:10:01 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-10-23 14:09:55 +0200 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-10-23 14:07:04 +0200 | trickard | (~trickard@cpe-55-98-47-163.wireline.com.au) |
| 2025-10-23 14:04:16 +0200 | <tomsmeding> | (if you put the dependency declarations on the same line as the class keyword, as they would normally be, this module has more language pragmas than lines of useful code) |
| 2025-10-23 14:03:37 +0200 | trickard_ | (~trickard@cpe-55-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-23 14:03:12 +0200 | <tomsmeding> | did I make a mistake? |
| 2025-10-23 14:03:08 +0200 | <tomsmeding> | uncommenting either of line 15 or 16 makes compilation fail |
| 2025-10-23 14:02:57 +0200 | <tomsmeding> | Leary: I can write that type class, but GHC doesn't seem to accept the dependencies: https://play.haskell.org/saved/EGhc89zh |
| 2025-10-23 14:00:31 +0200 | annamalai | (~annamalai@157.49.98.203) annamalai |
| 2025-10-23 13:55:08 +0200 | deptype | (~deptype@2406:b400:d4:c314:8332:aeaf:6094:c234) |
| 2025-10-23 13:54:50 +0200 | deptype | (~deptype@2406:b400:d4:c314:5abc:4b66:d843:af9d) (Remote host closed the connection) |
| 2025-10-23 13:54:27 +0200 | <Leary> | tomsmeding: Perhaps you can piggyback off `FunctionalDependencies`? Say: `class Append xs ys ~ xys => HasAppend xs ys xys | xs xys -> ys, ys xys -> xs where { type Append xs ys }` |
| 2025-10-23 13:40:04 +0200 | <tomsmeding> | is there a way I can tell GHC to use this implication in type inference? |
| 2025-10-23 13:39:52 +0200 | <tomsmeding> | now this thing is not injective in any of the standard ways, but we do have the property that Append a b ~ Append a c implies b ~ c |
| 2025-10-23 13:39:27 +0200 | <tomsmeding> | type family Append a b where { Append '[] b = b ; Append (x : xs) b = x : Append xs b } |
| 2025-10-23 13:39:08 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-10-23 13:38:52 +0200 | <tomsmeding> | is there a way to make the Append type family "half-injective"? |
| 2025-10-23 13:38:19 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
| 2025-10-23 13:37:52 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-10-23 13:35:49 +0200 | annamalai | (~annamalai@157.49.217.152) (Ping timeout: 256 seconds) |