Logs on 2024-02-04 (liberachat/#haskell)
| 00:03:18 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 256 seconds) |
| 00:06:42 | × | mhatta_ quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.8.2+deb4+b2 - https://znc.in) |
| 00:07:56 | × | beka_ quits (~beka@207.53.253.162) (Remote host closed the connection) |
| 00:09:05 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 00:13:49 | → | rvalue joins (~rvalue@user/rvalue) |
| 00:17:15 | → | vitorg joins (~vitorg@2804:d55:7604:3000:fc0e:3448:351e:7502) |
| 00:17:59 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 264 seconds) |
| 00:28:32 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:6056:3fbc:d316:a2c5) |
| 00:30:48 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:6056:3fbc:d316:a2c5) (Client Quit) |
| 00:33:42 | → | newsham joins (~newsham@2603-800c-2c01-6825-0457-4a1a-39c4-b53d.res6.spectrum.com) |
| 00:37:14 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:39:12 | × | masterbuilder quits (~quassel@user/masterbuilder) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 00:40:57 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 00:50:34 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 01:02:14 | → | pallas joins (~pallas@154.3.39.96) |
| 01:04:08 | × | pallas quits (~pallas@154.3.39.96) (Client Quit) |
| 01:05:51 | → | szkl joins (uid110435@2a03:5180:f:5::1:af63) |
| 01:14:16 | → | TonyStone joins (~TonyStone@074-076-057-186.res.spectrum.com) |
| 01:25:02 | × | TonyStone quits (~TonyStone@074-076-057-186.res.spectrum.com) (Quit: Leaving) |
| 01:39:47 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 01:39:56 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 255 seconds) |
| 01:43:52 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 01:44:42 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 01:45:48 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 01:47:35 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 01:48:14 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 01:49:22 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 01:50:04 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 01:50:38 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 01:53:20 | → | iightbet joins (~kekbazz@user/kekbazz) |
| 01:58:22 | → | Achylles_ joins (~Achylles_@45.182.57.74) |
| 02:01:04 | × | Achylles quits (~Achylles_@45.182.57.55) (Ping timeout: 276 seconds) |
| 02:02:09 | → | bilegeek joins (~bilegeek@2600:1008:b069:80f:da49:c6c1:4159:ddf9) |
| 02:05:42 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 02:06:24 | × | Achylles_ quits (~Achylles_@45.182.57.74) (Read error: Connection reset by peer) |
| 02:20:27 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 02:24:50 | × | Tuplanolla quits (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 02:27:11 | × | otto_s quits (~user@p4ff2717e.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 02:28:54 | → | otto_s joins (~user@p4ff27bd5.dip0.t-ipconnect.de) |
| 02:29:49 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 02:39:03 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 03:05:03 | × | op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 03:05:32 | → | op_4 joins (~tslil@user/op-4/x-9116473) |
| 03:14:56 | × | szkl quits (uid110435@2a03:5180:f:5::1:af63) (Quit: Connection closed for inactivity) |
| 03:37:01 | × | newsham quits (~newsham@2603-800c-2c01-6825-0457-4a1a-39c4-b53d.res6.spectrum.com) (Quit: Client closed) |
| 03:41:58 | × | td_ quits (~td@i53870905.versanet.de) (Ping timeout: 264 seconds) |
| 03:43:00 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 03:43:16 | → | td_ joins (~td@i5387090F.versanet.de) |
| 03:44:56 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 03:51:25 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 03:53:23 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 04:05:18 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:08:13 | × | JordiGH quits (~jordi@user/jordigh) (Ping timeout: 260 seconds) |
| 04:09:31 | → | igemnace joins (~ian@user/igemnace) |
| 04:10:21 | → | JordiGH joins (~jordi@user/jordigh) |
| 04:10:29 | × | JordiGH quits (~jordi@user/jordigh) (Remote host closed the connection) |
| 04:10:48 | → | JordiGH joins (~jordi@user/jordigh) |
| 04:14:02 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 04:20:48 | → | newsham joins (~newsham@2603-800c-2c01-6825-0457-4a1a-39c4-b53d.res6.spectrum.com) |
| 04:21:58 | × | Joao[3] quits (~Joao003@190.108.108.40) (Read error: Connection reset by peer) |
| 04:42:37 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 04:46:39 | → | aforemny_ joins (~aforemny@2001:9e8:6cdc:8000:635d:2469:7926:7e65) |
| 04:46:53 | × | aforemny quits (~aforemny@2001:9e8:6cf8:3600:3a73:5278:af3b:a076) (Ping timeout: 240 seconds) |
| 04:54:30 | × | bilegeek quits (~bilegeek@2600:1008:b069:80f:da49:c6c1:4159:ddf9) (Quit: Leaving) |
| 04:59:53 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 05:06:42 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 05:12:36 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 05:23:10 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 05:23:17 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 240 seconds) |
| 05:28:29 | → | poscat joins (~poscat@user/poscat) |
| 05:30:48 | → | igemnace joins (~ian@user/igemnace) |
| 05:32:14 | → | bilegeek joins (~bilegeek@2600:1008:b069:80f:da49:c6c1:4159:ddf9) |
| 05:40:35 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 05:46:15 | → | mei joins (~mei@user/mei) |
| 05:52:22 | × | newsham quits (~newsham@2603-800c-2c01-6825-0457-4a1a-39c4-b53d.res6.spectrum.com) (Quit: Client closed) |
| 05:55:07 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 06:02:22 | × | mulk quits (~mulk@pd9514187.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 06:04:07 | → | mulk joins (~mulk@p5b2dc663.dip0.t-ipconnect.de) |
| 06:10:40 | → | mobivme joins (~mobivme@130.105.162.60) |
| 06:18:29 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 06:23:00 | → | michalz joins (~michalz@185.246.207.201) |
| 06:26:30 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 06:31:57 | × | czy` quits (~user@114.226.59.181) (Remote host closed the connection) |
| 06:32:09 | × | JordiGH quits (~jordi@user/jordigh) (Ping timeout: 268 seconds) |
| 06:52:13 | × | michalz quits (~michalz@185.246.207.201) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:55:06 | → | michalz joins (~michalz@185.246.207.203) |
| 07:11:02 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 07:15:43 | × | iightbet quits (~kekbazz@user/kekbazz) (Quit: Leaving) |
| 07:30:49 | → | Square joins (~Square@user/square) |
| 07:39:25 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 07:41:13 | → | gmg joins (~user@user/gehmehgeh) |
| 07:45:54 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 07:46:50 | → | gmg joins (~user@user/gehmehgeh) |
| 08:00:07 | × | tt1231 quits (~tt123@2603-6010-8700-4a81-219f-50d3-618a-a6ee.res6.spectrum.com) (Quit: The Lounge - https://thelounge.chat) |
| 08:02:06 | → | tt1231 joins (~tt123@2603:6010:8700:4a81:219f:50d3:618a:a6ee) |
| 08:06:17 | → | sroso joins (~sroso@user/SrOso) |
| 08:17:14 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 08:18:27 | → | mreh joins (~matthew@host86-160-168-81.range86-160.btcentralplus.com) |
| 08:20:53 | × | Hooloovoo quits (~Hooloovoo@hax0rbana.org) (Ping timeout: 240 seconds) |
| 08:24:59 | → | Hooloovoo joins (~Hooloovoo@hax0rbana.org) |
| 08:27:09 | × | ph88 quits (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 08:35:25 | → | acidjnk_new joins (~acidjnk@p200300d6e737e71815e0d25cbf100a78.dip0.t-ipconnect.de) |
| 08:36:03 | → | Axman6 joins (~Axman6@user/axman6) |
| 08:39:22 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 08:50:05 | → | pallas joins (~pallas@154.3.39.96) |
| 08:50:08 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:04:36 | [exa] | discovers cabal-fmt |
| 09:04:40 | <[exa]> | \o/ |
| 09:19:14 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:24:52 | → | lambdaman joins (~textual@d172-218-204-71.bchsia.telus.net) |
| 09:30:25 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 09:32:56 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 09:34:00 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 09:34:14 | × | lambdaman quits (~textual@d172-218-204-71.bchsia.telus.net) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 09:36:06 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:36:21 | → | gentauro joins (~gentauro@user/gentauro) |
| 09:48:45 | → | lambdaman joins (~textual@172.218.204.71) |
| 09:51:22 | → | mastarija joins (~mastarija@9-181.dsl.iskon.hr) |
| 09:55:02 | <mastarija> | Does anyone have experience with nix flakes and freeglut / Gloss package? I'm loosing my mind. I had it working but haven't worked on my project in a while. In the meantime, I've upgraded and garbage collected my NixOS, and yesterday I've tried working on my project and now I have some cryptic freeglut error. |
| 09:55:24 | <mastarija> | The error happens when I try to run the graphic program. |
| 09:55:53 | <mastarija> | It compiles / builds and links fine. It's just when I try to run it that it reports the free glut message. |
| 09:56:03 | <mastarija> | I'll post the error and my nix flake in a sec. |
| 09:56:15 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 09:57:51 | <mastarija> | https://paste.tomsmeding.com/xQPdlqRE |
| 10:05:23 | → | laxmik joins (~laxmik@2a01:c22:8918:9900:b826:25a9:c9b5:46d) |
| 10:06:43 | laxmik | is now known as michals |
| 10:08:33 | × | michals quits (~laxmik@2a01:c22:8918:9900:b826:25a9:c9b5:46d) (Client Quit) |
| 10:14:02 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 10:14:47 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 10:20:08 | × | lambdaman quits (~textual@172.218.204.71) (Read error: Connection reset by peer) |
| 10:28:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:32:28 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 10:35:13 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 256 seconds) |
| 10:39:14 | × | mreh quits (~matthew@host86-160-168-81.range86-160.btcentralplus.com) (Ping timeout: 260 seconds) |
| 10:40:04 | ← | joel135 parts (sid136450@id-136450.hampstead.irccloud.com) () |
| 10:46:17 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 10:48:01 | → | califax joins (~califax@user/califx) |
| 10:53:10 | → | Tuplanolla joins (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi) |
| 10:56:08 | × | bilegeek quits (~bilegeek@2600:1008:b069:80f:da49:c6c1:4159:ddf9) (Quit: Leaving) |
| 10:57:55 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 10:59:21 | → | Guest14 joins (~Guest14@103.141.217.63) |
| 10:59:43 | × | Guest14 quits (~Guest14@103.141.217.63) (Client Quit) |
| 11:03:03 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 11:12:31 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 11:19:26 | → | mmhat joins (~mmh@p200300f1c73bf47eee086bfffe095315.dip0.t-ipconnect.de) |
| 11:20:11 | × | mmhat quits (~mmh@p200300f1c73bf47eee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 11:24:19 | → | Achylles_ joins (~Achylles_@45.182.57.53) |
| 11:26:36 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 11:27:58 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Client Quit) |
| 11:34:32 | → | mreh joins (~matthew@host86-160-168-81.range86-160.btcentralplus.com) |
| 11:44:22 | × | mastarija quits (~mastarija@9-181.dsl.iskon.hr) (Quit: Client closed) |
| 11:50:50 | → | ht_ joins (~Thunderbi@194.110.115.42) |
| 11:52:37 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Ping timeout: 264 seconds) |
| 11:52:37 | ht_ | is now known as _ht |
| 11:53:44 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 12:01:31 | × | mrmr15533 quits (~mrmr@user/mrmr) (Quit: Bye, See ya later!) |
| 12:03:10 | <Tisoxin> | Hm |
| 12:03:35 | <Tisoxin> | My previously working package using gloss returns the same error: freeglut (hart): ERROR: Internal error <FBConfig with necessary capabilities not found> in function fgOpenWindow |
| 12:05:20 | <Tisoxin> | Probabaly a driver mismatch with opengl |
| 12:08:13 | → | mrmr155334 joins (~mrmr@user/mrmr) |
| 12:10:04 | → | kffiatek joins (~Miranda@v254-138-142.vivaldiego.wroclaw.pl) |
| 12:10:33 | <Tisoxin> | https://paste.tomsmeding.com/NGjXWjR1 |
| 12:16:40 | → | rosco joins (~rosco@175.136.156.77) |
| 12:17:58 | × | kffiatek quits (~Miranda@v254-138-142.vivaldiego.wroclaw.pl) (Quit: Miranda NG! Smaller, Faster, Easier. https://miranda-ng.org/) |
| 12:27:02 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 255 seconds) |
| 12:27:37 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 12:31:56 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 12:32:21 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 12:34:12 | <[exa]> | Tisoxin: can you `ltrace` it? |
| 12:34:50 | <[exa]> | Tisoxin: also what does `glxinfo` say? |
| 12:35:43 | <[exa]> | btw looks like mastarija had essentially the same problem right before you, might be the case that something got borked by accident |
| 12:36:34 | <[exa]> | tbh it might be worth to try rolling back freeglut and gloss by one version and see what happens. :D |
| 12:37:20 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 12:37:55 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 12:40:06 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 12:41:13 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 12:45:30 | → | igemnace joins (~ian@user/igemnace) |
| 12:48:58 | <Tisoxin> | [exa] I wrote my messages as a reply to mastarija |
| 12:49:14 | <Tisoxin> | I didn't see that they aren't in the chat anymore |
| 12:49:42 | <Tisoxin> | But whatever ¯\_(ツ)_/¯ |
| 12:59:14 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 13:04:36 | → | Joao[3] joins (~Joao003@190.108.108.40) |
| 13:09:44 | × | Achylles_ quits (~Achylles_@45.182.57.53) (Remote host closed the connection) |
| 13:10:10 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 13:10:11 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 13:14:02 | <Joao[3]> | fun fact: there are more people on this channel than ##math :) |
| 13:27:49 | → | igemnace joins (~ian@user/igemnace) |
| 13:43:35 | × | Achylles quits (~Achylles_@45.182.57.53) (Ping timeout: 252 seconds) |
| 13:43:37 | × | vitorg quits (~vitorg@2804:d55:7604:3000:fc0e:3448:351e:7502) (Ping timeout: 264 seconds) |
| 13:44:18 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 13:44:35 | → | average joins (uid473595@user/average) |
| 13:44:40 | → | vitorg joins (~vitorg@189.28.157.44) |
| 13:45:11 | → | mobounce joins (~mobivme@104.28.194.104) |
| 13:45:12 | × | causal quits (~eric@50.35.85.7) (Quit: WeeChat 4.1.1) |
| 13:46:11 | × | mobivme quits (~mobivme@130.105.162.60) (Ping timeout: 264 seconds) |
| 13:51:19 | × | Achylles quits (~Achylles_@45.182.57.53) (Remote host closed the connection) |
| 13:57:05 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 13:57:31 | × | mreh quits (~matthew@host86-160-168-81.range86-160.btcentralplus.com) (Ping timeout: 256 seconds) |
| 14:07:05 | → | pavonia joins (~user@user/siracusa) |
| 14:10:53 | × | rosco quits (~rosco@175.136.156.77) (Read error: Connection reset by peer) |
| 14:15:09 | → | rosco joins (rosco@gateway/vpn/airvpn/rosco) |
| 14:20:34 | zer0bitz_ | is now known as zer0bitz |
| 14:29:49 | × | trev quits (~trev@109-252-35-136.nat.spd-mgts.ru) (Ping timeout: 264 seconds) |
| 14:31:36 | → | trev joins (~trev@109-252-33-130.nat.spd-mgts.ru) |
| 14:33:33 | × | trev quits (~trev@109-252-33-130.nat.spd-mgts.ru) (Client Quit) |
| 14:33:36 | → | substance_ joins (~substance@176.254.244.83) |
| 14:33:49 | → | trev joins (~trev@109-252-33-130.nat.spd-mgts.ru) |
| 14:37:03 | × | trev quits (~trev@109-252-33-130.nat.spd-mgts.ru) (Changing host) |
| 14:37:03 | → | trev joins (~trev@user/trev) |
| 14:37:11 | × | substance quits (~substance@176.254.244.83) (Ping timeout: 256 seconds) |
| 14:41:08 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 14:44:44 | → | ht_ joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 14:46:17 | × | _ht quits (~Thunderbi@194.110.115.42) (Ping timeout: 252 seconds) |
| 14:46:18 | ht_ | is now known as _ht |
| 14:53:13 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:54:25 | <[exa]> | Tisoxin: aaah ok :D |
| 14:56:07 | × | rembo10 quits (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 14:58:14 | → | rembo10 joins (~rembo10@main.remulis.com) |
| 15:04:37 | × | remmie quits (ianremsen@tilde.team) (Ping timeout: 264 seconds) |
| 15:20:59 | × | kimiamania4648 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 15:21:47 | → | kimiamania4648 joins (~65804703@user/kimiamania) |
| 15:22:57 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 15:23:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:26:41 | → | zetef joins (~quassel@95.77.17.251) |
| 15:29:08 | → | mreh joins (~matthew@host86-160-168-81.range86-160.btcentralplus.com) |
| 15:35:23 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 15:36:32 | → | euleritian joins (~euleritia@dynamic-176-006-201-083.176.6.pool.telefonica.de) |
| 15:41:08 | × | euleritian quits (~euleritia@dynamic-176-006-201-083.176.6.pool.telefonica.de) (Ping timeout: 256 seconds) |
| 15:41:35 | → | euleritian joins (~euleritia@dynamic-176-007-156-064.176.7.pool.telefonica.de) |
| 15:44:37 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 15:49:33 | → | rscastilho2024 joins (rscastilho@189.61.140.215) |
| 15:49:47 | × | zetef quits (~quassel@95.77.17.251) (Remote host closed the connection) |
| 15:55:20 | × | swistak- quits (~swistak@185.21.216.141) (Remote host closed the connection) |
| 15:56:59 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:02:06 | × | euleritian quits (~euleritia@dynamic-176-007-156-064.176.7.pool.telefonica.de) (Ping timeout: 256 seconds) |
| 16:03:22 | → | euleritian joins (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) |
| 16:11:22 | → | Pixi` joins (~Pixi@user/pixi) |
| 16:11:41 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 256 seconds) |
| 16:14:01 | → | remmie joins (ianremsen@tilde.team) |
| 16:14:31 | → | tremon joins (~tremon@83.80.159.219) |
| 16:15:36 | × | rscastilho2024 quits (rscastilho@189.61.140.215) (Remote host closed the connection) |
| 16:20:36 | → | rscastilho2024 joins (~rscastilh@189.61.140.215) |
| 16:25:10 | × | phma quits (~phma@host-67-44-208-155.hnremote.net) (Read error: Connection reset by peer) |
| 16:26:03 | → | phma joins (phma@2001:5b0:215d:dac8:5473:cd1c:1142:a768) |
| 16:28:29 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:29:58 | → | alexherbo2 joins (~alexherbo@2a02-8440-3441-8d47-edf0-ae93-9bd1-cf3e.rev.sfr.net) |
| 16:30:32 | → | JordiGH joins (~jordi@user/jordigh) |
| 16:31:24 | × | euleritian quits (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:31:42 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:34:09 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:34:50 | → | euleritian joins (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) |
| 16:35:12 | × | euleritian quits (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:35:54 | → | euleritian joins (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) |
| 16:41:26 | × | euleritian quits (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:41:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:43:28 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 16:46:30 | × | alexherbo2 quits (~alexherbo@2a02-8440-3441-8d47-edf0-ae93-9bd1-cf3e.rev.sfr.net) (Ping timeout: 250 seconds) |
| 16:50:43 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 16:53:57 | → | alexherbo2 joins (~alexherbo@2a02-8440-3441-8d47-edf0-ae93-9bd1-cf3e.rev.sfr.net) |
| 16:59:40 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 17:00:32 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:09:30 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 17:09:37 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:10:05 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 240 seconds) |
| 17:17:06 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 17:20:30 | → | rvalue joins (~rvalue@user/rvalue) |
| 17:27:18 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:33:02 | × | alexherbo2 quits (~alexherbo@2a02-8440-3441-8d47-edf0-ae93-9bd1-cf3e.rev.sfr.net) (Remote host closed the connection) |
| 17:33:39 | → | alexherbo2 joins (~alexherbo@2a02-8440-3441-8d47-e119-32c2-7052-7b61.rev.sfr.net) |
| 17:39:00 | → | puke joins (~puke@user/puke) |
| 17:40:05 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 17:41:11 | × | Achylles quits (~Achylles_@45.182.57.53) (Ping timeout: 252 seconds) |
| 17:43:27 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:44:22 | × | average quits (uid473595@user/average) (Quit: Connection closed for inactivity) |
| 17:45:18 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 17:45:38 | → | puke joins (~puke@user/puke) |
| 17:49:02 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 17:51:01 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 17:53:00 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:58:30 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 17:58:43 | → | euleritian joins (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) |
| 18:02:33 | × | euleritian quits (~euleritia@dynamic-176-000-139-121.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:03:59 | × | puke quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 18:03:59 | → | pyooque joins (~puke@user/puke) |
| 18:03:59 | pyooque | is now known as puke |
| 18:04:04 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:06:15 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 18:07:59 | × | mreh quits (~matthew@host86-160-168-81.range86-160.btcentralplus.com) (Ping timeout: 256 seconds) |
| 18:08:33 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 18:08:36 | → | califax joins (~califax@user/califx) |
| 18:08:59 | × | Buggys quits (Buggys@Buggy.shelltalk.net) (Ping timeout: 260 seconds) |
| 18:09:34 | <haskellbridge> | 15<Jade> I don't know if I'm just being stupid, but is there no way to lift a producing function of the form `(a -> b) -> c` into a monad? |
| 18:09:34 | <haskellbridge> | 15<Jade> i.e. `((a -> b) -> c) -> (a -> m b) -> m c` |
| 18:10:29 | <haskellbridge> | 15<Jade> specifically I have a predicate `a -> IO Bool` and I want to `partition` by that, but I don't want to just copy the definition of `partition` |
| 18:11:26 | <ncf> | there isn't; you need a monadic version of partition (search for partitionM) |
| 18:12:20 | <haskellbridge> | 15<Jade> yeah I saw those in a few different packages, but they just copy the definition of `partition` and monadify them |
| 18:13:29 | <haskellbridge> | 15<Jade> which ... seems icky? |
| 18:13:55 | × | mobounce quits (~mobivme@104.28.194.104) (Changing host) |
| 18:13:55 | → | mobounce joins (~mobivme@user/mobivme) |
| 18:13:56 | <monochrom> | Roughly speaking, it would require converting (a -> IO b) to (a -> b), which can't be done. |
| 18:14:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:14:13 | <haskellbridge> | 15<Jade> yeah that makes sense |
| 18:14:33 | <ncf> | well, that's what you have to do. alternatively, if m supports an "unKleisli" operation (a -> m b) -> m (a -> b) then you could use that and then apply your function inside m |
| 18:14:39 | <haskellbridge> | 15<Jade> (unsafePerformIO is crying in the corner) |
| 18:14:46 | <ncf> | you can probably achieve that in IO with some unsafe stuff |
| 18:15:24 | <haskellbridge> | 15<Jade> I think I'll cave in to the primitive method of copying the definition from ghc internals |
| 18:16:07 | <monochrom> | Ha I didn't think of the weaker requirement m (a -> b). Then again not quite for IO either. |
| 18:27:26 | → | Pixi__ joins (~Pixi@user/pixi) |
| 18:27:50 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 18:30:41 | × | Pixi` quits (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 18:32:52 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 18:41:32 | → | lambdaman joins (~textual@d172-218-204-71.bchsia.telus.net) |
| 18:50:47 | × | lambdaman quits (~textual@d172-218-204-71.bchsia.telus.net) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 18:53:16 | → | lambdaman joins (~textual@d172-218-204-71.bchsia.telus.net) |
| 18:57:18 | × | lambdaman quits (~textual@d172-218-204-71.bchsia.telus.net) (Client Quit) |
| 19:00:12 | × | pallas quits (~pallas@154.3.39.96) (Quit: Connection closed) |
| 19:02:33 | → | danza joins (~danza@151.47.37.212) |
| 19:02:52 | × | JordiGH quits (~jordi@user/jordigh) (Ping timeout: 276 seconds) |
| 19:05:01 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 19:09:55 | × | Joao[3] quits (~Joao003@190.108.108.40) (Read error: Connection reset by peer) |
| 19:10:12 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 19:12:20 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 19:14:14 | × | danza quits (~danza@151.47.37.212) (Quit: Leaving) |
| 19:17:21 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 19:18:32 | → | lambdaman joins (~textual@172.218.204.71) |
| 19:22:00 | × | rosco quits (rosco@gateway/vpn/airvpn/rosco) (Quit: Lost terminal) |
| 19:26:40 | → | mreh joins (~matthew@host86-160-168-81.range86-160.btcentralplus.com) |
| 19:27:39 | → | JordiGH joins (~jordi@user/jordigh) |
| 19:35:41 | × | Goodbye_Vincent quits (cyvahl@freakshells.net) (Ping timeout: 240 seconds) |
| 19:36:20 | → | Goodbye_Vincent joins (cyvahl@freakshells.net) |
| 19:36:23 | × | Square quits (~Square@user/square) (Ping timeout: 256 seconds) |
| 19:38:31 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 256 seconds) |
| 19:41:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:42:11 | × | Goodbye_Vincent quits (cyvahl@freakshells.net) (Ping timeout: 252 seconds) |
| 19:45:17 | → | Goodbye_Vincent joins (cyvahl@freakshells.net) |
| 19:45:23 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 19:52:05 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 252 seconds) |
| 19:52:43 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 19:57:25 | × | Goodbye_Vincent quits (cyvahl@freakshells.net) (Ping timeout: 264 seconds) |
| 19:58:51 | → | tomku joins (~tomku@user/tomku) |
| 20:00:50 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 20:02:02 | × | Achylles quits (~Achylles_@45.182.57.53) (Read error: Connection reset by peer) |
| 20:02:21 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 20:03:10 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:03:32 | × | Achylles quits (~Achylles_@45.182.57.53) (Read error: Connection reset by peer) |
| 20:03:41 | × | rscastilho2024 quits (~rscastilh@189.61.140.215) (Ping timeout: 268 seconds) |
| 20:03:52 | → | Achylles joins (~Achylles_@45.182.57.53) |
| 20:04:37 | × | todi quits (~todi@p5dca5fa8.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 20:05:17 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 20:09:30 | → | rscastilho2024 joins (~rscastilh@189.61.140.215) |
| 20:16:09 | → | todi joins (~todi@p5dca5fa8.dip0.t-ipconnect.de) |
| 20:19:29 | → | aforemny joins (~aforemny@89.245.22.249) |
| 20:19:31 | × | aforemny_ quits (~aforemny@2001:9e8:6cdc:8000:635d:2469:7926:7e65) (Ping timeout: 255 seconds) |
| 20:26:04 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 20:32:38 | → | Goodbye_Vincent joins (cyvahl@51.77.77.10) |
| 20:37:15 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:42:17 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:42:25 | × | Goodbye_Vincent quits (cyvahl@51.77.77.10) (Quit: Ping timeout (120 seconds)) |
| 20:56:04 | × | rscastilho2024 quits (~rscastilh@189.61.140.215) (Remote host closed the connection) |
| 21:11:21 | × | Pixi__ quits (~Pixi@user/pixi) (Quit: Leaving) |
| 21:12:56 | <haskellbridge> | 15<Jade> is it more idiomatic to have `Maybe (NonEmpty a)` or just `[a]` but use `[]` as the 'Nothing'? |
| 21:13:37 | → | Goodbye_Vincent joins (cyvahl@freakshells.net) |
| 21:13:48 | → | Joao[3] joins (~Joao003@190.108.108.40) |
| 21:16:41 | → | Pixi joins (~Pixi@user/pixi) |
| 21:16:50 | × | lambdaman quits (~textual@172.218.204.71) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 21:17:41 | <sshine> | I'd probably prefer [a] |
| 21:21:41 | × | Joao[3] quits (~Joao003@190.108.108.40) (Quit: Bye!) |
| 21:28:07 | <geekosaur> | unless there's some reason to distinguish [] from Nothing, yeh |
| 21:31:04 | × | JordiGH quits (~jordi@user/jordigh) (Ping timeout: 276 seconds) |
| 21:33:13 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 21:38:51 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:43:13 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:43:14 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 21:52:13 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 21:55:31 | → | lambdaman joins (~textual@d172-218-204-71.bchsia.telus.net) |
| 21:55:46 | × | mreh quits (~matthew@host86-160-168-81.range86-160.btcentralplus.com) (Ping timeout: 276 seconds) |
| 21:57:47 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 21:59:53 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:06:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 22:09:54 | → | jargon joins (~jargon@105.sub-174-205-230.myvzw.com) |
| 22:14:10 | → | JordiGH joins (~jordi@user/jordigh) |
| 22:20:56 | × | lambdaman quits (~textual@d172-218-204-71.bchsia.telus.net) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 22:21:44 | → | LukeHoersten joins (~LukeHoers@user/lukehoersten) |
| 22:23:04 | → | masterbuilder joins (~quassel@user/masterbuilder) |
| 22:29:48 | → | fansly joins (~fansly@103.3.221.233) |
| 22:30:00 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: Textual IRC Client: www.textualapp.com) |
| 22:30:59 | × | JordiGH quits (~jordi@user/jordigh) (Remote host closed the connection) |
| 22:31:21 | → | JordiGH joins (~jordi@user/jordigh) |
| 22:31:56 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:36:18 | × | michalz quits (~michalz@185.246.207.203) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:37:41 | × | alexherbo2 quits (~alexherbo@2a02-8440-3441-8d47-e119-32c2-7052-7b61.rev.sfr.net) (Remote host closed the connection) |
| 22:38:29 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.2.1) |
| 22:39:22 | × | JordiGH quits (~jordi@user/jordigh) (Ping timeout: 246 seconds) |
| 22:42:07 | → | a51 joins (a51@gateway/vpn/protonvpn/a51) |
| 22:55:17 | × | fansly quits (~fansly@103.3.221.233) (Read error: Connection reset by peer) |
| 23:00:21 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 23:06:21 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 23:08:07 | × | Goodbye_Vincent quits (cyvahl@freakshells.net) (Ping timeout: 260 seconds) |
| 23:09:44 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 23:12:21 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:12:49 | → | Goodbye_Vincent joins (cyvahl@freakshells.net) |
| 23:15:25 | × | acidjnk_new quits (~acidjnk@p200300d6e737e71815e0d25cbf100a78.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 23:21:44 | <haskellbridge> | 05<irregularsphere> (don't take this as professional advice) but I think `Maybe (NonEmpty a)` has concise safe functions like `>>= nonEmpty . init` |
| 23:23:04 | <haskellbridge> | 05<irregularsphere> ...or if that's the only benefit, then I'd prefer `[a]` i guess |
| 23:32:12 | × | potato44 quits (uid421314@id-421314.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 23:33:29 | <EvanR> | to spice things up consider Maybe (a, [a]) |
| 23:36:00 | <haskellbridge> | 05<irregularsphere> isn't `(a, [a])` just `NonEmpty a` but without the functions |
| 23:37:12 | <jackdk> | It's easier to pass `NonEmpty a` to consumers which don't want to consider empty lists, and that forces the emptiness check outwards in a convenient way |
| 23:37:48 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 23:39:16 | <haskellbridge> | 05<irregularsphere> ncf: if kleisli composition is `(>>=): Monad m => m a -> (a -> m b) -> m b`, shouldn't our theoretical `unKleisli` be `(m a -> m b) -> (a -> m b)` |
| 23:40:19 | × | mobounce quits (~mobivme@user/mobivme) (Ping timeout: 260 seconds) |
| 23:40:42 | <ncf> | well that's just (. pure) |
| 23:40:51 | <haskellbridge> | 05<irregularsphere> yea |
| 23:40:55 | <ncf> | but yeah, not a great name, i'm just parroting the agda codebase |
| 23:41:12 | <haskellbridge> | 05<irregularsphere> you said `-> m (a -> b)` though, I'm stressing on that |
| 23:41:28 | <ncf> | if i had to name it i'd name it distribute, or something (it should be some kind of distributive law for (->) over m) |
| 23:42:08 | <haskellbridge> | 05<irregularsphere> "(. pure)" yup |
| 23:43:10 | × | johnw quits (~johnw@69.62.242.138) (Ping timeout: 264 seconds) |
| 23:43:17 | → | johnw_ joins (~johnw@69.62.242.138) |
| 23:44:26 | → | fansly joins (~fansly@2001:448a:2010:476e:fcbe:e3e5:ceb0:7fbe) |
| 23:44:42 | × | johnw_ quits (~johnw@69.62.242.138) (Client Quit) |
| 23:46:55 | <jackdk> | I haven't been following closely but `m (a -> b) -> (m a -> m b)` is `(<*>)`, so would `(f a -> f b) -> f (a -> b)` be tied to some kind of coapplicative? (There's a remark in `Data.Distributive` that class `Distributive` uses `Functor` and not some kind of coapplicative because there are no non-trivial comonoids in standard Haskell, but maybe in other settings?) |
| 23:48:47 | <ncf> | that's not quite the type we're discussing |
| 23:49:13 | <jackdk> | ah, ok |
| 23:49:58 | <ncf> | your thing would be a closed monoidal functor, i think? |
| 23:50:22 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 23:50:33 | <jackdk> | something like that, but my cat-fu is too weak to be certain |
| 23:50:35 | → | son0p joins (~ff@186.121.12.53) |
| 23:51:48 | × | puke quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 23:52:08 | → | puke joins (~puke@user/puke) |
| 23:53:14 | → | JordiGH joins (~jordi@user/jordigh) |
| 23:56:32 | <ncf> | returning to unKleisli, one might cheekily name it "choice", because instantiating m with the propositional truncation monad yields the axiom of choice |
| 23:57:37 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 23:57:50 | <ncf> | "if for every a one can choose (in m) a b, then there is (in m) a function from a to b" |
All times are in UTC on 2024-02-04.