Logs: liberachat/#haskell
| 2025-10-23 11:03:36 | → | deptype joins (~deptype@2406:b400:d4:c314:5abc:4b66:d843:af9d) |
| 2025-10-23 11:06:26 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-10-23 11:06:51 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-10-23 11:10:58 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-10-23 11:11:26 | → | Pixi` joins (~Pixi@user/pixi) |
| 2025-10-23 11:12:11 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-10-23 11:14:02 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 248 seconds) |
| 2025-10-23 11:15:40 | → | Googulator56 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-23 11:15:46 | × | Googulator71 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-23 11:31:19 | → | jreicher joins (~user@user/jreicher) |
| 2025-10-23 11:33:01 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 2025-10-23 11:35:05 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-10-23 11:35:49 | × | annamalai quits (~annamalai@157.49.217.152) (Ping timeout: 256 seconds) |
| 2025-10-23 11:37:52 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-10-23 11:38:19 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
| 2025-10-23 11:38:52 | <tomsmeding> | is there a way to make the Append type family "half-injective"? |
| 2025-10-23 11:39:08 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2025-10-23 11:39:27 | <tomsmeding> | type family Append a b where { Append '[] b = b ; Append (x : xs) b = x : Append xs b } |
| 2025-10-23 11:39:52 | <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 11:40:04 | <tomsmeding> | is there a way I can tell GHC to use this implication in type inference? |
| 2025-10-23 11:54:27 | <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 11:54:50 | × | deptype quits (~deptype@2406:b400:d4:c314:5abc:4b66:d843:af9d) (Remote host closed the connection) |
| 2025-10-23 11:55:08 | → | deptype joins (~deptype@2406:b400:d4:c314:8332:aeaf:6094:c234) |
| 2025-10-23 12:00:31 | → | annamalai joins (~annamalai@157.49.98.203) |
| 2025-10-23 12:02:57 | <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 12:03:08 | <tomsmeding> | uncommenting either of line 15 or 16 makes compilation fail |
| 2025-10-23 12:03:12 | <tomsmeding> | did I make a mistake? |
| 2025-10-23 12:03:37 | × | trickard_ quits (~trickard@cpe-55-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-23 12:04:16 | <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 12:07:04 | → | trickard joins (~trickard@cpe-55-98-47-163.wireline.com.au) |
| 2025-10-23 12:09:55 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-10-23 12:10:01 | → | weary-traveler joins (~user@user/user363627) |
| 2025-10-23 12:11:45 | × | jreicher quits (~user@user/jreicher) (Quit: In transit) |
| 2025-10-23 12:22:18 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-10-23 12:24:16 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-10-23 12:24:33 | × | Square2 quits (~Square@user/square) (Ping timeout: 256 seconds) |
| 2025-10-23 12:25:41 | × | Googulator56 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-23 12:25:50 | → | Googulator56 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-23 12:28:02 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-10-23 12:31:17 | <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 12:31:35 | <Leary> | (see also, the style I've recently adopted for too many LANGUAGE pragmata) |
| 2025-10-23 12:32:30 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2025-10-23 12:32:52 | <tomsmeding> | yes I know you can merge LANGUAGE pragmata :) |
| 2025-10-23 12:33:05 | <tomsmeding> | let me try that |
| 2025-10-23 12:37:23 | <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 12:38:32 | <mauke> | proposal: every language pragma should have an associated unicode character/emoji. then you could say {-# LANGUAGE 🫃😅🤡💌💯👁️🗨️👌🫦🧑🦲 #-} |
| 2025-10-23 12:41:10 | <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 12:41:43 | <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 12:41:52 | <tomsmeding> | but foo2 does not because the semi-injectivity is not used |
| 2025-10-23 12:43:55 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-10-23 12:45:36 | <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 12:46:12 | <tomsmeding> | (hole-driven development becomes more useful if GHC can actually derive what the type of a hole should be) |
| 2025-10-23 12:48:03 | × | trickard quits (~trickard@cpe-55-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-23 12:48:16 | → | trickard_ joins (~trickard@cpe-55-98-47-163.wireline.com.au) |
| 2025-10-23 12:49:24 | <Leary> | This is the best I was able to do (lol): https://play.haskell.org/saved/IIKMopeT |
| 2025-10-23 12:49:39 | <Leary> | You might have to give up on this one. |
| 2025-10-23 12:51:28 | <tomsmeding> | Leary: the l12 can still be replaced by (Append l1 l2) in the body |
| 2025-10-23 12:51:33 | <tomsmeding> | but yeah, this won't fly :p |
| 2025-10-23 12:51:42 | <tomsmeding> | thank you for trying though! |
| 2025-10-23 12:51:48 | <tomsmeding> | I figured that the answer would be no |
| 2025-10-23 12:54:05 | → | jreicher joins (~user@user/jreicher) |
| 2025-10-23 12:54:18 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 256 seconds) |
| 2025-10-23 12:57:44 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2025-10-23 12:57:54 | × | trickard_ quits (~trickard@cpe-55-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-23 12:58:03 | → | divlamir joins (~divlamir@user/divlamir) |
| 2025-10-23 12:59:02 | → | trickard_ joins (~trickard@cpe-55-98-47-163.wireline.com.au) |
| 2025-10-23 13:00:15 | <kuribas> | tomsmeding: type classes are the biggest impediment in hole driven programming, the same in idris. |
| 2025-10-23 13:00:31 | × | wbrawner quits (~wbrawner@static.56.224.132.142.clients.your-server.de) (Ping timeout: 240 seconds) |
| 2025-10-23 13:00:33 | <kuribas> | tomsmeding: I don't get why it cannot create a hole for a type class instance that depends on another hole. |
| 2025-10-23 13:00:39 | <tomsmeding> | kuribas: in my original code there aren't even any classes! |
| 2025-10-23 13:00:40 | → | wbrawner joins (~wbrawner@static.56.224.132.142.clients.your-server.de) |
| 2025-10-23 13:00:41 | × | Googulator56 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-23 13:00:49 | → | Googulator56 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-23 13:01:08 | <tomsmeding> | this is about type family injectivity; the type classes were brought in in an attempt to abuse FunctionalDependencies, which are apparently slightly stronger than tyfam injectivity |
| 2025-10-23 13:01:53 | <kuribas> | But why do this in haskell at all? |
| 2025-10-23 13:02:03 | <tomsmeding> | good question |
| 2025-10-23 13:02:04 | <kuribas> | If you are doing lots of type level computation, maybe idris is a better language. |
| 2025-10-23 13:02:16 | <kuribas> | (or agda, lean, ...) |
| 2025-10-23 13:02:18 | <tomsmeding> | I have considered multiple times to rewrite this in agda |
| 2025-10-23 13:02:46 | <kuribas> | What is it exactly you are doing? |
| 2025-10-23 13:02:55 | <tomsmeding> | but I concluded each time that the increase in convenience for type-level stuff would not be offset against the loss of convenience when actually doing something useful |
| 2025-10-23 13:03:09 | × | bggd quits (~bgg@2a01:e0a:819:1510:f0f7:e908:85f6:a650) (Remote host closed the connection) |
| 2025-10-23 13:03:09 | <tomsmeding> | kuribas: writing a compiler |
| 2025-10-23 13:03:26 | <tomsmeding> | with a well-typed well-scoped De Bruijn AST |
| 2025-10-23 13:03:31 | <kuribas> | ah :) |
| 2025-10-23 13:03:38 | <tomsmeding> | and I'm implementing a highly nontrivial code transformation in it that changes types a bunch |
| 2025-10-23 13:03:43 | <[exa]> | oh man. |
| 2025-10-23 13:03:46 | <[exa]> | :) |
| 2025-10-23 13:03:51 | <kuribas> | tomsmeding: prototype it in idris/agda, then port to haskell? |
| 2025-10-23 13:03:59 | <tomsmeding> | kuribas: sunk cost, at this point |
| 2025-10-23 13:04:10 | <tomsmeding> | it may or may not have been a good idea |
| 2025-10-23 13:04:31 | <kuribas> | idk, haskell to idris may not be too hard? |
| 2025-10-23 13:04:32 | <tomsmeding> | a taste: https://git.tomsmeding.com/chad-fast/tree/src/CHAD.hs |
| 2025-10-23 13:04:52 | <tomsmeding> | (this is the most complicated file in the project) |
| 2025-10-23 13:05:02 | → | Enrico63 joins (~Enrico63@host-82-59-110-109.retail.telecomitalia.it) |
| 2025-10-23 13:05:45 | → | cipherrot joins (~jez@user/petrichor) |
| 2025-10-23 13:06:57 | <tomsmeding> | [exa]: does that mean that you commiserate? |
| 2025-10-23 13:07:02 | <kuribas> | Edwin Bradey said that using dependent types helped a lot in getting the Debruyn indexes correct in his code. |
| 2025-10-23 13:07:09 | <kuribas> | In the idris2 compiler. |
| 2025-10-23 13:07:12 | <tomsmeding> | yeah so this is the same thing |
All times are in UTC.