Logs: liberachat/#haskell
| 2025-12-04 10:10:06 | → | fp joins (~Thunderbi@130.233.70.22) |
| 2025-12-04 10:20:27 | × | Googulator quits (~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-12-04 10:20:38 | → | Googulator joins (~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) |
| 2025-12-04 10:26:07 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2025-12-04 10:29:54 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-12-04 10:29:55 | → | Jackneill_ joins (~Jackneill@94-21-15-191.pool.digikabel.hu) |
| 2025-12-04 10:32:34 | × | Jackneill quits (~Jackneill@178-164-177-218.pool.digikabel.hu) (Ping timeout: 260 seconds) |
| 2025-12-04 10:33:05 | → | divlamir_ joins (~divlamir@user/divlamir) |
| 2025-12-04 10:34:32 | × | fp quits (~Thunderbi@130.233.70.22) (Remote host closed the connection) |
| 2025-12-04 10:34:51 | → | fp joins (~Thunderbi@130.233.70.22) |
| 2025-12-04 10:35:48 | × | divlamir quits (~divlamir@user/divlamir) (Ping timeout: 256 seconds) |
| 2025-12-04 10:35:49 | divlamir_ | is now known as divlamir |
| 2025-12-04 10:36:49 | → | tromp joins (~textual@2001:1c00:3487:1b00:a4ed:9e46:fd5d:6b4e) |
| 2025-12-04 10:44:51 | → | inline__ joins (~wbooze@cgn-195-14-220-195.nc.de) |
| 2025-12-04 10:46:55 | × | wbooze quits (~wbooze@2001-4dd4-1daa-0-5961-9b55-d1ca-8eee.ipv6dyn.netcologne.de) (Killed (uranium.libera.chat (Nickname regained by services))) |
| 2025-12-04 10:46:55 | inline__ | is now known as wbooze |
| 2025-12-04 10:47:11 | × | Googulator quits (~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (*.net *.split) |
| 2025-12-04 10:48:23 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (*.net *.split) |
| 2025-12-04 10:48:23 | × | chexum_ quits (~quassel@gateway/tor-sasl/chexum) (*.net *.split) |
| 2025-12-04 10:48:23 | × | califax quits (~califax@user/califx) (*.net *.split) |
| 2025-12-04 10:48:23 | × | gmg quits (~user@user/gehmehgeh) (*.net *.split) |
| 2025-12-04 10:48:23 | × | ec quits (~ec@gateway/tor-sasl/ec) (*.net *.split) |
| 2025-12-04 10:48:23 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (*.net *.split) |
| 2025-12-04 11:04:05 | → | poscat0x04 joins (~poscat@user/poscat) |
| 2025-12-04 11:04:13 | × | fp quits (~Thunderbi@130.233.70.22) (Ping timeout: 264 seconds) |
| 2025-12-04 11:05:06 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 252 seconds) |
| 2025-12-04 11:05:29 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 2025-12-04 11:05:32 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2025-12-04 11:05:40 | × | lambda_gibbon quits (~lambda_gi@2603:7080:ee00:37d8:313d:1898:c3f8:5287) (Ping timeout: 246 seconds) |
| 2025-12-04 11:05:45 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 245 seconds) |
| 2025-12-04 11:08:50 | × | Square2 quits (~Square4@user/square) (Quit: Leaving) |
| 2025-12-04 11:09:53 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds) |
| 2025-12-04 11:16:35 | × | DetourNetworkUK quits (~DetourNet@user/DetourNetworkUK) (Ping timeout: 245 seconds) |
| 2025-12-04 11:17:25 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds) |
| 2025-12-04 11:23:23 | → | fp joins (~Thunderbi@130.233.70.22) |
| 2025-12-04 11:26:15 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 2025-12-04 11:28:49 | × | xff0x quits (~xff0x@fs98a57788.tkyc008.ap.nuro.jp) (Ping timeout: 264 seconds) |
| 2025-12-04 11:38:59 | → | DetourNetworkUK joins (~DetourNet@user/DetourNetworkUK) |
| 2025-12-04 11:39:51 | × | annamalai quits (~annamalai@157.32.217.175) (Ping timeout: 265 seconds) |
| 2025-12-04 11:57:40 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 255 seconds) |
| 2025-12-04 11:59:30 | × | trickard quits (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-04 11:59:44 | → | trickard_ joins (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-04 12:00:23 | × | wbooze quits (~wbooze@cgn-195-14-220-195.nc.de) (Quit: Leaving) |
| 2025-12-04 12:02:58 | → | __monty__ joins (~toonn@user/toonn) |
| 2025-12-04 12:05:22 | → | srazkvt joins (~sarah@user/srazkvt) |
| 2025-12-04 12:12:30 | <lucabtz> | https://paste.tomsmeding.com/blBvVp0I does this make any sense to you? |
| 2025-12-04 12:12:41 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-12-04 12:19:20 | → | wbooze joins (~wbooze@2001-4dd4-1daa-0-acf3-bea0-8250-a5a2.ipv6dyn.netcologne.de) |
| 2025-12-04 12:21:10 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2025-12-04 12:24:15 | × | trickard_ quits (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-04 12:24:29 | → | trickard_ joins (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-04 12:26:25 | <tomsmeding> | yes |
| 2025-12-04 12:26:32 | <tomsmeding> | names are a little long, but that's personal :p |
| 2025-12-04 12:26:57 | <tomsmeding> | lucabtz: with the <= bound it's impossible to hvae an "impossible" BoundedNatural |
| 2025-12-04 12:27:06 | <tomsmeding> | so there is kind of one natural case that you cannot express |
| 2025-12-04 12:27:18 | → | merijn joins (~merijn@77.242.116.146) |
| 2025-12-04 12:27:29 | <tomsmeding> | this need not be a problem at all, but I find that things work a bit more nicely if you keep to the convention "lower bounds are inclusive, upper bounds are exclusive" |
| 2025-12-04 12:27:39 | <tomsmeding> | consider changing the <= to < |
| 2025-12-04 12:29:00 | × | PaulMartensen quits (15a119e437@2001:bc8:1210:2cd8::3bc) (Remote host closed the connection) |
| 2025-12-04 12:29:00 | × | Ging_ quits (46fea76d80@2001:bc8:1210:2cd8::470) (Remote host closed the connection) |
| 2025-12-04 12:29:00 | × | Typosit quits (b41a81e702@2001:bc8:1210:2cd8::494) (Remote host closed the connection) |
| 2025-12-04 12:29:44 | × | X-Scale quits (~ARM@50.65.114.89.rev.vodafone.pt) (Ping timeout: 240 seconds) |
| 2025-12-04 12:30:20 | → | PaulMartensen joins (2c15493d69@2001:bc8:1210:2cd8::3bc) |
| 2025-12-04 12:30:20 | → | Ging_ joins (46fea76d80@2001:bc8:1210:2cd8::470) |
| 2025-12-04 12:30:21 | → | Typosit joins (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 12:34:41 | × | Typosit quits (b41a81e702@2001:bc8:1210:2cd8::494) (Ping timeout: 244 seconds) |
| 2025-12-04 12:35:01 | × | PaulMartensen quits (2c15493d69@2001:bc8:1210:2cd8::3bc) (Ping timeout: 255 seconds) |
| 2025-12-04 12:35:02 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 2025-12-04 12:36:32 | × | hdggxin quits (~hdggxin@2401:4900:88a9:bff0:be1a:791c:4871:3d3b) (Remote host closed the connection) |
| 2025-12-04 12:36:35 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 240 seconds) |
| 2025-12-04 12:36:35 | × | Ging_ quits (46fea76d80@2001:bc8:1210:2cd8::470) (Ping timeout: 245 seconds) |
| 2025-12-04 12:36:35 | ljdarj1 | is now known as ljdarj |
| 2025-12-04 12:38:21 | <lucabtz> | yeah i might change to that |
| 2025-12-04 12:39:35 | <lucabtz> | im confused on how to go from value level to type level though, if it even is possible |
| 2025-12-04 12:39:56 | × | img quits (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2025-12-04 12:41:09 | → | xff0x joins (~xff0x@2405:6580:b080:900:d454:e7ea:27f9:454f) |
| 2025-12-04 12:41:11 | → | img joins (~img@user/img) |
| 2025-12-04 12:46:18 | → | lambda_gibbon joins (~lambda_gi@2603:7080:ee00:37d8:313d:1898:c3f8:5287) |
| 2025-12-04 12:47:50 | → | divya joins (divya@140.238.251.170) |
| 2025-12-04 12:53:20 | → | Ging_ joins (46fea76d80@2001:bc8:1210:2cd8::470) |
| 2025-12-04 12:54:05 | → | Typosit joins (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 12:55:20 | → | PaulMartensen joins (15a119e437@2001:bc8:1210:2cd8::3bc) |
| 2025-12-04 12:56:09 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 250 seconds) |
| 2025-12-04 12:56:38 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2025-12-04 12:58:59 | <tomsmeding> | lucabtz: what do you mean with that? |
| 2025-12-04 12:59:07 | × | Typosit quits (b41a81e702@2001:bc8:1210:2cd8::494) (Ping timeout: 265 seconds) |
| 2025-12-04 12:59:07 | × | Ging_ quits (46fea76d80@2001:bc8:1210:2cd8::470) (Ping timeout: 265 seconds) |
| 2025-12-04 12:59:45 | → | X-Scale joins (~ARM@50.65.114.89.rev.vodafone.pt) |
| 2025-12-04 13:03:03 | → | annamalai joins (~annamalai@157.32.218.49) |
| 2025-12-04 13:03:08 | × | PaulMartensen quits (15a119e437@2001:bc8:1210:2cd8::3bc) (Ping timeout: 256 seconds) |
| 2025-12-04 13:04:12 | → | Typosit joins (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 13:05:24 | <ski> | lucabtz : fwiw, i'd s/UnsafeMkBoundedNatural/PromiseBoundedNatural/, indicating that by using the constructor, you promise that the argument/component is bounded, and that by pattern-matching, you are being promised that the component is bounded |
| 2025-12-04 13:06:16 | × | Typosit quits (b41a81e702@2001:bc8:1210:2cd8::494) (Write error: error:80000068:system library::Connection reset by peer) |
| 2025-12-04 13:06:45 | <tomsmeding> | oh what might be even nicer is to keep UnsafeMkBoundedNatural, but provide a pattern synonym (Mk)BoundedNatural that does a dynamic check on construction |
| 2025-12-04 13:06:48 | <ski> | (also i'd implement `fromInteger', or else i'd say that `Show' instance is incorrect) |
| 2025-12-04 13:07:27 | <ski> | mm, yea, that would be possible |
| 2025-12-04 13:07:50 | <lucabtz> | i will look better into it later |
| 2025-12-04 13:09:20 | → | Square2 joins (~Square4@user/square) |
| 2025-12-04 13:09:27 | <lucabtz> | i think mkBoundedNatural should have a different signature taking the bound into account too. it should be done with SNat |
| 2025-12-04 13:09:29 | <ski> | (`showsPrec p (PromiseBoundedNatural n) = showParen (p > 10) $ showString "PromiseBoundedNatural " . showsPrec 11 n' is how i'd do `Show', if no `fromInteger' for `BoundedNatural bound') |
All times are in UTC.