Logs: liberachat/#haskell
| 2025-10-15 21:02:23 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 21:02:56 | <monochrom> | No, I have (a+b) `mod` (natVal (Proxy :: Proxy m)). Only the modulus needs come from a type-level Nat. |
| 2025-10-15 21:03:10 | <tomsmeding> | right, so maybe you're in the fragment where typeclass-based masochism works very well :) |
| 2025-10-15 21:03:21 | <tomsmeding> | if you manage to stay there, it's a good place to be |
| 2025-10-15 21:04:00 | <monochrom> | For that one, KnownNat, SomeNat and someNatVal suffice. |
| 2025-10-15 21:04:22 | → | inline joins (~inline@2a02:8071:57a1:dc0:d7:5433:321f:bfae) |
| 2025-10-15 21:07:02 | <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 21:07:04 | <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 21:07:05 | <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 21:07:06 | <tomsmeding> | everything just works |
| 2025-10-15 21:07:12 | <tomsmeding> | sorry for the wall |
| 2025-10-15 21:07:52 | trickard_ | is now known as trickard |
| 2025-10-15 21:08:04 | × | gustrb quits (~gustrb@191.243.134.87) (Ping timeout: 244 seconds) |
| 2025-10-15 21:09:37 | × | xmyth quits (~xmyth@user/xmyth) (Ping timeout: 244 seconds) |
| 2025-10-15 21:10:48 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2025-10-15 21:13:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 21:14:45 | mal1 | is now known as lieven |
| 2025-10-15 21:15:28 | AlexNoo_ | is now known as AlexNoo |
| 2025-10-15 21:16:33 | → | Everything joins (~Everythin@46.96.48.125) |
| 2025-10-15 21:18:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 21:20:28 | × | trickard quits (~trickard@cpe-62-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-15 21:20:54 | → | trickard_ joins (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 21:22:39 | × | Everything quits (~Everythin@46.96.48.125) (Quit: leaving) |
| 2025-10-15 21:24:04 | → | inline_ joins (~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) |
| 2025-10-15 21:25:41 | × | Googulator8 quits (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-15 21:25:42 | → | Googulator45 joins (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 21:27:43 | × | inline quits (~inline@2a02:8071:57a1:dc0:d7:5433:321f:bfae) (Ping timeout: 246 seconds) |
| 2025-10-15 21:28:20 | → | inline joins (~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) |
| 2025-10-15 21:28:28 | × | inline quits (~inline@2a02:8071:57a1:1260:1db9:c9bb:4c1f:b2b7) (Client Quit) |
| 2025-10-15 21:28:44 | × | inline_ quits (~inline@2a02:8071:57a1:1260:b1ed:dc4f:eb19:541d) (Ping timeout: 244 seconds) |
| 2025-10-15 21:29:11 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 21:30:25 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2025-10-15 21:34:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-10-15 21:35:12 | × | titusg quits (~user@31.94.22.246) (Ping timeout: 260 seconds) |
| 2025-10-15 21:36:00 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2025-10-15 21:37:00 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-10-15 21:38:32 | → | inline joins (~inline@2a02:8071:57a1:1260:a05d:8279:eac0:a03a) |
| 2025-10-15 21:39:04 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Remote host closed the connection) |
| 2025-10-15 21:43:41 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2025-10-15 21:44:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 21:45:23 | × | trickard_ quits (~trickard@cpe-62-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-15 21:45:49 | → | trickard_ joins (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 21:49:13 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection) |
| 2025-10-15 21:49:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 21:52:30 | × | trickard_ quits (~trickard@cpe-62-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-10-15 21:53:52 | × | mreh quits (~matthew@host86-146-25-125.range86-146.btcentralplus.com) (Ping timeout: 260 seconds) |
| 2025-10-15 21:55:49 | → | trickard_ joins (~trickard@cpe-60-98-47-163.wireline.com.au) |
| 2025-10-15 21:57:32 | → | TriN joins (~tnguyen@69.74.159.34) |
| 2025-10-15 21:58:08 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Read error: Connection reset by peer) |
| 2025-10-15 21:58:21 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2025-10-15 21:59:42 | × | inline quits (~inline@2a02:8071:57a1:1260:a05d:8279:eac0:a03a) (Quit: Leaving) |
| 2025-10-15 22:00:36 | → | jrm2 joins (~jrm@user/jrm) |
| 2025-10-15 22:00:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 22:00:48 | → | Tuplanolla1 joins (~Tuplanoll@91-159-187-167.elisa-laajakaista.fi) |
| 2025-10-15 22:01:48 | × | CiaoSen quits (~Jura@ipservice-092-210-206-067.092.210.pools.vodafone-ip.de) (Ping timeout: 244 seconds) |
| 2025-10-15 22:03:37 | → | lol_ joins (~lol@2603:3016:1e01:b9c0:4892:4dea:36cf:7d26) |
| 2025-10-15 22:03:48 | × | bggd quits (~bgg@2a01:e0a:819:1510:a422:7a58:5231:4299) (Remote host closed the connection) |
| 2025-10-15 22:03:59 | → | ft_ joins (~ft@p4fc2a207.dip0.t-ipconnect.de) |
| 2025-10-15 22:04:31 | × | FANTOM quits (~fantom@90.244.183.5) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | Tuplanolla quits (~Tuplanoll@91-159-187-167.elisa-laajakaista.fi) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | bramh quits (~bramh@user/bramh) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | craunts795335385 quits (~craunts@136.158.7.194) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | Tri quits (~tnguyen@69.74.159.34) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | Ekho quits (~Ekho@user/ekho) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | jrm quits (~jrm@user/jrm) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | lortabac quits (~lortabac@mx1.fracta.dev) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | ft quits (~ft@p4fc2a207.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | otto_s quits (~user@p5de2f68d.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | × | Jonno_FTW quits (~come@user/jonno-ftw/x-0835346) (Ping timeout: 256 seconds) |
| 2025-10-15 22:04:32 | → | FANTOM joins (~fantom@90.244.183.5) |
| 2025-10-15 22:04:32 | jrm2 | is now known as jrm |
| 2025-10-15 22:04:33 | trickard_ | is now known as trickard |
| 2025-10-15 22:04:34 | ft_ | is now known as ft |
| 2025-10-15 22:04:38 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-10-15 22:04:49 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 2025-10-15 22:05:16 | → | Tri joins (~tnguyen@69.74.159.34) |
| 2025-10-15 22:05:33 | × | rubin55 quits (sid666180@id-666180.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-10-15 22:05:33 | × | b0o quits (0e4a0bf4c9@2a03:6000:1812:100::1bf) (Ping timeout: 260 seconds) |
| 2025-10-15 22:05:38 | × | nshepperd2 quits (~nshepperd@2a01:4f9:3b:4cc9::2) (Quit: Ping timeout (120 seconds)) |
| 2025-10-15 22:05:43 | → | rubin55_ joins (sid666180@id-666180.ilkley.irccloud.com) |
| 2025-10-15 22:05:48 | → | nshepperd2 joins (~nshepperd@2a01:4f9:3b:4cc9::2) |
| 2025-10-15 22:05:51 | → | otto_s joins (~user@p5de2f68d.dip0.t-ipconnect.de) |
| 2025-10-15 22:05:55 | → | b0o joins (0e4a0bf4c9@2a03:6000:1812:100::1bf) |
| 2025-10-15 22:06:43 | × | haltsolver quits (~cmo@2604:3d09:207f:8000::d1dc) (Read error: Connection reset by peer) |
| 2025-10-15 22:07:17 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b9c0:4892:4dea:36cf:7d26) (Ping timeout: 260 seconds) |
| 2025-10-15 22:07:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-10-15 22:07:52 | × | TriN quits (~tnguyen@69.74.159.34) (Ping timeout: 260 seconds) |
| 2025-10-15 22:08:09 | → | TriN joins (~tnguyen@69.74.159.34) |
| 2025-10-15 22:08:14 | → | ss4 joins (~wootehfoo@user/wootehfoot) |
| 2025-10-15 22:12:28 | → | orizuru joins (~orizuru@user/orizuru) |
| 2025-10-15 22:12:53 | → | jrm2 joins (~jrm@user/jrm) |
| 2025-10-15 22:12:55 | → | machined1od joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2025-10-15 22:12:59 | → | ft_ joins (~ft@p4fc2a207.dip0.t-ipconnect.de) |
| 2025-10-15 22:13:48 | × | ProofTechnique_ quits (sid79547@id-79547.ilkley.irccloud.com) (Ping timeout: 246 seconds) |
| 2025-10-15 22:13:55 | × | malte quits (~malte@mal.tc) (Ping timeout: 246 seconds) |
| 2025-10-15 22:13:55 | × | tnks quits (sid412124@id-412124.helmsley.irccloud.com) (Ping timeout: 246 seconds) |
| 2025-10-15 22:13:55 | × | edwardk quits (sid47016@haskell/developer/edwardk) (Ping timeout: 246 seconds) |
| 2025-10-15 22:14:16 | → | Square2 joins (~Square@user/square) |
| 2025-10-15 22:14:20 | → | malte joins (~malte@mal.tc) |
All times are in UTC.