Logs: liberachat/#haskell
| 2025-10-24 17:07:11 | Guest54 | is now known as Berimor |
| 2025-10-24 17:07:41 | × | Berimor quits (~Guest54@95.68.100.1) (Client Quit) |
| 2025-10-24 17:08:43 | → | qqe joins (~qqq@185.54.23.200) |
| 2025-10-24 17:10:56 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 2025-10-24 17:15:13 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-24 17:15:55 | × | tabaqui quits (~tabaqui@167.71.80.236) (Quit: WeeChat 4.7.1) |
| 2025-10-24 17:18:02 | → | bggd joins (~bgg@2a01:e0a:819:1510:7bcd:1a48:39fb:eb8e) |
| 2025-10-24 17:18:06 | → | jespada joins (~jespada@2800:a4:225c:5f00:7482:e18d:48f6:46e9) |
| 2025-10-24 17:23:06 | × | jespada quits (~jespada@2800:a4:225c:5f00:7482:e18d:48f6:46e9) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-10-24 17:25:30 | × | Googulator71 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 17:25:40 | → | Googulator71 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 17:31:36 | <tomsmeding> | Here's an idle complaint that you may well ignore if you want to. |
| 2025-10-24 17:31:50 | <tomsmeding> | Lists have nice syntax in Haskell, and they carry that syntax to the type level too: type-level lists are nice. |
| 2025-10-24 17:32:04 | <tomsmeding> | However, typing environments in programming language theory are snoc lists, not cons lists. |
| 2025-10-24 17:32:47 | <tomsmeding> | So if you have a well-typed AST indexed by a type-level list indicating the typing environment, then you have a choice: either your type-level list goes the wrong way and you hvae to mentally reverse all the time, or you use your own custom snoc list data type and lose the nice list syntax. |
| 2025-10-24 17:33:08 | <tomsmeding> | Can't have nice things |
| 2025-10-24 17:34:09 | <tomsmeding> | My current codebase has lists, and I have to mentally reverse all the time. I did this because I came from a codebase that had a custom data type, and the notation was ugly and verbose |
| 2025-10-24 17:34:24 | <tomsmeding> | I want both >.< |
| 2025-10-24 17:34:45 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 244 seconds) |
| 2025-10-24 17:38:09 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Read error: Connection reset by peer) |
| 2025-10-24 17:42:19 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2025-10-24 17:44:55 | × | Square2 quits (~Square@user/square) (Ping timeout: 246 seconds) |
| 2025-10-24 17:45:27 | × | trickard quits (~trickard@cpe-52-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-24 17:45:41 | → | trickard_ joins (~trickard@cpe-52-98-47-163.wireline.com.au) |
| 2025-10-24 17:49:00 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 2025-10-24 17:49:22 | × | juri_ quits (~juri@implicitcad.org) (Ping timeout: 260 seconds) |
| 2025-10-24 17:50:53 | → | juri_ joins (~juri@implicitcad.org) |
| 2025-10-24 17:59:47 | × | trickard_ quits (~trickard@cpe-52-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-24 18:00:01 | → | trickard_ joins (~trickard@cpe-52-98-47-163.wireline.com.au) |
| 2025-10-24 18:00:33 | → | karenw joins (~karenw@user/karenw) |
| 2025-10-24 18:06:11 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2025-10-24 18:07:50 | → | eron joins (~eron@143.0.15.19) |
| 2025-10-24 18:10:20 | × | ystael quits (~ystael@user/ystael) (Quit: Lost terminal) |
| 2025-10-24 18:16:51 | <EvanR> | yeah I will go with the nice syntax and metally reverse everything |
| 2025-10-24 18:20:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-10-24 18:20:23 | → | haltingsolver joins (~cmo@2604:3d09:207f:8000:d250:ea0c:366a:6e73) |
| 2025-10-24 18:20:32 | × | eron quits (~eron@143.0.15.19) (Quit: Client closed) |
| 2025-10-24 18:20:55 | × | Googulator71 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 18:21:09 | → | Googulator71 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 18:22:13 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 2025-10-24 18:22:58 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 2025-10-24 18:25:26 | × | Pozyomka quits (~pyon@user/pyon) (Ping timeout: 256 seconds) |
| 2025-10-24 18:27:12 | → | Pozyomka joins (~pyon@user/pyon) |
| 2025-10-24 18:30:55 | → | LainIwakura19 joins (~LainIwaku@user/LainIwakura) |
| 2025-10-24 18:31:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-24 18:31:15 | × | LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 250 seconds) |
| 2025-10-24 18:35:25 | → | LainIwakura joins (~LainIwaku@user/LainIwakura) |
| 2025-10-24 18:36:23 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-10-24 18:39:27 | × | qqe quits (~qqq@185.54.23.200) (Remote host closed the connection) |
| 2025-10-24 18:39:29 | × | LainIwakura19 quits (~LainIwaku@user/LainIwakura) (Ping timeout: 250 seconds) |
| 2025-10-24 18:45:44 | <monochrom> | For that kind of questions, usually we assume that there is no bottom, all functions/values involved are total. |
| 2025-10-24 18:46:08 | <monochrom> | (If the question intended to include bottom, it would not ask about = in the first place.) |
| 2025-10-24 18:46:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-24 18:47:54 | → | Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2025-10-24 18:52:02 | <tomsmeding> | EvanR: metally? |
| 2025-10-24 18:54:47 | <EvanR> | 🤘 |
| 2025-10-24 19:00:33 | → | rvalue- joins (~rvalue@about/hackers/rvalue) |
| 2025-10-24 19:01:39 | × | rvalue quits (~rvalue@about/hackers/rvalue) (Ping timeout: 252 seconds) |
| 2025-10-24 19:06:09 | rvalue- | is now known as rvalue |
| 2025-10-24 19:12:35 | × | Googulator71 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 19:12:51 | → | Googulator71 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 19:20:00 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-10-24 19:21:05 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 2025-10-24 19:26:19 | trickard_ | is now known as trickard |
| 2025-10-24 19:28:46 | → | jespada joins (~jespada@2800:a4:225c:5f00:301a:4a31:d5e6:2c05) |
| 2025-10-24 19:30:18 | × | fgidim quits (~lei@user/fgarcia) (Quit: Remote host closed the connection) |
| 2025-10-24 19:32:37 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 255 seconds) |
| 2025-10-24 19:33:50 | → | Tuplanolla joins (~Tuplanoll@91-159-187-167.elisa-laajakaista.fi) |
| 2025-10-24 19:35:25 | → | Achylles joins (~Achylles@45.182.57.47) |
| 2025-10-24 19:35:39 | × | Googulator71 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 19:35:46 | → | Googulator65 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 19:36:52 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2025-10-24 19:41:10 | × | target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 255 seconds) |
| 2025-10-24 19:42:13 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2025-10-24 19:43:58 | × | Achylles quits (~Achylles@45.182.57.47) (Remote host closed the connection) |
| 2025-10-24 19:44:16 | → | Achylles joins (~Achylles@45.182.57.47) |
| 2025-10-24 19:45:25 | × | jespada quits (~jespada@2800:a4:225c:5f00:301a:4a31:d5e6:2c05) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-10-24 19:49:04 | → | yauhsien joins (~Yau-Hsien@36-229-172-92.dynamic-ip.hinet.net) |
| 2025-10-24 19:50:21 | × | Achylles quits (~Achylles@45.182.57.47) (Remote host closed the connection) |
| 2025-10-24 19:51:02 | × | yauhsien quits (~Yau-Hsien@36-229-172-92.dynamic-ip.hinet.net) (Read error: Connection reset by peer) |
| 2025-10-24 19:51:19 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2025-10-24 19:51:37 | → | yauhsien joins (~Yau-Hsien@36-229-172-92.dynamic-ip.hinet.net) |
| 2025-10-24 19:55:33 | × | synchromesh quits (~john@2406:5a00:2412:2c00:443f:a42a:4395:130b) (Read error: Connection reset by peer) |
| 2025-10-24 19:56:57 | → | synchromesh joins (~john@2406:5a00:2412:2c00:443f:a42a:4395:130b) |
| 2025-10-24 19:59:43 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 2025-10-24 20:04:35 | × | td_ quits (~td@2001:9e8:19e0:2a00:334f:6dc4:3cb7:9653) (Ping timeout: 244 seconds) |
| 2025-10-24 20:05:04 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 2025-10-24 20:06:37 | → | td_ joins (~td@i53870931.versanet.de) |
| 2025-10-24 20:07:03 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-10-24 20:23:56 | × | yauhsien quits (~Yau-Hsien@36-229-172-92.dynamic-ip.hinet.net) (Quit: Leaving) |
| 2025-10-24 20:24:26 | × | haltingsolver quits (~cmo@2604:3d09:207f:8000:d250:ea0c:366a:6e73) (Ping timeout: 256 seconds) |
| 2025-10-24 20:25:38 | → | Googulator16 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 20:25:49 | × | Googulator65 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 20:27:37 | × | Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 264 seconds) |
| 2025-10-24 20:34:37 | → | Frostillicus joins (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2025-10-24 20:35:46 | → | Googulator52 joins (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) |
| 2025-10-24 20:36:14 | × | Googulator16 quits (~Googulato@2a01-036d-0106-03fa-d161-d36f-e0e5-1b0a.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-24 20:38:21 | → | trickard___ joins (~trickard@cpe-51-98-47-163.wireline.com.au) |
| 2025-10-24 20:39:13 | × | trickard quits (~trickard@cpe-52-98-47-163.wireline.com.au) (Ping timeout: 255 seconds) |
| 2025-10-24 20:42:18 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 252 seconds) |
All times are in UTC.