2025/10/15

Newest at the top

2025-10-15 23:49:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-10-15 23:49:13 +0200takuan(~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
2025-10-15 23:45:49 +0200trickard_(~trickard@cpe-62-98-47-163.wireline.com.au)
2025-10-15 23:45:23 +0200trickard_(~trickard@cpe-62-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-10-15 23:44:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-10-15 23:43:41 +0200machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod
2025-10-15 23:39:04 +0200machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) (Remote host closed the connection)
2025-10-15 23:38:32 +0200inline(~inline@2a02:8071:57a1:1260:a05d:8279:eac0:a03a) Inline
2025-10-15 23:37:00 +0200jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 244 seconds)
2025-10-15 23:36:00 +0200machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod
2025-10-15 23:35:12 +0200titusg(~user@31.94.22.246) (Ping timeout: 260 seconds)
2025-10-15 23:34:27 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-10-15 23:28:44 +0200inline_(~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) (Ping timeout: 244 seconds)
2025-10-15 23:28:28 +0200inline(~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) (Client Quit)
2025-10-15 23:28:20 +0200inline(~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) Inline
2025-10-15 23:27:43 +0200inline(~inline@2a02:8071:57a1:dc0:d7:5433:321f:bfae) (Ping timeout: 246 seconds)
2025-10-15 23:25:42 +0200Googulator45(~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu)
2025-10-15 23:25:41 +0200Googulator8(~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed)
2025-10-15 23:24:04 +0200inline_(~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) Inline
2025-10-15 23:22:39 +0200Everything(~Everythin@46.96.48.125) (Quit: leaving)
2025-10-15 23:20:54 +0200trickard_(~trickard@cpe-62-98-47-163.wireline.com.au)
2025-10-15 23:20:28 +0200trickard(~trickard@cpe-62-98-47-163.wireline.com.au) (Ping timeout: 244 seconds)
2025-10-15 23:18:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-10-15 23:16:33 +0200Everything(~Everythin@46.96.48.125) Everything
2025-10-15 23:15:28 +0200AlexNoo_AlexNoo
2025-10-15 23:14:45 +0200mal1lieven
2025-10-15 23:13:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-10-15 23:10:48 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-10-15 23:09:37 +0200xmyth(~xmyth@user/xmyth) (Ping timeout: 244 seconds)
2025-10-15 23:08:04 +0200gustrb(~gustrb@191.243.134.87) (Ping timeout: 244 seconds)
2025-10-15 23:07:52 +0200trickard_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 +0200inline(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-10-15 23:02:06 +0200ChaiTRex(~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 +0200ChaiTRex(~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