Logs on 2023-11-05 (liberachat/#haskell)
| 00:01:13 | × | falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 255 seconds) |
| 00:10:12 | × | target_i quits (~target_i@217.175.14.39) (Quit: leaving) |
| 00:18:44 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:19:04 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:24:22 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:24:50 | × | arahael quits (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Ping timeout: 255 seconds) |
| 00:25:07 | × | zetef quits (~quassel@2a02:2f00:5201:4b00:7fc8:6fbe:33d9:ba2a) (Ping timeout: 264 seconds) |
| 00:25:33 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:34:36 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:34:36 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:41:20 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:41:56 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:47:17 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:47:27 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:52:18 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 00:52:58 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 01:07:31 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 01:07:44 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 01:09:05 | Lord_of_Life_ | is now known as Lord_of_Life |
| 01:15:18 | → | berberman joins (~berberman@user/berberman) |
| 01:16:15 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 01:16:19 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 01:25:16 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 01:25:39 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:26:01 | × | Inst quits (~Inst@120.244.192.250) (Ping timeout: 240 seconds) |
| 01:28:09 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 01:28:19 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 01:30:33 | → | Inst joins (~Inst@120.244.192.250) |
| 01:48:43 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 01:48:54 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 01:59:24 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 01:59:43 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:00:17 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 02:01:02 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:02:59 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:03:13 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:05:35 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 02:07:01 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:07:06 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:11:27 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:11:53 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:17:01 | × | mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 02:17:07 | × | arjun quits (~arjun@user/arjun) (Ping timeout: 255 seconds) |
| 02:19:13 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:20:00 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:23:14 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:24:46 | × | otto_s quits (~user@p5de2f0ce.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 02:24:55 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:26:41 | → | otto_s joins (~user@p4ff27c21.dip0.t-ipconnect.de) |
| 02:28:18 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 02:29:11 | → | jargon joins (~jargon@184.101.69.217) |
| 02:29:47 | × | nyc quits (~nyc@user/nyc) (Read error: Connection reset by peer) |
| 02:30:52 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 02:31:59 | × | jargon quits (~jargon@184.101.69.217) (Remote host closed the connection) |
| 02:34:00 | → | arjun joins (~arjun@user/arjun) |
| 02:45:26 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 02:50:21 | <Inst> | btw, if Haskript were a thing, would traditional Haskellers complain? |
| 02:50:30 | <Inst> | where Haskript = |
| 02:50:31 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 02:51:11 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 02:51:12 | <Inst> | Community oriented toward building or wrapping libraries for Haskell scripting use, focused on ergonomics and simplicity, with the only concern for traditional Haskell architecture and values being once the script exceeds 500-1000 lines |
| 02:59:52 | × | qqq quits (~qqq@92.43.167.61) (Remote host closed the connection) |
| 03:03:55 | × | xff0x quits (~xff0x@ai101218.d.east.v6connect.net) (Ping timeout: 255 seconds) |
| 03:05:52 | → | xff0x joins (~xff0x@178.255.149.135) |
| 03:06:02 | → | tabemann joins (~tabemann@12.215.215.61) |
| 03:06:05 | <L29Ah> | so allow unsafePerformIO everywere and that's it? |
| 03:06:20 | <monochrom> | haha |
| 03:07:33 | <monochrom> | This is the problem with "grand visions" such as "ergonomics and simplicity". People have opposite definitions of them. |
| 03:08:19 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:08:20 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:08:29 | <monochrom> | There are people like me who actually consider, for example, unsafePerformIO to be unergonomic and unsimple, because it is so hard to get them to do the right thing. |
| 03:08:38 | <monochrom> | or at least so tricky. |
| 03:09:11 | × | Inst quits (~Inst@120.244.192.250) (Remote host closed the connection) |
| 03:09:28 | <L29Ah> | fair |
| 03:09:35 | → | Inst joins (~Inst@120.244.192.250) |
| 03:10:02 | <L29Ah> | Inst: can you show a representative example of Haskript? |
| 03:10:06 | <monochrom> | On Youtube I saw a programmer who converted from Java to APL. He would say that APL is more ergonomic and simpler. |
| 03:11:10 | <L29Ah> | it is, for things like programming contests |
| 03:11:42 | <L29Ah> | APL probably is the language that is tailored to the professional programming sport the most |
| 03:11:57 | <monochrom> | In fact, I bet it is a tautology that every language inventor believes that they invent their language to focus on ergonomics and simplicity. |
| 03:13:12 | <monochrom> | oh and productivity and power and expressivity and a dozen more grand vision buzzwords. |
| 03:14:30 | <monochrom> | Even COBOL fans get to claim "easy to debug because reads like English". That's another way to say ergonomic and simple. |
| 03:14:58 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 03:21:28 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 03:21:28 | × | xff0x quits (~xff0x@178.255.149.135) (Ping timeout: 255 seconds) |
| 03:23:19 | → | xff0x joins (~xff0x@2405:6580:b080:900:e3bc:44ff:b3f7:2dd5) |
| 03:24:34 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 03:25:21 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 03:27:16 | <Inst> | Haskript is just Haskell written unidiomatically, probably with lots of where clauses and IO, and maybe even with everything in main |
| 03:29:31 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 03:29:36 | <L29Ah> | re your question: haskellers complain about each others' non-idiomatic stuff all the time |
| 03:30:06 | <L29Ah> | for example i find lens unidiomatic |
| 03:30:30 | <L29Ah> | and use tabs exclusively for indentation |
| 03:30:55 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 03:31:34 | <L29Ah> | haskell is not really the language where there's a grand vision on how things get to get done |
| 03:32:26 | <Inst> | It's more that Haskell needs better library APIs for scripting |
| 03:32:44 | <L29Ah> | what APIs? |
| 03:33:00 | <L29Ah> | there are a few libraries for shell-script-like behavior |
| 03:33:12 | <Inst> | I know, Shelly and Turtle, no? |
| 03:33:23 | <Inst> | I just never found Aeson easy to use |
| 03:33:29 | L29Ah | doesn't remember |
| 03:33:31 | <Inst> | There are others, who've gotten to Chapter 27 of RWH |
| 03:33:40 | <Inst> | who have difficulty reading Haskell libraries |
| 03:33:49 | <L29Ah> | decided that zsh is good enough |
| 03:33:55 | <Inst> | setting up a Haskript ghetto for newbies, and picking them up for "real" Haskell once in a while, I think is a positive for the community |
| 03:35:32 | <L29Ah> | you may be interested in xmonad community |
| 03:35:33 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 03:40:07 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 03:40:22 | × | td_ quits (~td@i53870925.versanet.de) (Ping timeout: 258 seconds) |
| 03:42:17 | → | td_ joins (~td@i5387091C.versanet.de) |
| 03:48:21 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 03:50:08 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 03:53:19 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 03:57:28 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 04:00:39 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 04:12:19 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 04:13:34 | × | tabemann quits (~tabemann@12.215.215.61) (Remote host closed the connection) |
| 04:16:36 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 04:19:32 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 04:24:05 | → | tabemann joins (~tabemann@12.215.215.61) |
| 04:30:38 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 260 seconds) |
| 04:31:50 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 04:35:20 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 04:38:46 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 04:41:54 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 04:43:07 | × | xff0x quits (~xff0x@2405:6580:b080:900:e3bc:44ff:b3f7:2dd5) (Ping timeout: 264 seconds) |
| 04:44:52 | → | xff0x joins (~xff0x@ai101218.d.east.v6connect.net) |
| 04:46:42 | → | trev joins (~trev@user/trev) |
| 04:47:52 | × | aforemny quits (~aforemny@i59f516df.versanet.de) (Ping timeout: 255 seconds) |
| 04:48:08 | → | aforemny joins (~aforemny@2001:9e8:6cf3:8800:56a7:5281:8d04:8d56) |
| 04:51:35 | × | Ram-Z quits (Ram-Z@2a01:7e01::f03c:91ff:fe57:d2df) (Ping timeout: 240 seconds) |
| 04:53:53 | → | Ram-Z joins (~Ram-Z@li1814-254.members.linode.com) |
| 04:56:15 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:00:46 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:03:45 | <Inst> | L29Ah: |
| 05:03:50 | <Inst> | this I'm particularly embarrassed by |
| 05:03:51 | <Inst> | https://paste.tomsmeding.com/qacjVfxi |
| 05:04:06 | <Inst> | literally "everything in main" |
| 05:04:59 | <Inst> | also, too many operators |
| 05:05:23 | <Inst> | I sort of wish (<$) <*> (undefined :: a -> m a) were idiomatic, though |
| 05:05:44 | <Inst> | and someone pointed out theres' a space leak because of misuse of concurrently |
| 05:05:58 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 05:15:00 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:16:47 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 05:18:07 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:26:21 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:29:37 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:31:15 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:39:17 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 05:40:40 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:42:08 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 05:43:55 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:45:36 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 05:45:54 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 05:45:55 | × | arjun quits (~arjun@user/arjun) (Ping timeout: 255 seconds) |
| 05:47:38 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:47:38 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:48:28 | × | pixelmonk quits (~pixelmonk@50.205.76.66) (Quit: WeeChat 4.1.0) |
| 05:55:47 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 05:56:16 | × | ddellacosta quits (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 05:56:38 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 05:58:01 | → | ddellacosta joins (~ddellacos@ool-44c738de.dyn.optonline.net) |
| 05:58:24 | <thegman> | why are the error messages in haskell so... |
| 05:58:26 | <thegman> | strange |
| 05:59:31 | <thegman> | i forgot to add a coma and its explanation was "couldnt match expected type (a1, b1) -> (a, b) with actual type (a0, b0)" |
| 05:59:34 | <thegman> | comma* |
| 06:00:08 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:01:13 | <L29Ah> | because replacing a comma with a space in your case probably means replacing a tuple construction with a function application |
| 06:01:42 | <L29Ah> | could be less cryptic if the language demanded parens for application |
| 06:02:17 | <thegman> | it just seems unnessesary to say "couldnt match expected type with actual type" in every single error message |
| 06:02:39 | <L29Ah> | it's not like that in every single error message |
| 06:02:55 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:03:05 | <thegman> | it is in a lot of them |
| 06:03:13 | <L29Ah> | if you got to type errors your code actually parsed well, that's a great success |
| 06:03:29 | <Lycurgus> | same as elsewhite but mutatis mutandis for hs |
| 06:03:37 | <Lycurgus> | *elsewhere |
| 06:03:45 | <Lycurgus> | other langs |
| 06:03:58 | <Lycurgus> | famously |
| 06:04:45 | <Lycurgus> | the basis of a skill which seldom get a lot of general development because of monoglossy |
| 06:05:50 | <Lycurgus> | *gets |
| 06:06:31 | <Lycurgus> | or near monoglossy |
| 06:07:04 | <Lycurgus> | and with a few standard algol like langs |
| 06:08:06 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:08:15 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:18:11 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 06:18:37 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:18:37 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:22:56 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:23:04 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:26:20 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:29:20 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:35:36 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:42:43 | → | Enrico63 joins (~Enrico63@81.109.143.226) |
| 06:44:17 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 06:47:16 | → | gmg joins (~user@user/gehmehgeh) |
| 06:47:28 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:50:34 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:52:36 | × | thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving) |
| 06:54:29 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 06:57:38 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 06:57:38 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 07:01:21 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 07:05:25 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 07:11:04 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 07:16:36 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 07:16:50 | × | img_ quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 07:18:23 | → | img joins (~img@user/img) |
| 07:21:14 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 07:23:52 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 07:26:07 | × | Enrico63 quits (~Enrico63@81.109.143.226) (Ping timeout: 248 seconds) |
| 07:32:59 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 245 seconds) |
| 07:33:38 | → | cmtaur^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 07:34:43 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 264 seconds) |
| 07:35:06 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 07:43:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:46:10 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 07:46:18 | <Inst> | erm, just curious |
| 07:46:32 | → | takuan joins (~takuan@178.116.218.225) |
| 07:46:36 | <Inst> | how do you split a Haskell program off a console? |
| 07:50:10 | → | acidjnk joins (~acidjnk@p200300d6e72b93365d0d304e1b7de813.dip0.t-ipconnect.de) |
| 07:51:31 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 07:52:35 | <probie> | Inst: What do you mean by that? |
| 07:53:37 | <Inst> | let's say, i want a program to be a daemon |
| 07:53:44 | <Inst> | or a graphics program that releases the console after the window opens |
| 08:02:56 | → | rosco joins (~rosco@yp-150-69.tm.net.my) |
| 08:04:21 | <haskellbridge> | 06<sm> it might be somewhere like System.IO or GHC.IO |
| 08:05:26 | <mauke> | a real daemon should run in the foreground, managed by some sort of services system |
| 08:06:03 | → | arjun joins (~arjun@user/arjun) |
| 08:07:19 | <mauke> | you'd have to use fork(), which isn't really supported in Haskell |
| 08:08:10 | <mauke> | also: reopen stdin/stdout/stderr to /dev/null or some kind of log file; chdir to /; call setsid() |
| 08:08:25 | <mauke> | I'm not sure what that would look like in Haskell |
| 08:09:27 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 08:10:06 | <mauke> | (fork() because all of this should happen in the child process; the parent should just exit) |
| 08:15:02 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 08:15:59 | → | fendor joins (~fendor@2a02:8388:1640:be00:2a62:2dd0:490d:f2ca) |
| 08:17:19 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 08:21:29 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 08:26:45 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 08:26:46 | × | Inst quits (~Inst@120.244.192.250) (Remote host closed the connection) |
| 08:27:07 | → | Inst joins (~Inst@120.244.192.250) |
| 08:29:30 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 08:36:25 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:39:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:40:40 | × | Inst quits (~Inst@120.244.192.250) (Ping timeout: 255 seconds) |
| 08:40:46 | × | arjun quits (~arjun@user/arjun) (Quit: Quit!) |
| 08:44:09 | → | Inst joins (~Inst@120.244.192.250) |
| 08:53:41 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 08:55:57 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 08:56:26 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 08:58:19 | → | Jackneill_ joins (~Jackneill@20014C4E1E16F00019AC831304B7663E.dsl.pool.telekom.hu) |
| 08:59:29 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 09:01:00 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 09:10:00 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 09:15:06 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 09:18:00 | × | rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 09:18:22 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 09:19:48 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 09:23:45 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 09:25:27 | → | mastarija joins (~mastarija@141-136-170-90.dsl.iskon.hr) |
| 09:26:04 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 09:27:30 | <mastarija> | Is there a way, via some language extension, to "re-define" a list with all the nice syntax sugar like `[ x ]`? I'd like to do a little demo for some students, and defining a list like `data List a = Empty | Cons a (List a)` is not as cool I think :) |
| 09:28:47 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ed19:80b6:e70a:c3d) (Remote host closed the connection) |
| 09:29:23 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) |
| 09:29:32 | idgaen | thinks that syntax is wired in the language |
| 09:29:56 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 09:30:07 | <mastarija> | Yeah. But I was hoping there's something like TypeOperators |
| 09:30:29 | <probie> | mastarija: You can use `OverloadedLists` (https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/overloaded_lists.html), but that won't disallow the syntax from being used to write the old lists |
| 09:30:31 | × | pavonia quits (~user@user/siracusa) (Ping timeout: 264 seconds) |
| 09:30:53 | <probie> | and the types might be intimidating |
| 09:30:55 | → | mosul joins (~mosul@user/kantokuen) |
| 09:31:04 | <probie> | % :set -XOverloadedLists |
| 09:31:04 | <yahb2> | <no output> |
| 09:31:15 | × | mosul quits (~mosul@user/kantokuen) (Client Quit) |
| 09:31:16 | <probie> | % :t ["foo", "bar", "baz"] |
| 09:31:16 | <yahb2> | ["foo", "bar", "baz"] ; :: (GHC.Exts.Item l ~ [Char], GHC.Exts.IsList l) => l |
| 09:31:36 | <mastarija> | Hm.. yeah. Not really what I'm looking for xD |
| 09:32:17 | <mastarija> | Agda is nice in that regard, everything is "open" to you in a way. Haskell is like that too, but it still has some "baked in" things. |
| 09:32:32 | <mastarija> | Less than other languages though. |
| 09:33:48 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Ping timeout: 258 seconds) |
| 09:34:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:34:54 | <int-e> | Isn't it easier to point out that [a] is essentially defined as `data [] a = [] | a : [a]` which is standard except for the odd [] and : name? And then you get [a,b,c] as extra syntax sugar. |
| 09:35:25 | <mastarija> | Yeah, that's what I'll do. But I was hoping we can get `[a]` somehow. |
| 09:35:27 | <int-e> | (if you type `:i []` in ghci it will actually spit out that definition though it's a bit of a lie) |
| 09:35:47 | <mastarija> | %:i [] |
| 09:36:02 | <mastarija> | % :i [] |
| 09:36:02 | <yahb2> | type [] :: * -> * ; data [] a = [] | a : [a] ; -- Defined in ‘GHC.Types’ ; instance Applicative [] -- Defined in ‘GHC.Base’ ; instance Eq a => Eq [a] -- Defined in ‘GHC.Classes’ ; instance Funct... |
| 09:37:05 | <int-e> | If you look at GHC.Types you'll find `data List a = [] | a : List a` so clearly there's some magic in play :-) |
| 09:37:55 | <int-e> | (so maybe don't go that deep :-) ) |
| 09:40:41 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 240 seconds) |
| 09:40:43 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 264 seconds) |
| 09:41:18 | → | cmtaur^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 09:41:18 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 09:41:20 | × | fendor quits (~fendor@2a02:8388:1640:be00:2a62:2dd0:490d:f2ca) (Remote host closed the connection) |
| 09:41:39 | → | fendor joins (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) |
| 09:42:20 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 09:43:47 | → | rosco joins (~rosco@193.138.218.161) |
| 09:45:14 | → | pavonia joins (~user@user/siracusa) |
| 09:45:51 | × | Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 240 seconds) |
| 09:46:00 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 09:49:07 | × | rosco quits (~rosco@193.138.218.161) (Ping timeout: 264 seconds) |
| 09:49:28 | → | rosco joins (~rosco@yp-150-69.tm.net.my) |
| 09:57:31 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 09:59:58 | → | neceve joins (~neceve@user/neceve) |
| 10:00:38 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 10:03:23 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) |
| 10:08:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:09:01 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 10:12:40 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:13:13 | → | mechap joins (~mechap@user/mechap) |
| 10:13:31 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 10:14:34 | × | mastarija quits (~mastarija@141-136-170-90.dsl.iskon.hr) (Quit: Client closed) |
| 10:16:48 | → | gooba_ joins (~gooba@90-231-13-185-no3430.tbcn.telia.com) |
| 10:18:37 | × | gooba quits (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Ping timeout: 255 seconds) |
| 10:19:27 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 10:20:59 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 10:24:31 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 10:27:01 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 10:27:31 | × | lg188 quits (~lg188@82.18.98.230) (Ping timeout: 260 seconds) |
| 10:31:03 | → | lg188 joins (~lg188@82.18.98.230) |
| 10:32:11 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 10:36:43 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 10:38:07 | × | AssCrackBandit quits (~user@cust-west-par-46-193-2-167.cust.wifirst.net) (Ping timeout: 255 seconds) |
| 10:39:50 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 10:50:59 | <Inst> | wow, hahahhaa |
| 10:51:04 | <Inst> | i have my punishment for stuffing everything in main |
| 10:51:22 | <Inst> | i found a bit of code that i have to go through that's 200-300 SLOC and is an IO action abusing where |
| 10:52:52 | <Inst> | nope, it's 400-600 SLOC |
| 10:52:57 | <Inst> | and it's just one do block |
| 10:52:58 | <Inst> | :D |
| 10:53:11 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Ping timeout: 260 seconds) |
| 10:54:02 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 10:54:06 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 10:57:20 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 10:58:26 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:00:04 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 245 seconds) |
| 11:00:47 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:01:04 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 272 seconds) |
| 11:02:12 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 11:04:23 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:07:15 | × | sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection) |
| 11:09:51 | → | sefidel joins (~sefidel@user/sefidel) |
| 11:11:08 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:12:05 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 11:14:19 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:15:01 | × | pavonia quits (~user@user/siracusa) (Ping timeout: 240 seconds) |
| 11:19:58 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:24:05 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:27:59 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:29:28 | × | xff0x quits (~xff0x@ai101218.d.east.v6connect.net) (Quit: xff0x) |
| 11:31:09 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:32:27 | → | xff0x joins (~xff0x@2405:6580:b080:900:6924:f1c7:f24d:2a0e) |
| 11:32:58 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 11:36:28 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 11:40:44 | → | erty joins (~user@user/aeroplane) |
| 11:48:19 | → | andrewboltachev joins (~andrey@178.141.195.228) |
| 11:52:18 | <andrewboltachev> | Hi. I'm using Twain library to create a server. The endpoint I've created accepts JSON, does some experimental work and should return JSON. For certain inputs, request is terminating silently after 1min without response. Is there any way to access logs for Twain, 'cause I don't see any debug output anywhere on that failure |
| 11:56:59 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:01:07 | × | mrmr155 quits (~mrmr@user/mrmr) (Quit: Bye, See ya later!) |
| 12:01:18 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:02:53 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:03:06 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Quit: WeeChat 4.1.1) |
| 12:06:13 | <[exa]> | andrewboltachev: quite often I just do a `strace` on the process to see where it's hanging |
| 12:06:16 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:06:23 | <[exa]> | andrewboltachev: btw just to check, you compile with -threaded, right ? |
| 12:06:24 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:07:53 | <[exa]> | also, anything specific in the "certain" inputs, or is it completely random? |
| 12:08:30 | → | mrmr1553 joins (~mrmr@user/mrmr) |
| 12:08:45 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Remote host closed the connection) |
| 12:10:23 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:10:25 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:10:34 | × | erty quits (~user@user/aeroplane) (Read error: Connection reset by peer) |
| 12:10:48 | → | erty joins (~user@user/aeroplane) |
| 12:14:30 | <andrewboltachev> | [exa]: Very specific inputs. But it's anyway doing quite heavy operations: it's my own parser generator processing JSON I've got from Figma API (Figma, the graphical design tool) |
| 12:15:06 | <andrewboltachev> | [exa]: Now solved that with just: https://hackage.haskell.org/package/warp-3.3.30/docs/Network-Wai-Handler-Warp.html#g:3 setTimeout |
| 12:18:00 | → | pavonia joins (~user@user/siracusa) |
| 12:20:24 | × | rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 12:20:35 | → | rosco joins (~rosco@yp-150-69.tm.net.my) |
| 12:21:31 | × | erty quits (~user@user/aeroplane) (Ping timeout: 264 seconds) |
| 12:23:03 | <andrewboltachev> | [exa] And yes -threaded is in my package.yaml |
| 12:30:45 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:31:40 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 258 seconds) |
| 12:31:43 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 264 seconds) |
| 12:32:00 | → | cmtaur^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 12:32:02 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 12:32:41 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:36:28 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:38:00 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:41:26 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 12:42:17 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:43:16 | → | __monty__ joins (~toonn@user/toonn) |
| 12:46:20 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:50:05 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 12:50:50 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) |
| 12:53:49 | <[exa]> | andrewboltachev: hm perhaps the parser was hanging somewhere? (might be reading from the input when there wasn't more stuff to be read?) |
| 12:54:02 | <[exa]> | anyway good that timeout solves it :] |
| 12:57:30 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 12:59:47 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 13:01:08 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 13:04:49 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 13:05:55 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 13:09:46 | <Umeaboy> | [exa] GHC compiled and successfully built with ghcup, however HLS failed. I'm now trying to build HLS 1.8.0.0........ So far so good. |
| 13:10:03 | <Umeaboy> | I read this page: https://haskell-language-server.readthedocs.io/en/latest/support/ghc-version-support.html |
| 13:10:10 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 13:10:15 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Ping timeout: 240 seconds) |
| 13:11:49 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 13:14:57 | → | tomith joins (tomith@user/tomith) |
| 13:15:35 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 13:15:50 | → | target_i joins (~target_i@217.175.14.39) |
| 13:15:59 | × | Umeaboy quits (~Umeaboy@94-255-145-133.cust.bredband2.com) (Remote host closed the connection) |
| 13:20:24 | → | Umeaboy joins (~Umeaboy@94-255-145-133.cust.bredband2.com) |
| 13:23:55 | × | Inst quits (~Inst@120.244.192.250) (Ping timeout: 264 seconds) |
| 13:24:23 | → | falafel joins (~falafel@62.175.113.194.dyn.user.ono.com) |
| 13:26:37 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 13:28:06 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 13:29:48 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 13:29:59 | → | cods joins (~fred@tuxee.net) |
| 13:31:48 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Client Quit) |
| 13:35:55 | × | Square quits (~Square@user/square) (Ping timeout: 252 seconds) |
| 13:45:01 | × | Umeaboy quits (~Umeaboy@94-255-145-133.cust.bredband2.com) (Ping timeout: 240 seconds) |
| 13:45:32 | × | rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 13:47:07 | → | Inst joins (~Inst@120.244.192.250) |
| 13:47:23 | × | CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
| 13:48:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:49:30 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 13:51:59 | <andrewboltachev> | [exa]: I've even had "stack overflow" on it once. But it's not the case for this problem — as it took 1min13sec, which is bigger than 1min |
| 13:55:12 | <[exa]> | ah lot of processing then |
| 13:55:58 | <[exa]> | good, I somehow assumed the webservices take like 1s per request max... (might also be the case with twain folks, is it tested that way?) |
| 13:56:07 | → | rosco joins (~rosco@yp-150-69.tm.net.my) |
| 13:57:10 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:02:12 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Ping timeout: 272 seconds) |
| 14:05:37 | → | Pickchea joins (~private@user/pickchea) |
| 14:08:49 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 14:09:08 | → | mmhat joins (~mmh@p200300f1c7445e8aee086bfffe095315.dip0.t-ipconnect.de) |
| 14:09:22 | × | mmhat quits (~mmh@p200300f1c7445e8aee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 14:11:31 | × | falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 260 seconds) |
| 14:20:07 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 14:20:37 | → | CO2 joins (CO2@gateway/vpn/protonvpn/co2) |
| 14:20:57 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 14:24:48 | → | Umeaboy joins (~Umeaboy@94-255-145-133.cust.bredband2.com) |
| 14:26:19 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 14:33:05 | × | gooba_ quits (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Quit: Leaving) |
| 14:33:23 | → | gooba joins (~gooba@90-231-13-185-no3430.tbcn.telia.com) |
| 14:36:01 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 240 seconds) |
| 14:55:58 | → | ski joins (~ski@88.131.7.247) |
| 15:10:19 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 15:10:51 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 15:13:54 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 15:15:38 | → | zetef joins (~quassel@5.14.139.38) |
| 15:21:20 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 15:23:31 | × | fendor quits (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection) |
| 15:29:19 | × | zetef quits (~quassel@5.14.139.38) (Ping timeout: 264 seconds) |
| 15:35:15 | × | Inst quits (~Inst@120.244.192.250) (Read error: Connection reset by peer) |
| 15:38:46 | → | zetef joins (~quassel@86.124.124.51) |
| 15:41:19 | × | ski quits (~ski@88.131.7.247) (Ping timeout: 264 seconds) |
| 15:42:53 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 15:48:45 | → | ph88 joins (~ph88@2a02:8109:9e26:c800::302a) |
| 15:49:04 | × | phma quits (phma@2001:5b0:212a:b088:bde:88f:7cf:d96) (Read error: Connection reset by peer) |
| 15:49:43 | × | zetef quits (~quassel@86.124.124.51) (Ping timeout: 264 seconds) |
| 15:49:50 | → | phma joins (~phma@host-67-44-208-186.hnremote.net) |
| 15:49:56 | → | zetef joins (~quassel@5.14.137.55) |
| 15:50:37 | → | Tlsx joins (~rscastilh@187.40.125.21) |
| 15:53:41 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 240 seconds) |
| 15:53:41 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 240 seconds) |
| 15:54:37 | → | cmtaur^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 15:54:38 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 15:56:38 | → | lydell joins (~lydell@2001:1ba8:14b4:f200:89b1:efc8:1d1b:fed7) |
| 15:58:00 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 15:58:21 | × | zetef quits (~quassel@5.14.137.55) (Ping timeout: 240 seconds) |
| 15:58:36 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) |
| 15:58:37 | → | zetef joins (~quassel@5.14.143.55) |
| 16:03:11 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 16:05:43 | → | pixelmonk joins (~pixelmonk@50.205.76.66) |
| 16:06:48 | × | CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
| 16:10:41 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 240 seconds) |
| 16:10:41 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Ping timeout: 240 seconds) |
| 16:11:00 | → | dsrt^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 16:11:24 | → | cmtaur^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 16:17:48 | → | CO2 joins (CO2@gateway/vpn/protonvpn/co2) |
| 16:27:20 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 16:28:15 | × | zetef quits (~quassel@5.14.143.55) (Remote host closed the connection) |
| 16:31:05 | → | trev joins (~trev@user/trev) |
| 16:33:01 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 16:36:13 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 16:42:42 | × | tabemann quits (~tabemann@12.215.215.61) (Quit: Leaving) |
| 16:43:34 | × | cmtaur^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Remote host closed the connection) |
| 16:43:46 | × | dsrt^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Remote host closed the connection) |
| 16:45:29 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 16:50:46 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 16:53:18 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 16:56:39 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 17:00:01 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:02:22 | × | Umeaboy quits (~Umeaboy@94-255-145-133.cust.bredband2.com) (Quit: Leaving) |
| 17:03:32 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 17:04:29 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:06:48 | <andrewboltachev> | [exa]: Well what's interesting that's Network.Wai that manages the timeout (it exposes functions called run/runSettings). So it's not Twain: https://github.com/andrewboltachev/matcher/blob/master/app/Main.hs#L27 |
| 17:06:51 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:10:01 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 17:10:45 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 17:13:44 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:15:09 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 17:18:27 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 17:18:53 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 17:19:38 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:27:55 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:31:09 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 17:32:18 | × | rosco quits (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 17:34:20 | → | iteratee joins (~kyle@162.218.222.207) |
| 17:36:20 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:37:44 | × | lydell quits (~lydell@2001:1ba8:14b4:f200:89b1:efc8:1d1b:fed7) (Quit: Client closed) |
| 17:38:58 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 17:42:08 | → | todi joins (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 17:44:09 | × | todi quits (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Client Quit) |
| 17:49:52 | → | thegman joins (~thegman@072-239-207-086.res.spectrum.com) |
| 18:06:41 | × | andrewboltachev quits (~andrey@178.141.195.228) (Quit: Leaving.) |
| 18:07:12 | → | zetef joins (~quassel@5.2.182.98) |
| 18:11:52 | → | falafel joins (~falafel@62.175.113.194.dyn.user.ono.com) |
| 18:13:51 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) (Ping timeout: 240 seconds) |
| 18:15:06 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 18:15:11 | → | zetef_ joins (~quassel@5.2.182.98) |
| 18:16:40 | → | fendor joins (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) |
| 18:17:41 | × | falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 240 seconds) |
| 18:17:41 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 240 seconds) |
| 18:22:27 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 18:25:16 | → | pruiz joins (~user@90.167.98.188) |
| 18:27:31 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 18:28:39 | × | zetef_ quits (~quassel@5.2.182.98) (Ping timeout: 240 seconds) |
| 18:30:41 | × | pruiz quits (~user@90.167.98.188) (Changing host) |
| 18:30:41 | → | pruiz joins (~user@user/pruiz) |
| 18:30:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:33:54 | → | Guest71 joins (~Guest51@2804:14c:658b:5993:414e:c397:748f:b8af) |
| 18:34:39 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 240 seconds) |
| 18:35:36 | → | qqq joins (~qqq@92.43.167.61) |
| 18:37:53 | → | zetef joins (~quassel@5.2.182.98) |
| 18:38:54 | → | falafel joins (~falafel@62.175.113.194.dyn.user.ono.com) |
| 18:39:28 | Guest71 | is now known as edil |
| 18:41:57 | → | jinsun joins (~jinsun@user/jinsun) |
| 18:50:55 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 264 seconds) |
| 18:53:42 | → | miguelnegrao joins (~miguelneg@2001:818:dc71:d100:f016:1b9:e7c1:3567) |
| 18:55:18 | <miguelnegrao> | Hi all. Is there a package, github repo or gist where div is defined for Peano natural numbers at the type level defined via induction, e.g., data Nat = Zero | Succ Nat ? |
| 18:56:00 | <miguelnegrao> | The definition of for Lean uses the "less or equal to" relation, which seems a bit tricky to do at the type level. |
| 18:56:32 | <miguelnegrao> | plus, mult, minus, and pow are easy, in comparison |
| 18:57:22 | <miguelnegrao> | I have a version working defining LE return a bool, but it seems quite hard to do proofs with that approach. |
| 19:00:01 | × | pruiz quits (~user@user/pruiz) (Ping timeout: 240 seconds) |
| 19:04:56 | × | edil quits (~Guest51@2804:14c:658b:5993:414e:c397:748f:b8af) (Quit: Client closed) |
| 19:14:08 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:1052:6194:3db5:da7a) |
| 19:16:10 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 256 seconds) |
| 19:16:22 | × | falafel quits (~falafel@62.175.113.194.dyn.user.ono.com) (Ping timeout: 255 seconds) |
| 19:18:15 | × | miguelnegrao quits (~miguelneg@2001:818:dc71:d100:f016:1b9:e7c1:3567) (Quit: miguelnegrao) |
| 19:18:35 | × | Flow quits (~none@gentoo/developer/flow) (Ping timeout: 240 seconds) |
| 19:18:37 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 19:26:29 | <EvanR> | drat |
| 19:26:34 | → | Flow joins (~none@gentoo/developer/flow) |
| 19:26:34 | <EvanR> | they left! |
| 19:26:39 | × | rncwnd quits (~quassel@2a01:4f8:221:27c6::1) (Quit: Later) |
| 19:27:15 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 19:27:19 | → | rncwnd joins (~quassel@2a01:4f8:221:27c6::1) |
| 19:27:35 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 19:27:45 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 19:28:50 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 19:31:06 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:35:12 | → | Guest73 joins (~Guest73@2001:8a0:fcac:9000:10bf:dfbb:64e:cc63) |
| 19:37:40 | <EvanR> | @tell miguelnegrao if you look at the idris standard library you will find an example of a decidable divisibility predicate for natural numbers which can be used to implement division / remainder in a way that is useful to other proofs |
| 19:37:41 | <lambdabot> | Consider it noted. |
| 19:38:13 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 19:39:23 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 19:40:48 | × | Guest73 quits (~Guest73@2001:8a0:fcac:9000:10bf:dfbb:64e:cc63) (Quit: Client closed) |
| 19:43:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:45:22 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 19:45:30 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 19:46:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 19:47:03 | × | haskellbridge quits (~haskellbr@069-135-003-034.biz.spectrum.com) (Ping timeout: 260 seconds) |
| 19:48:27 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 19:49:43 | × | pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 264 seconds) |
| 19:49:50 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 19:50:47 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 19:58:51 | → | haskellbridge joins (~haskellbr@069-135-003-034.biz.spectrum.com) |
| 19:58:51 | ChanServ | sets mode +v haskellbridge |
| 19:59:53 | × | thegman quits (~thegman@072-239-207-086.res.spectrum.com) (Read error: Connection reset by peer) |
| 20:00:23 | → | thegman joins (~thegman@072-239-207-086.res.spectrum.com) |
| 20:01:13 | → | pixelmonk joins (~pixelmonk@50.205.76.66) |
| 20:05:21 | × | pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 240 seconds) |
| 20:19:37 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 20:24:01 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds) |
| 20:24:54 | → | pixelmonk joins (~pixelmonk@50.205.76.66) |
| 20:29:52 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 20:31:37 | → | ciiur^^ joins (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) |
| 20:32:55 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 20:33:24 | ec_ | is now known as ec |
| 20:33:48 | → | __________ joins (~nobody@user/noodly) |
| 20:34:40 | × | _________ quits (~nobody@user/noodly) (Ping timeout: 258 seconds) |
| 20:37:37 | ec | is now known as R |
| 20:38:07 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 20:42:44 | × | Tlsx quits (~rscastilh@187.40.125.21) () |
| 20:45:29 | × | __________ quits (~nobody@user/noodly) (Quit: leaving) |
| 20:53:19 | × | neceve quits (~neceve@user/neceve) (Ping timeout: 264 seconds) |
| 20:54:09 | → | _________ joins (~nobody@user/noodly) |
| 20:59:52 | → | AssCrackBandit joins (~user@cust-west-par-46-193-2-167.cust.wifirst.net) |
| 21:01:39 | → | Pickchea joins (~private@user/pickchea) |
| 21:05:29 | R | is now known as ec |
| 21:05:41 | → | tabemann joins (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 21:10:58 | × | fendor quits (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection) |
| 21:11:31 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 21:17:01 | → | zetef joins (~quassel@5.2.182.98) |
| 21:37:58 | ← | ec parts (~ec@gateway/tor-sasl/ec) () |
| 21:40:55 | → | pavonia joins (~user@user/siracusa) |
| 21:42:40 | <yin> | does haskeel have something like pm2 for node? |
| 21:43:18 | <yin> | or some kind of process manager |
| 21:45:27 | <exarkun> | yin: "some kind of"? sure. |
| 21:46:00 | <yin> | i mean to manage ghc processes |
| 21:47:15 | × | pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 255 seconds) |
| 21:48:07 | <geekosaur> | ghc processes are native, you use a process manager for native processes, not one for a javascript backend |
| 21:48:46 | <Hecate> | yin: still pm2 https://pm2.keymetrics.io/docs/usage/process-management/#start-any-process-type |
| 21:50:21 | <yin> | geekosaur: ok so systemd I guess |
| 21:50:30 | → | pixelmonk joins (~pixelmonk@50.205.76.66) |
| 21:50:32 | <yin> | Hecate: nice, thanks! |
| 21:51:21 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 240 seconds) |
| 21:54:14 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:58:49 | × | Jackneill_ quits (~Jackneill@20014C4E1E16F00019AC831304B7663E.dsl.pool.telekom.hu) (Ping timeout: 245 seconds) |
| 22:05:18 | <EvanR> | Coyoneda f a is some mapping function (b -> a) polymorphic in the return type paired with some f b waiting to be mapped by it. You just have to pick the a. Is the only real example of this in action Coyoneda id |
| 22:09:28 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 22:09:43 | <dolio> | What do you mean? |
| 22:10:20 | → | talismanick joins (~user@2601:204:ef00:bb0::f34e) |
| 22:10:21 | <EvanR> | ok you could do \x -> Coyoneda snd (7, x). I mean, function returning "whatever type you want" seem to be hard to come up with examples for |
| 22:11:41 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 22:11:55 | <EvanR> | or I'm just way off |
| 22:12:15 | × | quintasan quits (~quassel@quintasan.pl) () |
| 22:12:24 | → | quintasan joins (~quassel@quintasan.pl) |
| 22:12:28 | <EvanR> | a isn't "existential" so I'm trippin |
| 22:12:32 | <dolio> | `Coyoneda f a` has a particular a. |
| 22:14:33 | <ncf> | Coyoneda snd (7, x) is ill-typed |
| 22:15:05 | → | falafel joins (~falafel@62.175.113.194.dyn.user.ono.com) |
| 22:15:18 | <ncf> | or i guess it isn't, but the snd doesn't apply to the pair |
| 22:15:31 | <monochrom> | No, Coyoneda is an existential type. |
| 22:16:09 | <EvanR> | \x -> CY snd (7, x) :: Num a1 => (a2, a3) -> Coyoneda ((,) a1) a3 |
| 22:16:20 | <EvanR> | worked for me without enabling any extensions yay |
| 22:16:44 | <EvanR> | er... well it typed but not to what I thought it would |
| 22:18:47 | <EvanR> | yeah i see |
| 22:20:50 | <monochrom> | My example would be: Coyoneda (length :: String -> Int) ["hello", "hi"] :: Coyoneda [] Int. I am hiding the String type and a list of String values. You can see my example is a long way to say [5,2]. |
| 22:21:01 | → | Inst joins (~Inst@120.244.192.250) |
| 22:21:47 | <EvanR> | basically it is delaying the inevitable, the only thing you do is apply them |
| 22:21:50 | <EvanR> | or this |
| 22:21:52 | <EvanR> | hoistCoyoneda :: (forall a. f a -> g a) -> Coyoneda f b -> Coyoneda g b |
| 22:22:20 | <monochrom> | If you pattern match my value against Coyoneda fst snd, you won't be told that I have String inside, but you can fmap fst snd to recover [5,2]. |
| 22:22:58 | <monochrom> | I forgot the use cases, but yes the use cases benefit greatly from the delay. |
| 22:23:07 | <dolio> | The coyoneda lemma says that for functors `f`, `CY id fx` for `fx :: f x` is 'essentially' the only value. |
| 22:23:57 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 22:28:54 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 258 seconds) |
| 22:29:07 | × | takuan quits (~takuan@178.116.218.225) (Remote host closed the connection) |
| 22:30:07 | <EvanR> | the same thing is happening in data Data f g a = forall b c . Day (f b) (g c) (b -> c -> a), some f b and some g c paired with a function returning a, waiting for you to apply it to them |
| 22:32:14 | <EvanR> | (using Applicative) |
| 22:32:38 | <EvanR> | (and only then, if f = g) |
| 22:33:12 | <EvanR> | that should have said data Day f g a |
| 22:33:56 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 256 seconds) |
| 22:34:06 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 22:34:53 | → | bramhaag7 joins (~bramhaag@198.8.58.39) |
| 22:34:56 | <ncf> | coends are your cofriends |
| 22:35:32 | × | bramhaag7 quits (~bramhaag@198.8.58.39) (Client Quit) |
| 22:36:00 | <dolio> | In general you can use Coyoneda on an `f` that isn't a functor. Then it makes it into one. |
| 22:36:15 | → | bramhaag7 joins (~bramhaag@198.8.58.39) |
| 22:36:30 | → | zetef joins (~quassel@5.2.182.98) |
| 22:39:00 | × | bramhaag7 quits (~bramhaag@198.8.58.39) (Client Quit) |
| 22:39:48 | → | bramhaag7 joins (~bramhaag@198.8.58.39) |
| 22:40:36 | <EvanR> | in a trivial way? |
| 22:40:48 | <EvanR> | there's some fine print about that |
| 22:41:22 | × | bramhaag7 quits (~bramhaag@198.8.58.39) (Client Quit) |
| 22:42:09 | → | bramhaag7 joins (~bramhaag@198.8.58.39) |
| 22:45:15 | <ncf> | in a free way |
| 22:45:31 | <ncf> | you could say it's the "free functor" free functor if you wanted everyone to hate you |
| 22:45:48 | <Rembane> | The hateful functor? |
| 22:46:15 | <EvanR> | if f is not a functor, it seems you can never do anything but continue to append post processing functions to the inner map |
| 22:46:16 | <ncf> | (in the sense that it's left adjoint to the forgetful functor from a category of functors to the discrete category of object mappings) |
| 22:49:00 | <EvanR> | you can put any f x into Coyoneda, but once you ship that it's not coming back out again if f is not a functor |
| 22:49:46 | <EvanR> | it's not like a nightclub |
| 22:50:21 | × | Ram-Z quits (~Ram-Z@li1814-254.members.linode.com) (Ping timeout: 240 seconds) |
| 22:51:08 | <ncf> | wait that forgetful functor doesn't make sense, what am i trying to say |
| 22:51:15 | → | Square joins (~Square@user/square) |
| 22:52:04 | <jackdk> | EvanR: have you seen https://blog.ocharles.org.uk/posts/2017-08-23-extensible-effects-and-transformers.html ? |
| 22:52:15 | <ncf> | oh yeah it's not discrete. the category of object mappings and unnatural transformations |
| 22:53:19 | <EvanR> | no but it looks interesting |
| 22:53:45 | <monochrom> | Yikes unnatural transformations. Is that belated Halloween? Is that like how Palpatine lives again? >:) |
| 22:54:08 | <ncf> | they're like natural transformations except not natural |
| 22:57:21 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:57:30 | <EvanR> | side tangent >Obviously, interacting with ListenBrainz requires some sort of IO so whatever API I will be offering has to live within some sort of monad |
| 22:57:40 | <EvanR> | citation needed xD |
| 22:57:42 | → | Ram-Z joins (~Ram-Z@li1814-254.members.linode.com) |
| 22:58:13 | <EvanR> | on the monad required par |
| 22:58:48 | <jackdk> | How do you propose to do anything useful with the result if it doesn't? |
| 23:01:11 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
| 23:03:23 | <EvanR> | ok Applicative has no way of doing that, I guess |
| 23:04:08 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:04:39 | × | ciiur^^ quits (~cd@70-88-177-118-Atlanta.hfc.comcastbusiness.net) (Remote host closed the connection) |
| 23:07:56 | <EvanR> | if Coyoneda is a free functor factory, is Yoneda a forgetful functor factory? |
| 23:12:42 | <ncf> | nah |
| 23:16:03 | × | acidjnk quits (~acidjnk@p200300d6e72b93365d0d304e1b7de813.dip0.t-ipconnect.de) (Ping timeout: 258 seconds) |
| 23:16:43 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 264 seconds) |
| 23:18:06 | × | pixelmonk quits (~pixelmonk@50.205.76.66) (Ping timeout: 260 seconds) |
| 23:18:56 | × | target_i quits (~target_i@217.175.14.39) (Quit: leaving) |
| 23:19:25 | <dolio> | Yoneda is the cofree functor. |
| 23:21:17 | → | zetef joins (~quassel@5.2.182.98) |
| 23:21:19 | <dolio> | You can put anything in Coyoneda, but need it to be a functor to get it out. You can get anything out of Yoneda, but need it to be a functor to put it in. |
| 23:24:55 | <ncf> | Yoneda would be the right adjoint to my forgetful functor, i think |
| 23:25:02 | <dolio> | Right. |
| 23:25:03 | → | notzmv joins (~zmv@user/notzmv) |
| 23:25:54 | × | zetef quits (~quassel@5.2.182.98) (Remote host closed the connection) |
| 23:25:55 | <EvanR> | I see they "got out" in the blog post by hoisting from the non-functor to a functor (the implementation monad transformer) |
| 23:26:21 | → | zetef joins (~quassel@5.2.182.98) |
| 23:26:39 | × | zetef quits (~quassel@5.2.182.98) (Read error: Connection reset by peer) |
| 23:27:07 | → | zetef joins (~quassel@5.2.182.98) |
| 23:27:26 | × | zetef quits (~quassel@5.2.182.98) (Remote host closed the connection) |
| 23:27:32 | <ncf> | i'm actually confused about something now: if you put a functor through Coyoneda you're supposed to get the same functor you put in, i.e. Coyoneda (U F) ≅ F. but that would imply that functors are a full subcategory of object-mappings-and-natural-transformations, which they aren't since morphism mappings aren't unique |
| 23:27:54 | → | zetef joins (~quassel@5.2.182.98) |
| 23:27:57 | × | zetef quits (~quassel@5.2.182.98) (Read error: Connection reset by peer) |
| 23:28:23 | <ncf> | a reflective subcategory even |
| 23:29:26 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 23:29:45 | → | califax joins (~califax@user/califx) |
| 23:30:01 | <dolio> | I don't know if that's actually the right forgetful functor. |
| 23:30:35 | <ncf> | i should ask agda what it thinks |
| 23:31:39 | → | pixelmonk joins (~pixelmonk@50.205.76.66) |
| 23:31:59 | → | Square2 joins (~Square4@user/square) |
| 23:37:09 | <ncf> | what am i even doing |
| 23:37:23 | <ncf> | Coyoneda is defined as a coend, so you can't apply it to something that's not in functor |
| 23:37:40 | <ncf> | you can only do that in haskell because the coend condition is not enforced |
| 23:37:55 | <ncf> | s/in/a/ |
| 23:38:23 | × | Inst quits (~Inst@120.244.192.250) (Read error: Connection reset by peer) |
| 23:39:50 | × | xff0x quits (~xff0x@2405:6580:b080:900:6924:f1c7:f24d:2a0e) (Ping timeout: 255 seconds) |
| 23:40:43 | <ncf> | i think really what's going on is that every * → * in haskell is a functor even if you don't declare a Functor instance for it, because parametricity |
| 23:40:50 | → | xff0x joins (~xff0x@2405:6580:b080:900:9f61:b997:2a7f:e8b4) |
| 23:40:55 | <dolio> | No. |
| 23:41:05 | <ncf> | er |
| 23:41:12 | <ncf> | assuming the right variance |
| 23:41:19 | <dolio> | Okay, so, no. |
| 23:44:43 | → | Inst joins (~Inst@120.244.192.250) |
| 23:45:42 | <EvanR> | every * -> * is a functor in the category hask restricted to having only identity morphisms? |
| 23:45:59 | <EvanR> | am I doing category theory right? xD |
| 23:46:02 | <dolio> | Certainly that, at least. |
| 23:49:18 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 23:50:39 | <ncf> | on Core(Hask), even |
| 23:50:59 | <ncf> | ok but at least Functor is a property because of parametricity, so that solves the uniqueness mystery |
| 23:51:51 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 23:55:21 | <monochrom> | My favourite "newtype D a = D (D a -> a)" is not going to be a functor. >:) |
| 23:55:47 | <monochrom> | In fact, it's so contravariant to the extreme, it recovers fix. |
| 23:56:40 | × | Square2 quits (~Square4@user/square) (Quit: Leaving) |
| 23:59:13 | × | CO2 quits (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
| 23:59:34 | <EvanR> | hold my beer |
All times are in UTC on 2023-11-05.