Newest at the top
| 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 |
| 2025-10-15 23:00:39 +0200 | Googulator63 | (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-15 23:00:39 +0200 | Googulator8 | (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 22:58:26 +0200 | <EvanR> | which is where it gets dicey to understand |
| 2025-10-15 22:58:07 +0200 | <EvanR> | there are ways to trick the type class system into "inferring" things right |
| 2025-10-15 22:57:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-10-15 22:57:21 +0200 | <tomsmeding> | I find singletons more verbose but also more powerful; my experience (doing type tetris) is that if the inference system is not clever enough to do what you want, you're suddenly in a bind, whereas with singletons it's limited by your programming (and tetris) skills only |
| 2025-10-15 22:57:09 +0200 | <EvanR> | in the modern version of that bug |
| 2025-10-15 22:57:01 +0200 | <EvanR> | GHC deletes your code if it type checks |
| 2025-10-15 22:56:34 +0200 | <monochrom> | haha |
| 2025-10-15 22:56:24 +0200 | <int-e> | monochrom: you need to be carefule when doing that; if things fit too well, your code disappears. |
| 2025-10-15 22:56:11 +0200 | <tomsmeding> | oh you're taking the typeclasses approach to type-level haskell masochism |
| 2025-10-15 22:56:07 +0200 | inline | (~inline@2a02:8071:57a1:1260:1c9a:31b4:1f4:c0dc) (Ping timeout: 260 seconds) |
| 2025-10-15 22:56:05 +0200 | <monochrom> | (It's the only reason why Proxy suffices.) |
| 2025-10-15 22:55:50 +0200 | <monochrom> | OK, I have also been doing withDict tetris. Is that OK? :) |
| 2025-10-15 22:54:54 +0200 | <tomsmeding> | if you can suffice with Proxy then you aren't doing enough tetris |
| 2025-10-15 22:54:45 +0200 | <monochrom> | (I have been doing that for type-assured modulus arithmetic, e.g., a+b `mod` m, where m is determined by a phantom type.) |
| 2025-10-15 22:54:40 +0200 | <tomsmeding> | I concur with singleton tetris |
| 2025-10-15 22:53:56 +0200 | <geekosaur> | I'd say singleton tetris |
| 2025-10-15 22:53:27 +0200 | <monochrom> | Hot take: Lean/Agda programming is type tetris, Haskell dependent type programming is Proxy tetris. :) |
| 2025-10-15 22:51:36 +0200 | inline | (~inline@2a02:8071:57a1:1260:1c9a:31b4:1f4:c0dc) Inline |
| 2025-10-15 22:50:28 +0200 | inline | (~inline@ip-178-202-059-161.um47.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2025-10-15 22:47:22 +0200 | inline | (~inline@ip-178-202-059-161.um47.pools.vodafone-ip.de) Inline |
| 2025-10-15 22:46:12 +0200 | inline | (~inline@2a02:8071:57a1:1260:590e:ee4d:f63f:13ad) (Ping timeout: 260 seconds) |
| 2025-10-15 22:44:15 +0200 | xmyth | (~xmyth@user/xmyth) xmyth |
| 2025-10-15 22:44:00 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-10-15 22:42:43 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-10-15 22:41:26 +0200 | trickard_ | (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 22:41:12 +0200 | trickard_ | (~trickard@cpe-62-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-15 22:40:42 +0200 | tromp | (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) |