Logs: liberachat/#haskell
| 2025-11-30 19:07:58 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-11-30 19:08:01 | × | smiesner quits (b0cf5acf8c@user/smiesner) (Ping timeout: 246 seconds) |
| 2025-11-30 19:08:07 | × | sus quits (1b7af6299f@user/zeromomentum) (Ping timeout: 264 seconds) |
| 2025-11-30 19:08:07 | × | lukec quits (9dfd4d094e@2a03:6000:1812:100::10e) (Ping timeout: 264 seconds) |
| 2025-11-30 19:08:07 | × | RussetParrotBear quits (45ce440a48@2a03:6000:1812:100::e2) (Ping timeout: 264 seconds) |
| 2025-11-30 19:08:14 | → | lukec joins (9dfd4d094e@2a03:6000:1812:100::10e) |
| 2025-11-30 19:08:15 | × | fvr quits (ef3e56ca8b@2a03:6000:1812:100::3c4) (Ping timeout: 245 seconds) |
| 2025-11-30 19:08:15 | × | chaitlatte0 quits (ea29c0bb16@user/chaitlatte0) (Ping timeout: 245 seconds) |
| 2025-11-30 19:08:15 | × | thatonelutenist quits (8216c46202@2a03:6000:1812:100::fb3) (Ping timeout: 245 seconds) |
| 2025-11-30 19:08:15 | × | exfalsoquodlibet quits (a7085e0f71@user/exfalsoquodlibet) (Ping timeout: 245 seconds) |
| 2025-11-30 19:08:15 | × | bsima1 quits (9d7e39c8ad@2a03:6000:1812:100::dd) (Ping timeout: 245 seconds) |
| 2025-11-30 19:08:21 | → | bsima1 joins (9d7e39c8ad@2a03:6000:1812:100::dd) |
| 2025-11-30 19:08:24 | × | aniketd quits (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 252 seconds) |
| 2025-11-30 19:08:24 | × | ajrdck quits (e0a4b72d53@user/ajrdck) (Ping timeout: 252 seconds) |
| 2025-11-30 19:08:57 | × | filwisher quits (2e6936c793@2a03:6000:1812:100::170) (Ping timeout: 250 seconds) |
| 2025-11-30 19:09:32 | → | stureplan joins (22e45d5caf@user/stureplan) |
| 2025-11-30 19:09:34 | → | filwisher joins (2e6936c793@2a03:6000:1812:100::170) |
| 2025-11-30 19:09:35 | → | pmk joins (6afe4476a1@2a03:6000:1812:100::26d) |
| 2025-11-30 19:09:35 | → | eso joins (a0662dfd5e@2a03:6000:1812:100::1266) |
| 2025-11-30 19:09:35 | → | evanrelf joins (3addc196af@2a03:6000:1812:100::f0) |
| 2025-11-30 19:09:35 | → | jakzale joins (6291399afa@user/jakzale) |
| 2025-11-30 19:09:35 | → | lane joins (809450f172@2a03:6000:1812:100::1300) |
| 2025-11-30 19:09:36 | → | ajrdck joins (e0a4b72d53@user/ajrdck) |
| 2025-11-30 19:09:36 | → | fn_lumi joins (3d621153a5@2a03:6000:1812:100::df7) |
| 2025-11-30 19:09:36 | → | thatonelutenist joins (8216c46202@2a03:6000:1812:100::fb3) |
| 2025-11-30 19:09:36 | → | aniketd joins (32aa4844cd@2a03:6000:1812:100::dcb) |
| 2025-11-30 19:09:36 | → | smiesner joins (b0cf5acf8c@user/smiesner) |
| 2025-11-30 19:09:36 | → | chr55 joins (57a0c161b0@user/chr55) |
| 2025-11-30 19:09:36 | → | jkoshy joins (99b9359beb@user/jkoshy) |
| 2025-11-30 19:09:36 | → | bheesham joins (3aa22d8375@2a03:6000:1812:100::e40) |
| 2025-11-30 19:09:36 | → | fvr joins (ef3e56ca8b@2a03:6000:1812:100::3c4) |
| 2025-11-30 19:09:36 | → | ymherklotz joins (cb2c9cfbdd@2a03:6000:1812:100::29a) |
| 2025-11-30 19:09:36 | → | arcadewise joins (52968ed80d@2a03:6000:1812:100::3df) |
| 2025-11-30 19:09:37 | → | b0o joins (0e4a0bf4c9@2a03:6000:1812:100::1bf) |
| 2025-11-30 19:09:37 | → | uint64_t joins (ec7b9bb9f3@2a03:6000:1812:100::139b) |
| 2025-11-30 19:09:37 | → | rprospero joins (eadde01e73@user/rprospero) |
| 2025-11-30 19:09:37 | → | sus joins (1b7af6299f@user/zeromomentum) |
| 2025-11-30 19:09:37 | → | sherbert joins (d006a0b946@2a03:6000:1812:100::155) |
| 2025-11-30 19:09:37 | → | ggb joins (a62ffbaf4f@2a03:6000:1812:100::3ac) |
| 2025-11-30 19:09:37 | → | fgaz joins (1ff9197ed6@2a03:6000:1812:100::11ea) |
| 2025-11-30 19:09:37 | → | raghavgururajan joins (ea769b8000@user/raghavgururajan) |
| 2025-11-30 19:09:38 | → | chaitlatte0 joins (ea29c0bb16@user/chaitlatte0) |
| 2025-11-30 19:09:38 | → | bgtdsword joins (b968c1779f@user/titibandit) |
| 2025-11-30 19:09:39 | → | exfalsoquodlibet joins (a7085e0f71@user/exfalsoquodlibet) |
| 2025-11-30 19:09:39 | → | cephei8 joins (b8652603d7@2a03:6000:1812:100::1535) |
| 2025-11-30 19:09:45 | → | ursa-major joins (114efe6c39@2a03:6000:1812:100::11f3) |
| 2025-11-30 19:09:52 | → | cpli joins (77fc530071@2a03:6000:1812:100::252) |
| 2025-11-30 19:09:55 | → | RussetParrotBear joins (45ce440a48@2a03:6000:1812:100::e2) |
| 2025-11-30 19:09:57 | → | septimi joins (9f60f4cb70@user/septimi) |
| 2025-11-30 19:09:57 | → | JoelMcCracken joins (5ea8252fbb@2a03:6000:1812:100::10e3) |
| 2025-11-30 19:09:57 | → | shreyasminocha joins (51fdc93eda@user/shreyasminocha) |
| 2025-11-30 19:09:57 | → | simendsjo joins (34b0550437@2a03:6000:1812:100::1441) |
| 2025-11-30 19:09:58 | → | samhh joins (7569f027cf@2a03:6000:1812:100::e4) |
| 2025-11-30 19:09:58 | → | rselim joins (ce261f06ff@user/milesrout) |
| 2025-11-30 19:09:58 | → | sm2n joins (ae95cb1267@user/sm2n) |
| 2025-11-30 19:10:00 | → | slondr joins (cf9f9e8f44@2a03:6000:1812:100::10b6) |
| 2025-11-30 19:10:01 | → | duncan joins (c6181279e3@user/meow/duncan) |
| 2025-11-30 19:10:02 | → | Ankhers joins (e99e97ef8e@2a03:6000:1812:100::2a2) |
| 2025-11-30 19:10:02 | → | lucyy joins (228ee8f0ce@user/lucyy) |
| 2025-11-30 19:10:05 | → | probie joins (cc0b34050a@user/probie) |
| 2025-11-30 19:10:06 | → | alethkit joins (23bd17ddc6@sourcehut/user/alethkit) |
| 2025-11-30 19:10:15 | → | whereiseveryone joins (206ba86c98@2a03:6000:1812:100::2e4) |
| 2025-11-30 19:10:22 | → | akspecs joins (00cc8321af@sourcehut/user/akspecs) |
| 2025-11-30 19:11:53 | → | samhh_ joins (7569f027cf@2a03:6000:1812:100::e4) |
| 2025-11-30 19:17:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 19:21:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 19:21:42 | → | karenw joins (~karenw@user/karenw) |
| 2025-11-30 19:24:26 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-11-30 19:24:57 | → | monochrm joins (trebla@216.138.220.146) |
| 2025-11-30 19:25:35 | × | ft quits (~ft@p508db844.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2025-11-30 19:25:56 | × | FANTOM quits (~fantom@212.228.181.156) (Ping timeout: 240 seconds) |
| 2025-11-30 19:26:01 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2025-11-30 19:26:15 | × | monochrom quits (trebla@216.138.220.146) (Ping timeout: 240 seconds) |
| 2025-11-30 19:26:16 | monochrm | is now known as monochrom |
| 2025-11-30 19:26:26 | → | weary-traveler joins (~user@user/user363627) |
| 2025-11-30 19:27:37 | → | ft joins (~ft@p508db844.dip0.t-ipconnect.de) |
| 2025-11-30 19:29:22 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2025-11-30 19:31:17 | → | FANTOM joins (~fantom@212.228.181.156) |
| 2025-11-30 19:32:25 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-11-30 19:39:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 19:43:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-11-30 19:47:33 | × | carbolymer quits (~carbolyme@delirium.systems) () |
| 2025-11-30 19:47:48 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 2025-11-30 19:48:16 | × | cephei8 quits (b8652603d7@2a03:6000:1812:100::1535) (Changing host) |
| 2025-11-30 19:48:16 | → | cephei8 joins (b8652603d7@user/cephei8) |
| 2025-11-30 19:52:57 | <hololeap> | I just realized that I don't exactly know what a "witness" is, even though I've intuited it, more or less |
| 2025-11-30 19:53:03 | <hololeap> | https://blog.jle.im/entry/introduction-to-singletons-1.html |
| 2025-11-30 19:53:09 | <hololeap> | > We say that SOpened is a runtime witness to s being 'Opened. |
| 2025-11-30 19:53:11 | <lambdabot> | <hint>:1:61: error: |
| 2025-11-30 19:53:11 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 2025-11-30 19:53:30 | <hololeap> | is there a proper definition somewhere? |
| 2025-11-30 19:54:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-11-30 19:54:36 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 252 seconds) |
| 2025-11-30 19:55:05 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-11-30 19:55:32 | <[exa]> | hololeap: tbh I was thinking about that very informally too. Usually turns out the SOened can't ever exist if the thing wasn't opened in the first place (unless people are cheating with unsafeCreateWitness or whatever) |
| 2025-11-30 19:56:39 | <[exa]> | and wait that might be the easier case. :D |
| 2025-11-30 19:56:39 | <hololeap> | could you, for instance, say that (Proxy 'Opened) is a type-level witness to Opened |
| 2025-11-30 19:56:42 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 2025-11-30 19:58:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-11-30 20:00:03 | <[exa]> | https://serokell.io/blog/haskell-type-level-witness sounds useful |
All times are in UTC.