Newest at the top
| 2025-10-15 23:49:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 23:49:13 +0200 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-10-15 23:45:49 +0200 | trickard_ | (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 23:45:23 +0200 | trickard_ | (~trickard@cpe-62-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-15 23:44:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-10-15 23:43:41 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2025-10-15 23:39:04 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Remote host closed the connection) |
| 2025-10-15 23:38:32 +0200 | inline | (~inline@2a02:8071:57a1:1260:a05d:8279:eac0:a03a) Inline |
| 2025-10-15 23:37:00 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-10-15 23:36:00 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2025-10-15 23:35:12 +0200 | titusg | (~user@31.94.22.246) (Ping timeout: 260 seconds) |
| 2025-10-15 23:34:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-10-15 23:30:25 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-10-15 23:29:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-10-15 23:28:44 +0200 | inline_ | (~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) (Ping timeout: 244 seconds) |
| 2025-10-15 23:28:28 +0200 | inline | (~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) (Client Quit) |
| 2025-10-15 23:28:20 +0200 | inline | (~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) Inline |
| 2025-10-15 23:27:43 +0200 | inline | (~inline@2a02:8071:57a1:dc0:d7:5433:321f:bfae) (Ping timeout: 246 seconds) |
| 2025-10-15 23:25:42 +0200 | Googulator45 | (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 23:25:41 +0200 | Googulator8 | (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-15 23:24:04 +0200 | inline_ | (~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) Inline |
| 2025-10-15 23:22:39 +0200 | Everything | (~Everythin@46.96.48.125) (Quit: leaving) |
| 2025-10-15 23:20:54 +0200 | trickard_ | (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 23:20:28 +0200 | trickard | (~trickard@cpe-62-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-15 23:18:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 23:16:33 +0200 | Everything | (~Everythin@46.96.48.125) Everything |
| 2025-10-15 23:15:28 +0200 | AlexNoo_ | AlexNoo |
| 2025-10-15 23:14:45 +0200 | mal1 | lieven |
| 2025-10-15 23:13:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-10-15 23:10:48 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-10-15 23:09:37 +0200 | xmyth | (~xmyth@user/xmyth) (Ping timeout: 244 seconds) |
| 2025-10-15 23:08:04 +0200 | gustrb | (~gustrb@191.243.134.87) (Ping timeout: 244 seconds) |
| 2025-10-15 23:07:52 +0200 | trickard_ | trickard |
| 2025-10-15 23:07:12 +0200 | <tomsmeding> | sorry for the wall |
| 2025-10-15 23:07:06 +0200 | <tomsmeding> | everything just works |
| 2025-10-15 23:07:05 +0200 | <monochrom> | But next, I also have (Z mod prime)[x] mod (x^2+x+1). I am not going to define a singleton type for polynomials! So I use withDict if the polynomial is a runtime input. (I have a class Modulus m where type Carrier m; modulus :: p m -> Carrier m. In that example, modulus _ = x^2+x+1.) |
| 2025-10-15 23:07:04 +0200 | <tomsmeding> | are you going to magic up a Monoid constraint on the (type family transformed) type? Not sure. If the types in the AST are singletons and the zero/plus operations are just functions that recurse on the singleton and do the right thing (the other side of the expression problem), then you just mirror the type family on the singleton values, and you apply the zero/plus functoins to the result and |
| 2025-10-15 23:07:02 +0200 | <tomsmeding> | another example where singletons worked for me where typeclasses didn't: I was writing a interpreter-ish thing where the object language had some built-in concept of a monoid. I wanted to implement a code transformation in there that also modified types; among other things, it mapped monoid types to different monoid types. If you represent monoidness with a Monoid constraint in the AST, then how |
| 2025-10-15 23:04:22 +0200 | inline | (~inline@2a02:8071:57a1:dc0:d7:5433:321f:bfae) Inline |
| 2025-10-15 23:04:00 +0200 | <monochrom> | For that one, KnownNat, SomeNat and someNatVal suffice. |
| 2025-10-15 23:03:21 +0200 | <tomsmeding> | if you manage to stay there, it's a good place to be |
| 2025-10-15 23:03:10 +0200 | <tomsmeding> | right, so maybe you're in the fragment where typeclass-based masochism works very well :) |
| 2025-10-15 23:02:56 +0200 | <monochrom> | No, I have (a+b) `mod` (natVal (Proxy :: Proxy m)). Only the modulus needs come from a type-level Nat. |
| 2025-10-15 23:02:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 23:02:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-10-15 23:01:51 +0200 | <tomsmeding> | unless you bring in a GHC plugin that does it for you |
| 2025-10-15 23:01:45 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-10-15 23:01:43 +0200 | <tomsmeding> | you... don't |
| 2025-10-15 23:01:37 +0200 | <tomsmeding> | if they're type-level Nats with KnownNat constraints around, how are you going to conjure up a KnownNat (a + b)? |
| 2025-10-15 23:01:20 +0200 | <tomsmeding> | suppose you have two type-level naturals that you want to add. If they're peano SNats and there's no library function for that, you just do the stupid peano addition |