Logs: liberachat/#haskell
| 2025-09-28 18:30:33 | <tomsmeding> | what do you mean with "add an instance statement" precisely? |
| 2025-09-28 18:31:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-09-28 18:31:55 | <tomsmeding> | oh you mean an instance for VerseIndex, not an instance for KnownSymbol |
| 2025-09-28 18:32:04 | <tomsmeding> | yeah that makes perfect sense |
| 2025-09-28 18:32:39 | <tomsmeding> | though I do wonder why the class is necessary |
| 2025-09-28 18:36:02 | <tomsmeding> | dcpagan: https://play.haskell.org/saved/YzCmA0EI works fine for me |
| 2025-09-28 18:36:15 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-09-28 18:36:15 | <tomsmeding> | I did have to convert the "type signatures" for Verses/Stanza/Song to StandaloneKindSignatures |
| 2025-09-28 18:38:24 | <dcpagan> | tomsmeding: Before, I forgot to add the line "instance (KnownNat n, n <= SongLength) => VerseIndex (n :: Natural)" |
| 2025-09-28 18:38:45 | <tomsmeding> | right |
| 2025-09-28 18:39:01 | <tomsmeding> | that line has nothing to do with KnownSymbol, though :) |
| 2025-09-28 18:39:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-28 18:40:07 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 240 seconds) |
| 2025-09-28 18:41:09 | × | fp quits (~Thunderbi@2001-14ba-6e24-3000--198.rev.dnainternet.fi) (Ping timeout: 252 seconds) |
| 2025-09-28 18:41:45 | <dcpagan> | I am getting conflicting conflicting type instances from the commented block of code: |
| 2025-09-28 18:41:58 | <dcpagan> | https://github.com/DCPagan/Exercism-Haskell/blob/62845d21c972414c648e69a456990a00280c3faa/house/src/House.hs#L124-L127 |
| 2025-09-28 18:42:29 | <dcpagan> | I want to encapsulate the constraints and type errors in a separate instance. |
| 2025-09-28 18:42:36 | <tomsmeding> | instances are chosen/disambiguated purely based on the part to the right of the => |
| 2025-09-28 18:42:43 | <tomsmeding> | so both your `VerseIndex n` instances apply to all n |
| 2025-09-28 18:42:53 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 250 seconds) |
| 2025-09-28 18:43:05 | <tomsmeding> | haskell typeclasses are not a logic programming language, unfortunately |
| 2025-09-28 18:43:08 | <dcpagan> | So how do I constrain the kind variables? |
| 2025-09-28 18:43:19 | <tomsmeding> | with instances, you don't |
| 2025-09-28 18:43:24 | <dcpagan> | That sucks. |
| 2025-09-28 18:43:33 | <tomsmeding> | you can use type families though :) |
| 2025-09-28 18:43:43 | <tomsmeding> | I don't see why you cannot just compute these things with type families |
| 2025-09-28 18:44:25 | <dcpagan> | Can I pattern match with type families? |
| 2025-09-28 18:44:28 | × | bgg quits (~bgg@2a01:e0a:819:1510:ce70:2793:3b21:6fbd) (Remote host closed the connection) |
| 2025-09-28 18:44:41 | <tomsmeding> | use https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeLits.html#t:-60--61--63- and https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Type-Bool.html#t:If |
| 2025-09-28 18:45:03 | <tomsmeding> | dcpagan: what is `Song' Nothing = "" ; Song' (Just n) = ...` doing if not pattern matching? |
| 2025-09-28 18:45:15 | <tomsmeding> | but in this case, you don't want to pattern-match, you want to have a conditional on <= |
| 2025-09-28 18:45:24 | <dcpagan> | Last time I tried Data.Type.Bool.If, I got reduction stack overflows. |
| 2025-09-28 18:45:42 | <dcpagan> | It's why I refactored to recursion with Maybe Natural. |
| 2025-09-28 18:45:53 | <tomsmeding> | sure, you can do that here too |
| 2025-09-28 18:46:02 | <dcpagan> | I want to guard against naturals beyond a certain value. |
| 2025-09-28 18:46:04 | <tomsmeding> | but I expect the If to work |
| 2025-09-28 18:46:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-09-28 18:47:12 | <tomsmeding> | instance selection is "greedy" in haskell, no backtracking is performed |
| 2025-09-28 18:47:38 | <tomsmeding> | the algorithm does, however, guard against ambiguity: an instance is chosen only if it can be determined, without looking at the constraints, that it's the only one that matches |
| 2025-09-28 18:47:56 | <tomsmeding> | this means that the result of the greedy algorithm is always compatible with what a full backtracking algorithm would have produced |
| 2025-09-28 18:49:12 | <tomsmeding> | why exactly this choice for greediness was made I don't know; perhaps to not accidentally build a prolog |
| 2025-09-28 18:49:33 | <tomsmeding> | and retain sane compile times |
| 2025-09-28 18:52:19 | <EvanR> | warning warning prolog detected. Abort |
| 2025-09-28 18:52:26 | <EvanR> | it's too late |
| 2025-09-28 18:57:57 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-28 19:00:03 | × | caconym74787 quits (~caconym@user/caconym) (Quit: bye) |
| 2025-09-28 19:00:12 | <[exa]> | EvanR: no one used cut yet! backtrack! |
| 2025-09-28 19:00:47 | → | caconym74787 joins (~caconym@user/caconym) |
| 2025-09-28 19:01:40 | <dcpagan> | I used Data.Type.Bool.If, and there were no reduction stack overflows. |
| 2025-09-28 19:01:43 | <dcpagan> | https://github.com/DCPagan/Exercism-Haskell/blob/73c27000e602ea2fe1718f552b717ae62a490257/house/src/House.hs#L109-L118 |
| 2025-09-28 19:02:19 | <dcpagan> | Would this render redundant the constraint (n <= SongLength)? |
| 2025-09-28 19:02:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-09-28 19:07:30 | <dcpagan> | The only thing I'm missing is specifying the input index in the custom type error message. |
| 2025-09-28 19:08:01 | <dcpagan> | How do I convert a Natural to a Symbol for displaying in a custom type error message? |
| 2025-09-28 19:08:17 | <dcpagan> | Like a type-promoted show? |
| 2025-09-28 19:08:33 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-09-28 19:10:13 | × | trickard_ quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Ping timeout: 264 seconds) |
| 2025-09-28 19:12:19 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 2025-09-28 19:12:36 | → | tromp joins (~textual@2001:1c00:3487:1b00:259a:5516:59ca:4e5) |
| 2025-09-28 19:12:53 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-09-28 19:13:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-28 19:17:16 | <tomsmeding> | dcpagan: use ShowType? https://hackage.haskell.org/package/base-4.20.0.1/docs/GHC-TypeError.html#t:ErrorMessage |
| 2025-09-28 19:17:40 | <tomsmeding> | dcpagan: why is the instance still there? Why are Verses/Stanza/Song not just top-level type families at this point? |
| 2025-09-28 19:18:07 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-09-28 19:18:24 | <tomsmeding> | a class with a single, blanket instance (like you have here with VerseIndex) is very rarely useful |
| 2025-09-28 19:18:37 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-09-28 19:19:05 | <tomsmeding> | there are very specific reasons why you may need such a thing sometimes (in particular if it appears in a QuantifiedConstraint elsewhere), but none of those apply here |
| 2025-09-28 19:20:45 | × | Googulator64 quits (~Googulato@2a01-036d-0106-03fa-f110-0864-c42c-107f.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-09-28 19:20:56 | → | Googulator64 joins (~Googulato@2a01-036d-0106-03fa-f110-0864-c42c-107f.pool6.digikabel.hu) |
| 2025-09-28 19:21:16 | <dcpagan> | I was planning on constraining the type family with the constraint. |
| 2025-09-28 19:21:19 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-09-28 19:22:31 | <tomsmeding> | right |
| 2025-09-28 19:25:38 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 272 seconds) |
| 2025-09-28 19:27:04 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2025-09-28 19:29:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-28 19:30:30 | <dcpagan> | Do custom type errors always make such constraints redundant? |
| 2025-09-28 19:30:42 | × | Googulator64 quits (~Googulato@2a01-036d-0106-03fa-f110-0864-c42c-107f.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-09-28 19:30:43 | → | Googulator59 joins (~Googulato@193-226-241-153.pool.digikabel.hu) |
| 2025-09-28 19:30:48 | <dcpagan> | Latest update: https://github.com/DCPagan/Exercism-Haskell/blob/master/house/src/House.hs |
| 2025-09-28 19:31:32 | <dcpagan> | I really like how custom type errors are immediately communicated to the IDE. |
| 2025-09-28 19:32:05 | <dcpagan> | It's like I'm programming the IDE to gently hand-hold anyone who inherits this code. |
| 2025-09-28 19:34:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-09-28 19:37:56 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-09-28 19:39:50 | × | arandombit quits (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2025-09-28 19:40:07 | → | arandombit joins (~arandombi@2603:7000:4600:ffbe:b1d5:1527:b9ee:ee90) |
| 2025-09-28 19:40:07 | × | arandombit quits (~arandombi@2603:7000:4600:ffbe:b1d5:1527:b9ee:ee90) (Changing host) |
| 2025-09-28 19:40:07 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-09-28 19:40:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-28 19:45:19 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2025-09-28 19:46:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-09-28 19:47:54 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 244 seconds) |
| 2025-09-28 19:48:45 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 2025-09-28 19:49:29 | <tomsmeding> | well, the kind of type-level programming that you're doing here is not quite what the type system was designed for :) |
| 2025-09-28 19:50:09 | <tomsmeding> | if your type class had a value in it too, then you would not have been able to eliminate the type class |
| 2025-09-28 19:51:12 | <tomsmeding> | usually, if there's a sensible place to put a constraint and thereby save an explicit If in a type family, using the constraint is the better choice |
| 2025-09-28 19:51:25 | <tomsmeding> | because constraints behave more nicely in the type system, in general |
| 2025-09-28 19:51:49 | <tomsmeding> | but in this case you have no values in the first place, so there is no sensible place to put a constraint, so TypeError it is |
| 2025-09-28 19:53:27 | <EvanR> | you have class but no value |
| 2025-09-28 19:53:39 | <EvanR> | an awkward position to be in |
| 2025-09-28 19:53:46 | <tomsmeding> | rather |
All times are in UTC.