Logs: freenode/#haskell
| 2021-05-05 10:33:17 | × | Pickchea quits (~private@unaffiliated/pickchea) (Ping timeout: 246 seconds) |
| 2021-05-05 10:33:37 | <siers> | Hi! Is it the case that the 'Nat's in agda are fully representable in haskell, just not as useful? |
| 2021-05-05 10:36:42 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 265 seconds) |
| 2021-05-05 10:36:56 | <dminuoso> | Yes. |
| 2021-05-05 10:37:04 | → | rayyyy joins (~nanoz@gateway/tor-sasl/nanoz) |
| 2021-05-05 10:37:11 | <dminuoso> | You can simply write `data Nat = Z | S Nat` and use that. |
| 2021-05-05 10:37:26 | <dminuoso> | But you have to handroll all functions to work with that, and have terrible efficiency as well. |
| 2021-05-05 10:41:00 | → | kderme joins (2e675c7c@46-92-124.adsl.cyta.gr) |
| 2021-05-05 10:42:26 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 240 seconds) |
| 2021-05-05 10:46:40 | × | Gurkenglas_ quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 252 seconds) |
| 2021-05-05 10:48:18 | × | minoru_shiraeesh quits (~shiraeesh@77.94.25.20) (Ping timeout: 265 seconds) |
| 2021-05-05 10:48:28 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-05-05 10:49:13 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Read error: Connection reset by peer) |
| 2021-05-05 10:49:27 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-05-05 10:49:33 | × | rayyyy quits (~nanoz@gateway/tor-sasl/nanoz) (Ping timeout: 240 seconds) |
| 2021-05-05 10:54:01 | → | EvilMagix joins (~aVikingTr@2001:8003:340d:d00:b2de:b98:7a93:b0ea) |
| 2021-05-05 10:58:40 | × | kristijonas quits (~kristijon@78-56-32-39.static.zebra.lt) (Remote host closed the connection) |
| 2021-05-05 10:59:06 | → | kristijonas joins (~kristijon@78-56-32-39.static.zebra.lt) |
| 2021-05-05 11:00:04 | → | Alleria joins (~textual@2603-7000-3040-0000-84d6-e1ad-c4e3-d276.res6.spectrum.com) |
| 2021-05-05 11:00:27 | Alleria | is now known as Guest41562 |
| 2021-05-05 11:01:46 | → | minoru_shiraeesh joins (~shiraeesh@77.94.25.20) |
| 2021-05-05 11:02:31 | × | finn_elija quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Remote host closed the connection) |
| 2021-05-05 11:02:53 | → | finn_elija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 2021-05-05 11:03:47 | → | timCF joins (~i.tkachuk@ec2-35-158-4-35.eu-central-1.compute.amazonaws.com) |
| 2021-05-05 11:04:10 | → | ddellacosta joins (~ddellacos@86.106.143.200) |
| 2021-05-05 11:04:14 | <timCF> | Hello! Can anybody help me to find this function? `(a -> Either b c) -> [a] -> Either b [c]` It feels like it should be something very standard |
| 2021-05-05 11:04:33 | <Uniaika> | timCF: does hoogle give you a result? |
| 2021-05-05 11:04:34 | × | Guest41562 quits (~textual@2603-7000-3040-0000-84d6-e1ad-c4e3-d276.res6.spectrum.com) (Ping timeout: 245 seconds) |
| 2021-05-05 11:04:40 | <timCF> | Uniaika: no |
| 2021-05-05 11:05:16 | <timCF> | Uniaika: it might be something more generic like `(a -> f b c) -> t a -> f b (t c)` but it gives no result as well |
| 2021-05-05 11:05:33 | <Taneb> | :t traverse @[] @(Either a) |
| 2021-05-05 11:05:35 | <lambdabot> | error: |
| 2021-05-05 11:05:35 | <lambdabot> | Pattern syntax in expression context: traverse@[] |
| 2021-05-05 11:05:35 | <lambdabot> | Did you mean to enable TypeApplications? |
| 2021-05-05 11:05:46 | <Uniaika> | % :t traverse @[] @(Either a) |
| 2021-05-05 11:05:46 | <yahb> | Uniaika: ; <interactive>:1:23: error: Not in scope: type variable `a' |
| 2021-05-05 11:05:50 | <Uniaika> | damnation |
| 2021-05-05 11:05:53 | <Uniaika> | % :t traverse @[] @(Either Int) |
| 2021-05-05 11:05:53 | <yahb> | Uniaika: (a -> Either Int b) -> [a] -> Either Int [b] |
| 2021-05-05 11:05:59 | <Uniaika> | ah, we're getting somewhere |
| 2021-05-05 11:06:01 | × | v01d4lph4 quits (~v01d4lph4@122.160.65.250) () |
| 2021-05-05 11:06:14 | <Taneb> | As is often the case, it's trverse |
| 2021-05-05 11:06:22 | <Uniaika> | Taneb: praise be 🙇 |
| 2021-05-05 11:06:50 | <Taneb> | Note that this'll take the left-most Left |
| 2021-05-05 11:07:07 | <Taneb> | If you want to combine them, you could use traverse with Validation from one of the handful of libraries that provide that |
| 2021-05-05 11:08:32 | × | ddellacosta quits (~ddellacos@86.106.143.200) (Ping timeout: 240 seconds) |
| 2021-05-05 11:08:56 | <Uniaika> | timCF: yep, if you want to validate data, validation-selective is certainly your best bet |
| 2021-05-05 11:09:38 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-05-05 11:09:49 | → | p4trix joins (~p4trix@101.red-83-43-247.dynamicip.rima-tde.net) |
| 2021-05-05 11:10:43 | <timCF> | thanks! |
| 2021-05-05 11:13:05 | → | mav1 joins (~mav@ip-88-152-11-229.hsi03.unitymediagroup.de) |
| 2021-05-05 11:16:42 | × | royal_screwup213 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-05-05 11:17:00 | → | royal_screwup213 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-05-05 11:19:06 | → | tempate_ joins (~alpha@90.167.202.9) |
| 2021-05-05 11:19:24 | × | timCF quits (~i.tkachuk@ec2-35-158-4-35.eu-central-1.compute.amazonaws.com) (Quit: leaving) |
| 2021-05-05 11:19:31 | → | ADG1089 joins (~aditya@122.163.193.183) |
| 2021-05-05 11:22:11 | × | tempate quits (~alpha@unaffiliated/tempate) (Ping timeout: 240 seconds) |
| 2021-05-05 11:23:36 | × | p4trix quits (~p4trix@101.red-83-43-247.dynamicip.rima-tde.net) (Quit: Leaving) |
| 2021-05-05 11:25:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-05 11:34:30 | × | wei2912 quits (~wei2912@unaffiliated/wei2912) (Remote host closed the connection) |
| 2021-05-05 11:35:05 | × | ADG1089 quits (~aditya@122.163.193.183) (Remote host closed the connection) |
| 2021-05-05 11:35:09 | → | rdivyanshu joins (uid322626@gateway/web/irccloud.com/x-vhbgevczuzdaydua) |
| 2021-05-05 11:35:30 | → | ADG1089 joins (~aditya@122.163.193.183) |
| 2021-05-05 11:36:43 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-05-05 11:37:08 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-05-05 11:40:51 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-05-05 11:40:59 | → | Guest78827 joins (~zmv@unaffiliated/zmv) |
| 2021-05-05 11:41:41 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 2021-05-05 11:44:32 | × | jneira quits (4f9b01f9@gateway/web/cgi-irc/kiwiirc.com/ip.79.155.1.249) (Ping timeout: 240 seconds) |
| 2021-05-05 11:45:01 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-05-05 11:45:38 | → | Codaraxis joins (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) |
| 2021-05-05 11:46:21 | × | bitmagie quits (~Thunderbi@200116b806538300bd7044d2c2250373.dip.versatel-1u1.de) (Quit: bitmagie) |
| 2021-05-05 11:48:12 | × | Codaraxis_ quits (~Codaraxis@ip68-5-90-227.oc.oc.cox.net) (Ping timeout: 240 seconds) |
| 2021-05-05 11:51:01 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2021-05-05 11:52:27 | × | cprofitt quits (~cprofitt@139.28.218.148) (Remote host closed the connection) |
| 2021-05-05 11:54:26 | × | rond_ quits (5940206b@89-64-32-107.dynamic.chello.pl) (Quit: Connection closed) |
| 2021-05-05 11:56:02 | × | oleks_ quits (~oleks@188.166.34.97) (Remote host closed the connection) |
| 2021-05-05 11:56:25 | → | oleks joins (~oleks@188.166.34.97) |
| 2021-05-05 11:56:43 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 2021-05-05 11:57:29 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 2021-05-05 11:57:54 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 2021-05-05 11:58:46 | × | mav1 quits (~mav@ip-88-152-11-229.hsi03.unitymediagroup.de) (Ping timeout: 240 seconds) |
| 2021-05-05 12:02:07 | → | rodriga joins (~quassel@134.204.25.66) |
| 2021-05-05 12:05:31 | <siers> | dminuoso, is agda more efficient with those? |
| 2021-05-05 12:05:59 | <dminuoso> | siers: Im not sure, but Idris is at least. |
| 2021-05-05 12:06:16 | <siers> | dminuoso, how is that achieved? |
| 2021-05-05 12:06:32 | → | Neuromancer joins (~Neuromanc@unaffiliated/neuromancer) |
| 2021-05-05 12:06:41 | <siers> | if you have any diea |
| 2021-05-05 12:06:47 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 268 seconds) |
| 2021-05-05 12:08:55 | Guest78827 | is now known as notzmv |
| 2021-05-05 12:08:59 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-05-05 12:09:43 | × | ADG1089 quits (~aditya@122.163.193.183) (Remote host closed the connection) |
| 2021-05-05 12:10:15 | × | Pickchea quits (~private@unaffiliated/pickchea) (Ping timeout: 252 seconds) |
| 2021-05-05 12:10:15 | × | knupfer quits (~Thunderbi@dynamic-046-114-150-034.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2021-05-05 12:10:52 | → | ogelbukh joins (~ogelbukh@185.163.110.100) |
| 2021-05-05 12:11:19 | <siers> | ok, I found a reddit post about it |
| 2021-05-05 12:11:22 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Ping timeout: 252 seconds) |
| 2021-05-05 12:13:41 | × | coot quits (~coot@37.30.58.122.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-05-05 12:13:41 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-05-05 12:14:11 | → | proteusguy joins (~proteusgu@cm-58-10-209-239.revip7.asianet.co.th) |
All times are in UTC.