Logs on 2022-02-09 (liberachat/#haskell)
| 00:00:59 | → | Clatters joins (~Clatters@host86-130-58-7.range86-130.btcentralplus.com) |
| 00:01:29 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 256 seconds) |
| 00:02:13 | → | foul_owl joins (~kerry@217.114.38.61) |
| 00:02:13 | <EvanR> | "jQuery is a monad" |
| 00:02:17 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 00:02:26 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 00:05:06 | × | Guest67 quits (~Guest67@host86-130-58-7.range86-130.btcentralplus.com) (Quit: Client closed) |
| 00:05:12 | × | Clatters quits (~Clatters@host86-130-58-7.range86-130.btcentralplus.com) (Client Quit) |
| 00:06:07 | → | Codaraxis__ joins (~Codaraxis@user/codaraxis) |
| 00:07:07 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 00:09:12 | × | LiaoTao quits (~LiaoTao@gateway/tor-sasl/liaotao) (Remote host closed the connection) |
| 00:09:26 | → | LiaoTao joins (~LiaoTao@gateway/tor-sasl/liaotao) |
| 00:10:02 | × | Codaraxis_ quits (~Codaraxis@user/codaraxis) (Ping timeout: 260 seconds) |
| 00:12:58 | → | Majiir joins (~majiir@pool-96-237-149-35.bstnma.fios.verizon.net) |
| 00:14:29 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 00:16:40 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dd3b:3d16:5046:6705) |
| 00:22:12 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 00:22:12 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 00:22:12 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:25:54 | × | max22- quits (~maxime@lfbn-ren-1-1026-62.w92-139.abo.wanadoo.fr) (Remote host closed the connection) |
| 00:26:06 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4) |
| 00:26:57 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 00:27:02 | × | ec quits (~ec@gateway/tor-sasl/ec) (Quit: ec) |
| 00:29:53 | × | Midjak quits (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Quit: This computer has gone to sleep) |
| 00:31:16 | → | deadmarshal joins (~deadmarsh@95.38.116.14) |
| 00:33:27 | × | jgeerds quits (~jgeerds@55d4a547.access.ecotel.net) (Ping timeout: 256 seconds) |
| 00:34:41 | × | vicfred quits (~vicfred@user/vicfred) (Quit: Leaving) |
| 00:35:17 | × | deadmarshal quits (~deadmarsh@95.38.116.14) (Ping timeout: 240 seconds) |
| 00:36:10 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 00:39:41 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 252 seconds) |
| 00:41:54 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 00:44:54 | → | mvk joins (~mvk@2607:fea8:5cdc:bf00::5483) |
| 00:46:59 | × | mmhat quits (~mmh@55d4b3be.access.ecotel.net) (Quit: WeeChat 3.4) |
| 00:48:26 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 00:48:41 | → | lavaman joins (~lavaman@98.38.249.169) |
| 00:48:48 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 00:53:55 | × | DNH quits (~DNH@2a02:8108:1100:16d8:30a6:9d4e:5fe4:7e50) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 01:04:42 | × | Codaraxis__ quits (~Codaraxis@user/codaraxis) (Ping timeout: 250 seconds) |
| 01:09:12 | × | jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
| 01:09:33 | → | jonathanx joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 01:10:35 | → | lavaman joins (~lavaman@98.38.249.169) |
| 01:11:17 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:48 | × | jlamothe quits (~jlamothe@198.251.61.229) (Ping timeout: 256 seconds) |
| 01:13:28 | × | lbseale_ quits (~ep1ctetus@user/ep1ctetus) (Quit: Leaving) |
| 01:14:33 | → | d34df00d joins (~d34df00d@2600:1700:8c60:3a10::48) |
| 01:14:37 | <d34df00d> | Hi! |
| 01:14:58 | <d34df00d> | What's up with pattern synonyms and coverage checker? |
| 01:15:57 | <d34df00d> | To be more precise, I had a `data Definition = Function Ty Arg | ...`, and I figured I want to refactor this into `data FunDef = FunDef Ty Arg; data Definition = Function FunDef | ...` |
| 01:17:05 | × | cynomys quits (~cynomys@user/cynomys) (Ping timeout: 256 seconds) |
| 01:17:20 | <d34df00d> | There's a lot of code that pattern-matches on Definition, so I thought adding `pattern Function ty arg <- Function (FunDef ty arg) where Function ty arg = Function (FunDef ty arg)` would help. |
| 01:17:23 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:00 | <d34df00d> | But now ghc complains pattern-matches are not exhaustive. |
| 01:18:05 | <d34df00d> | (ergh, replace one of the Function's with a different name to avoid clashes, but the idea is the same) |
| 01:18:20 | <d34df00d> | So, anyway, is there a way to convince ghc the matches are exhaustive? |
| 01:18:22 | <monochrom> | I haven't checked, but I wouldn't name-clash "Function" so many times. |
| 01:18:58 | <d34df00d> | Yep, let's assume Function as in the definition ctor is named differently. |
| 01:19:04 | <d34df00d> | In the real code the names are a lot uglier. |
| 01:19:55 | <monochrom> | And I would write like "pattern F ty arg = Function (FunDef ty arg)" for this obviously bidirectional pattern. |
| 01:21:15 | <d34df00d> | Well, it's still non-exhaustive. |
| 01:21:23 | <d34df00d> | But it's much nicer this way, thanks! |
| 01:21:58 | <geekosaur> | what ghc version? the coverage checker gets better with each version although there may be regressions in 9.2.1 which will hopefully be fixed in 9.2.2 |
| 01:22:12 | <jackdk> | also {-# COMPLETE #-} annotations are a thing |
| 01:22:25 | <d34df00d> | 8.10, sadly. |
| 01:23:18 | × | alp quits (~alp@user/alp) (Ping timeout: 260 seconds) |
| 01:27:05 | <d34df00d> | jackdk: thanks, {-# COMPLETE #-} does the trick! Ideally the compiler'd see the completeness itself, so let's hope I could remove this pragma when I will be able to upgrade to newer ghc versions. |
| 01:30:22 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 256 seconds) |
| 01:30:50 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 01:30:52 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dd3b:3d16:5046:6705) (Remote host closed the connection) |
| 01:38:55 | × | x_kuru quits (~xkuru@user/xkuru) (Read error: Connection reset by peer) |
| 01:38:59 | → | cynomys joins (~cynomys@user/cynomys) |
| 01:40:11 | × | Majiir quits (~majiir@pool-96-237-149-35.bstnma.fios.verizon.net) (Quit: Lost terminal) |
| 01:47:56 | × | chenqisu1 quits (~chenqisu1@183.217.200.249) (Ping timeout: 256 seconds) |
| 01:48:06 | → | ensyde joins (~ensyde@2600:1700:2050:1040::48) |
| 01:49:17 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds) |
| 01:56:33 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 02:00:37 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4) |
| 02:01:23 | → | lavaman joins (~lavaman@98.38.249.169) |
| 02:04:41 | × | xsperry quits (~xs@user/xsperry) (Remote host closed the connection) |
| 02:06:04 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 02:06:09 | × | xff0x quits (~xff0x@2001:1a81:533f:ea00:4e49:abcb:9c05:c4b8) (Ping timeout: 256 seconds) |
| 02:06:32 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dd3b:3d16:5046:6705) |
| 02:08:06 | → | xff0x joins (~xff0x@2001:1a81:537c:5300:675b:21ba:4e49:e802) |
| 02:08:37 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds) |
| 02:11:29 | × | neurocyte0917090 quits (~neurocyte@user/neurocyte) (Ping timeout: 256 seconds) |
| 02:13:59 | → | califax- joins (~califax@user/califx) |
| 02:17:09 | × | califax quits (~califax@user/califx) (Ping timeout: 276 seconds) |
| 02:17:10 | califax- | is now known as califax |
| 02:20:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 02:22:35 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 02:30:08 | → | fef joins (~thedawn@user/thedawn) |
| 02:32:51 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 02:42:23 | × | cynomys quits (~cynomys@user/cynomys) (Ping timeout: 250 seconds) |
| 02:50:07 | × | ober quits (~ober@c-73-68-74-41.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 02:51:13 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 02:56:34 | → | mbuf joins (~Shakthi@171.61.235.32) |
| 03:01:00 | → | k8yun joins (~k8yun@user/k8yun) |
| 03:02:17 | × | xff0x quits (~xff0x@2001:1a81:537c:5300:675b:21ba:4e49:e802) (Ping timeout: 240 seconds) |
| 03:04:17 | → | xff0x joins (~xff0x@2001:1a81:5384:400:cf7c:5041:a517:d608) |
| 03:06:32 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Ping timeout: 252 seconds) |
| 03:07:01 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds) |
| 03:07:30 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 03:12:29 | × | jao quits (~jao@static-68-235-44-10.cust.tzulo.com) (Remote host closed the connection) |
| 03:14:43 | × | fef quits (~thedawn@user/thedawn) (Quit: Leaving) |
| 03:16:18 | → | chenqisu1 joins (~chenqisu1@183.217.200.249) |
| 03:18:56 | → | jao joins (~jao@static-68-235-44-10.cust.tzulo.com) |
| 03:26:37 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 256 seconds) |
| 03:27:42 | → | cynomys joins (~cynomys@user/cynomys) |
| 03:28:12 | → | wavemode30 joins (~wavemode@2601:241:0:fc90:ed74:bac6:9a73:6e1a) |
| 03:28:53 | × | wavemode30 quits (~wavemode@2601:241:0:fc90:ed74:bac6:9a73:6e1a) (Client Quit) |
| 03:29:06 | × | wavemode quits (~wavemode@2601:241:0:fc90:1186:8dd8:ad8a:69e2) (Quit: Client closed) |
| 03:30:33 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 03:40:01 | → | wavemode joins (~wavemode@2601:241:0:fc90:ed74:bac6:9a73:6e1a) |
| 03:42:28 | × | terrorjack quits (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
| 03:43:30 | → | k8yun_ joins (~k8yun@user/k8yun) |
| 03:43:40 | → | terrorjack joins (~terrorjac@2a01:4f8:1c1e:509a::1) |
| 03:45:49 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 03:47:14 | × | k8yun quits (~k8yun@user/k8yun) (Ping timeout: 252 seconds) |
| 03:47:15 | × | td_ quits (~td@muedsl-82-207-238-149.citykom.de) (Ping timeout: 256 seconds) |
| 03:48:42 | → | td_ joins (~td@94.134.91.16) |
| 03:58:27 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 03:59:52 | × | ystael quits (~ystael@user/ystael) (Quit: Lost terminal) |
| 04:00:01 | × | haasn quits (~nand@haasn.dev) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 04:01:56 | → | haasn joins (~nand@haasn.dev) |
| 04:03:25 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds) |
| 04:06:01 | × | ensyde quits (~ensyde@2600:1700:2050:1040::48) (Ping timeout: 250 seconds) |
| 04:08:18 | × | wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 276 seconds) |
| 04:14:54 | → | wyrd joins (~wyrd@gateway/tor-sasl/wyrd) |
| 04:15:24 | × | burnsidesLlama quits (~burnsides@dhcp168-036.wadham.ox.ac.uk) (Remote host closed the connection) |
| 04:15:56 | → | burnsidesLlama joins (~burnsides@client-8-95.eduroam.oxuni.org.uk) |
| 04:20:07 | × | burnsidesLlama quits (~burnsides@client-8-95.eduroam.oxuni.org.uk) (Ping timeout: 256 seconds) |
| 04:21:07 | → | lavaman joins (~lavaman@98.38.249.169) |
| 04:22:04 | → | dajoer joins (~david@user/gvx) |
| 04:25:47 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 04:26:00 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 04:26:28 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 04:27:50 | → | caubert_ joins (~caubert@136.244.111.235) |
| 04:28:16 | → | deadmarshal joins (~deadmarsh@95.38.116.14) |
| 04:28:57 | × | caubert quits (~caubert@136.244.111.235) (Ping timeout: 240 seconds) |
| 04:32:04 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:34:00 | × | k8yun_ quits (~k8yun@user/k8yun) (Ping timeout: 250 seconds) |
| 04:34:34 | × | modnar quits (~modnar@shell.sonic.net) (Quit: No Ping reply in 180 seconds.) |
| 04:36:05 | → | lavaman joins (~lavaman@98.38.249.169) |
| 04:37:16 | → | modnar joins (~modnar@shell.sonic.net) |
| 04:46:03 | → | sebastiandb joins (~sebastian@2620:0:5301:2101:1fb2:b569:b87b:10e9) |
| 05:02:03 | × | chenqisu1 quits (~chenqisu1@183.217.200.249) (Ping timeout: 256 seconds) |
| 05:06:03 | × | vysn quits (~vysn@user/vysn) (Ping timeout: 250 seconds) |
| 05:07:51 | × | wavemode quits (~wavemode@2601:241:0:fc90:ed74:bac6:9a73:6e1a) (Quit: Client closed) |
| 05:08:21 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 05:14:10 | → | wavemode joins (~wavemode@2601:241:0:fc90:2892:d0:a7ec:bc11) |
| 05:19:01 | → | ksqsf joins (~user@134.209.106.31) |
| 05:19:23 | <ksqsf> | Is there a stack command that prints the resolver of the current project? |
| 05:21:02 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 05:22:13 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 05:24:20 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 05:24:32 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 05:28:27 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 05:31:50 | <dsal> | The resolver can be a file path or URL. I don't know if there's a commandline way to do it offhand, but it might be confusing. |
| 05:33:06 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 05:33:06 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 05:33:06 | → | wroathe joins (~wroathe@user/wroathe) |
| 05:33:47 | × | deadmarshal quits (~deadmarsh@95.38.116.14) (Ping timeout: 256 seconds) |
| 05:37:26 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds) |
| 05:37:27 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 05:38:34 | × | sebastiandb quits (~sebastian@2620:0:5301:2101:1fb2:b569:b87b:10e9) (Ping timeout: 260 seconds) |
| 05:40:55 | × | jao quits (~jao@static-68-235-44-10.cust.tzulo.com) (Ping timeout: 256 seconds) |
| 05:44:30 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 05:47:40 | <koala_man> | hey I'm looking at the "infinite loops" section at the bottom of https://wiki.haskell.org/Debugging but I can't reproduce it. Does anyone know if this still works? |
| 05:48:26 | <koala_man> | or any other convenient way to track down an infinite loop |
| 05:49:02 | <jackdk> | call smaller and smaller parts of your program - if the small part doesn't infinitely loop, the loop is in the part you left our |
| 05:49:05 | <jackdk> | out* |
| 05:49:59 | <Axman6> | Debug.Trace can be useful too, if you have: loop some args = ..., you can do loop some args | trace ("loop",some,args) False = undefined; | otherwise = ... |
| 05:50:35 | <koala_man> | jackdk: due to laziness this is not the case |
| 05:51:44 | <modnar> | ksqsf: perhaps? grep -A2 "^resolver:" stack.yaml |
| 05:53:39 | <ephemient> | might not be on the same line since it's yaml. `python -c 'import yaml;print(yaml.load(open("stack.yaml"))["resolver"])' would reliably get the right stanza but as mentioned above, it could be a name or a path or a url... |
| 06:00:08 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 06:09:08 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 06:13:25 | × | HotblackDesiato quits (~HotblackD@gateway/tor-sasl/hotblackdesiato) (Remote host closed the connection) |
| 06:13:46 | → | HotblackDesiato joins (~HotblackD@gateway/tor-sasl/hotblackdesiato) |
| 06:14:30 | × | ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 06:15:27 | <koala_man> | I build my executable with profiling, but I'm not getting any results when I ctrl-c it. Is there anything I can do about that? |
| 06:16:13 | <Axman6> | what have you actually done? |
| 06:16:43 | <koala_man> | `cabal build -p` followed by `myexe +RTS -p` |
| 06:16:56 | <Axman6> | but what have you done to your code |
| 06:16:58 | <koala_man> | also --enable-profiling |
| 06:17:26 | <Axman6> | Keep in mind that that page you liked to is from the GHC 6 era, and a lot of it is probably pretty useless |
| 06:17:40 | <koala_man> | not sure what you mean. I've made extensive modifications to it? |
| 06:18:14 | <Axman6> | I suggested you make sone changes to your code to make it easier to see what's going on, did you try that? |
| 06:18:40 | <koala_man> | I'm very familiar with trace debugging, I'm just tired of doing it every time |
| 06:23:24 | <ephemient> | compile with ghc -prof -fprof-auto for some default {-# SCC #-} everywhere, run with +RTS -xc to include stack traces… should work but I always had a better time breaking things down into smaller testable components then using quickcheck or Debug.Trace |
| 06:31:44 | <koala_man> | ephemient: I'm not getting a stack trace, but Ctrl-C only kills it the second time so maybe the handler gets stuck |
| 06:33:31 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 06:33:31 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 06:33:31 | → | wroathe joins (~wroathe@user/wroathe) |
| 06:33:31 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 06:33:49 | → | gentauro joins (~gentauro@user/gentauro) |
| 06:34:17 | × | Inst quits (~delicacie@2601:6c4:4080:3f80:6cf2:b906:2bc7:1ff9) (Ping timeout: 240 seconds) |
| 06:35:33 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 06:36:18 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 06:37:15 | × | bliminse quits (~bliminse@host86-188-36-166.range86-188.btcentralplus.com) (Ping timeout: 256 seconds) |
| 06:37:27 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 06:37:39 | → | chenqisu1 joins (~chenqisu1@183.217.200.249) |
| 06:38:06 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 06:38:38 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 06:38:51 | → | bliminse joins (~bliminse@host86-158-241-239.range86-158.btcentralplus.com) |
| 06:41:36 | → | Inst joins (~delicacie@2601:6c4:4080:3f80:1d81:9f23:5ac8:407a) |
| 06:41:46 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 06:43:10 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 06:53:26 | × | echoreply quits (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 06:54:44 | → | echoreply joins (~echoreply@2001:19f0:9002:1f3b:5400:ff:fe6f:8b8d) |
| 06:59:12 | <koala_man> | ephemient: hah, I started the operation in a forkIO and killed the thread after a delay. it showed a stack trace that was at least close |
| 07:02:04 | × | little_mac quits (~little_ma@2601:410:4300:3ce0:c1b4:4e62:c0e4:304a) (Remote host closed the connection) |
| 07:02:21 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 07:02:26 | × | superbil quits (~superbil@1-34-176-171.hinet-ip.hinet.net) (Ping timeout: 256 seconds) |
| 07:04:38 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 07:04:52 | → | lavaman joins (~lavaman@98.38.249.169) |
| 07:05:00 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 07:05:16 | → | superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net) |
| 07:05:32 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 07:05:45 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 07:10:50 | → | michalz joins (~michalz@185.246.204.93) |
| 07:11:14 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 07:12:32 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 07:13:22 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 07:14:02 | → | alp joins (~alp@user/alp) |
| 07:16:41 | → | dschrempf joins (~dominik@mobiledyn-62-240-134-126.mrsn.at) |
| 07:18:14 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Ping timeout: 250 seconds) |
| 07:18:34 | → | phma_ joins (~phma@2001:5b0:211f:d758:6f18:ab28:6bcc:58fd) |
| 07:18:34 | × | phma quits (phma@2001:5b0:211f:7e68:f18f:96de:b488:61b7) (Read error: Connection reset by peer) |
| 07:19:03 | → | deadmarshal joins (~deadmarsh@95.38.116.14) |
| 07:19:11 | × | dschrempf quits (~dominik@mobiledyn-62-240-134-126.mrsn.at) (Client Quit) |
| 07:22:07 | → | Jing joins (~hedgehog@240e:390:7c53:a7e1:dc0:c5aa:294f:7621) |
| 07:25:11 | × | n3rdy1 quits (~n3rdy1@2600:1700:4570:3480:1b88:50f:dae0:9293) (Ping timeout: 256 seconds) |
| 07:27:05 | → | cosimone joins (~user@93-34-133-254.ip49.fastwebnet.it) |
| 07:29:06 | × | LiaoTao quits (~LiaoTao@gateway/tor-sasl/liaotao) (Remote host closed the connection) |
| 07:30:02 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 07:31:33 | → | LiaoTao joins (~LiaoTao@gateway/tor-sasl/liaotao) |
| 07:32:14 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 07:32:45 | <dminuoso> | koala_man: Last I checked it worked, yes. |
| 07:32:58 | → | zeenk joins (~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5) |
| 07:34:04 | phma_ | is now known as phma |
| 07:34:08 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 07:35:32 | → | lavaman joins (~lavaman@98.38.249.169) |
| 07:36:53 | → | zaquest joins (~notzaques@5.130.79.72) |
| 07:39:49 | → | MajorBiscuit joins (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 07:39:50 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 07:44:39 | × | MajorBiscuit quits (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 250 seconds) |
| 07:44:55 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 07:45:56 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 07:46:04 | → | MajorBiscuit joins (~MajorBisc@c-001-013-035.client.tudelft.eduvpn.nl) |
| 07:47:25 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:48:41 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 07:54:12 | → | chele joins (~chele@user/chele) |
| 07:54:53 | × | cynomys quits (~cynomys@user/cynomys) (Ping timeout: 256 seconds) |
| 07:55:11 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 07:55:24 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 07:55:40 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 07:56:13 | → | sektor|3 joins (~kvirc@94.155.193.66) |
| 07:57:54 | → | max22- joins (~maxime@2a01cb088335980044f7b68859555b87.ipv6.abo.wanadoo.fr) |
| 07:58:09 | → | vysn joins (~vysn@user/vysn) |
| 07:58:52 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:59:25 | × | sektor|2 quits (~kvirc@87.227.175.182) (Ping timeout: 256 seconds) |
| 08:00:13 | × | michalz quits (~michalz@185.246.204.93) (Remote host closed the connection) |
| 08:00:37 | × | ksqsf quits (~user@134.209.106.31) (Ping timeout: 240 seconds) |
| 08:02:58 | → | ksqsf joins (~user@134.209.106.31) |
| 08:05:20 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 08:06:47 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:cb78:26c4:6167:fc4) |
| 08:07:27 | → | elkcl joins (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 08:07:29 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 08:08:03 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 250 seconds) |
| 08:10:08 | → | AlexisTP joins (~AlexisTP3@92.57.44.63) |
| 08:11:25 | × | AlexisTP quits (~AlexisTP3@92.57.44.63) (Client Quit) |
| 08:11:45 | → | AlexisTP joins (~AlexisTP3@92.57.44.63) |
| 08:12:27 | × | hgolden quits (~hgolden2@cpe-172-114-81-123.socal.res.rr.com) (Ping timeout: 256 seconds) |
| 08:12:37 | × | ksqsf quits (~user@134.209.106.31) (Ping timeout: 240 seconds) |
| 08:13:01 | × | Akiva quits (~Akiva@user/Akiva) (Ping timeout: 256 seconds) |
| 08:13:53 | × | AlexisTP quits (~AlexisTP3@92.57.44.63) (Client Quit) |
| 08:14:11 | → | AlexisTP joins (~AlexisTP3@92.57.44.63) |
| 08:15:40 | × | AlexisTP quits (~AlexisTP3@92.57.44.63) (Client Quit) |
| 08:16:03 | → | AlexisTP joins (~AlexisTP@92.57.44.63) |
| 08:16:45 | → | hgolden joins (~hgolden2@cpe-172-114-81-123.socal.res.rr.com) |
| 08:17:36 | → | ksqsf joins (~user@134.209.106.31) |
| 08:17:59 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dd3b:3d16:5046:6705) (Remote host closed the connection) |
| 08:19:02 | → | michalz joins (~michalz@185.246.204.65) |
| 08:22:07 | × | ksqsf quits (~user@134.209.106.31) (Ping timeout: 250 seconds) |
| 08:22:11 | → | dhouthoo joins (~dhouthoo@178-117-36-167.access.telenet.be) |
| 08:24:57 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 08:25:32 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 240 seconds) |
| 08:25:44 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 08:28:51 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 08:31:20 | → | ksqsf joins (~user@134.209.106.31) |
| 08:33:25 | × | foul_owl quits (~kerry@217.114.38.61) (Ping timeout: 256 seconds) |
| 08:34:17 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 08:34:17 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 08:34:17 | → | wroathe joins (~wroathe@user/wroathe) |
| 08:34:29 | → | Pickchea joins (~private@user/pickchea) |
| 08:37:20 | <elkcl> | hi! I recently saw someone implement a function that checks if a list is a palindrome like this: |
| 08:37:20 | <elkcl> | isPalindrome = (==) <*> reverse |
| 08:37:20 | <elkcl> | I was trying to figure out how it works and after fooling around with type signatures it appears that (a ->) gets substituted in (Applicative f). My question is: how the hell does this work? I always thought -> was some special syntax, but here it works like a parametric type or something? Sorry if it's an absolute beginner question, but I could find any info |
| 08:37:38 | <elkcl> | *couldn't find any info about this |
| 08:39:16 | → | Tuplanolla joins (~Tuplanoll@91-159-68-166.elisa-laajakaista.fi) |
| 08:39:16 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
| 08:41:17 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 08:43:43 | <[exa]> | elkcl: you're right, this is a result of `instance Applicative ((->) r)` |
| 08:45:05 | <[exa]> | anyway it's not an absolute beginner question, I'll need to have a look at how this actually decomposes too :D |
| 08:45:32 | <[exa]> | did you work with some other applicatives |
| 08:45:45 | <[exa]> | ...for example this: |
| 08:45:54 | <[exa]> | > (+) <$> Just 3 <*> Just 5 |
| 08:45:55 | <lambdabot> | Just 8 |
| 08:46:11 | → | RFV joins (~Thunderbi@243.red-88-5-247.dynamicip.rima-tde.net) |
| 08:47:01 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 08:47:26 | <elkcl> | Yeah, I more or less understand how applicatives work in general, what confused me was (->) behaving like a parametric type |
| 08:47:40 | <[exa]> | yeah, well, it is. :D |
| 08:49:02 | <[exa]> | the instance is here: https://hackage.haskell.org/package/base-4.16.0.0/docs/src/GHC.Base.html#line-1007 |
| 08:49:44 | <[exa]> | in short, (p ->) forms a proper functor, you may imagine it as a "box for a result that requires a parameter of type `p` to get a result" |
| 08:51:07 | <[exa]> | > (+1) 3 -- example: (+1) is a box for a result, and we get the result by giving it the parameter |
| 08:51:08 | <lambdabot> | 4 |
| 08:51:43 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.3) |
| 08:51:45 | <[exa]> | > ((*2) <$> (+1)) 3 -- example 2: we multiply whatever is in the box by 2, then get it out of a box (and pretend the 3 was there even before :D ) |
| 08:51:46 | <lambdabot> | 8 |
| 08:52:31 | <[exa]> | applicative in this works similarly, you combine the boxes as with other applicative "containers", and when you finally supply the parameter, it gets sent to all boxes |
| 08:53:03 | <[exa]> | (if you worked with combinators, you might notice from the definition that <*> is perfectly equivalent to S combinator) |
| 08:53:31 | <[exa]> | so let's make a bit of an allegory with simpler applicatives: |
| 08:53:49 | <[exa]> | > (+) <$> Just 3 <*> Just 7 |
| 08:53:50 | <lambdabot> | Just 10 |
| 08:53:59 | → | cynomys joins (~cynomys@user/cynomys) |
| 08:54:07 | <[exa]> | :t (+) <$> (+3) <*> (+7) |
| 08:54:08 | <lambdabot> | Num b => b -> b |
| 08:54:21 | <[exa]> | > ( (+) <$> (+3) <*> (+7) ) 1 |
| 08:54:23 | <lambdabot> | 12 |
| 08:54:37 | × | AlexisTP quits (~AlexisTP@92.57.44.63) (Ping timeout: 250 seconds) |
| 08:54:48 | × | shriekingnoise quits (~shrieking@201.231.16.156) (Quit: Quit) |
| 08:55:09 | → | kuribas joins (~user@ptr-25vy0i7qdirbfvrk27x.18120a2.ip6.access.telenet.be) |
| 08:55:18 | <[exa]> | (basically rewrites to `(+) ((+3) 1) ((+7) 1)` ) |
| 08:55:56 | <[exa]> | in your case, the parameter "broadcasting" works the same way, although the parameter is not explicitly there |
| 08:57:03 | <[exa]> | `isPalindrome p = ((==) <*> reverse) p` is basically equivalent to `p` getting sent to all boxes in the applicative expression, in this case: `isPalindrome p = ((==) p) (reverse p)` |
| 08:59:02 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:00:37 | × | ishutin quits (~ishutin@80-95-86-56.pool.digikabel.hu) (Ping timeout: 256 seconds) |
| 09:01:43 | <elkcl> | woah, thanks, I think I get it now |
| 09:01:43 | <elkcl> | Does that also mean that all type signatures are just "applications" of parametric types then? I thought -> was special, but looks like the only special thing about it is being an infix operator |
| 09:01:43 | <elkcl> | Can I define my own "infix types" by the way? |
| 09:02:04 | <[exa]> | anyway, this allows a really nice form of passing "global parameters" to whole computations, people usually call it "Reader style", there's whole Reader monad for that purpose, which does roughly the same thing. Might be a nice intuition to have a look at it |
| 09:02:25 | → | ishutin joins (~ishutin@193-110-63-21.cable-modem.hdsnet.hu) |
| 09:02:59 | <Axman6> | % type a ~~> b = (a,a) -> (b,b) |
| 09:03:01 | <yahb> | Axman6: |
| 09:03:37 | <Axman6> | % both :: a -> b -> (a ~~> b); both f (x,y) = (f x, f y) |
| 09:03:37 | <yahb> | Axman6: ; <interactive>:2:45: error:; * Couldn't match type: (b0, b0); with: (a, a) -> (b, b); Expected: a ~~> b; Actual: (b0, b0); * In the expression: (f x, f y); In an equation for `both': both f (x, y) = (f x, f y); * Relevant bindings include; f :: a (bound at <interactive>:2:35); both :: a -> b -> a ~~> b (bound at <interactive>:2:30) |
| 09:03:53 | <Axman6> | % both :: (a -> b) -> (a ~~> b); both f (x,y) = (f x, f y) |
| 09:03:53 | <yahb> | Axman6: |
| 09:04:02 | <Axman6> | % both show (1,2) |
| 09:04:02 | <yahb> | Axman6: ("1","2") |
| 09:04:26 | <[exa]> | elkcl: technically (->) is not special at all, just a normal type with 2 parameters and sligtly complicated representation at runtime |
| 09:04:45 | <lortabac> | (->) is special because it's built-in |
| 09:04:58 | <[exa]> | infix types are AFAIK possible but you need to prefix them with `:` or something, not sure |
| 09:05:19 | × | jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
| 09:05:32 | <lortabac> | infix types are possible but you have to enable TypeOperators |
| 09:06:09 | <lortabac> | and yes, prefix them with (:) |
| 09:06:27 | <[exa]> | wow, TypeOperators doesn't even need the : prefix |
| 09:06:39 | <ski> | they used to |
| 09:06:48 | <[exa]> | still it's a very useful distinction to keep. |
| 09:07:02 | <lortabac> | oh I didn't know, I thought only type families were allowed without : |
| 09:07:49 | <lortabac> | data constructors still require the :, right? |
| 09:08:10 | <[exa]> | yes, seems so |
| 09:08:17 | <[exa]> | (phew..!) |
| 09:08:40 | <ski> | % data (f <+> g) a = Left1 (f a) | Right1 (g a) |
| 09:08:40 | <yahb> | ski: |
| 09:09:17 | → | ardell joins (~ardell@user/ardell) |
| 09:09:29 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 09:11:17 | <ski> | you used to be able to say `graph :: Arrow (~>) => (a ~ b) -> (a ~> (a,b)); graph f = arr id &&& f; cograph :: ArrowChoice (~>) => (a ~> b) -> (Either a b ~> b); cograph f = f ||| arr id' |
| 09:11:56 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:12:53 | → | jco joins (~jco@90-228-194-139-no542.tbcn.telia.com) |
| 09:13:57 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Ping timeout: 240 seconds) |
| 09:14:18 | <ski> | (`(~>)' there being a type variable .. just like you can say `on :: (b -> b -> c) -> (a -> b) -> (a -> a -> c); ((+) `on` f) x y = f x + f y', where `(+)' is a variable) |
| 09:14:42 | × | RFV quits (~Thunderbi@243.red-88-5-247.dynamicip.rima-tde.net) (Quit: RFV) |
| 09:15:26 | <jco> | I'm using Emacs, LSP, and company-mode. Is there a way to disable the feature that when autocompleting, the arguments to a function are also completed (i.e. their types are added after the function name). I'd only want the function name itself to be inserted as a result of selecting the completion candidate. |
| 09:17:25 | → | jonathanx joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 09:18:31 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 256 seconds) |
| 09:18:57 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 09:19:16 | → | xsperry joins (~xs@user/xsperry) |
| 09:23:27 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 250 seconds) |
| 09:25:11 | <elkcl> | ah, so it's possible with a ghc extension, cool |
| 09:25:11 | <elkcl> | ok, thanks everyone |
| 09:25:14 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 09:25:26 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 09:25:49 | → | zer0bitz joins (~zer0bitz@2001:2003:f74d:b800:2df2:1ec5:8dd3:29f0) |
| 09:26:13 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 09:27:53 | → | InternetCitizen joins (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) |
| 09:28:09 | <InternetCitizen> | any ideas why llvm-hs is stuck on 9.0? |
| 09:28:40 | <InternetCitizen> | even at upstream all I could find was an llvm-12 dev branch, and last release was in 2019 |
| 09:30:14 | <InternetCitizen> | is the C API extension proving too costly to maintain? or is there very little interest in building LLVM-backed compilers in Haskell |
| 09:33:04 | <[exa]> | maintenance ain't easy I'd say |
| 09:34:59 | <merijn> | LLVM is a nightmare beast of Lovecraftian horror :p |
| 09:35:26 | <InternetCitizen> | I just find it odd since the OCaml bindings are up to date and I always imagined the Haskell community to be bigger |
| 09:35:54 | <[exa]> | related: https://github.com/llvm-hs/llvm-hs/issues/364 |
| 09:36:50 | <merijn> | So, the answer is: the ocaml bindings aren't up to date either :p |
| 09:39:09 | <InternetCitizen> | ? apparently they're part of the llvm project |
| 09:39:31 | <InternetCitizen> | "Our FFI layer directly provides bindings to things that the C API doesn't expose, in addition to wrapping the C API for other things, so we have a decently large maintenance burden when something changes." |
| 09:39:42 | → | `2jt joins (~jtomas@130.red-88-22-46.staticip.rima-tde.net) |
| 09:39:57 | <[exa]> | that's one way to make maintenance hard, yes. |
| 09:39:58 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 09:40:13 | <merijn> | InternetCitizen: Yeah, but that llvm-hs issue mentions that Ocaml only supports the C interface and thus not all of LLVM's functionality |
| 09:40:31 | <[exa]> | isn't there some kind of simpler project that would just c2hs the whole thing? |
| 09:40:32 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 09:40:42 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 09:41:00 | <InternetCitizen> | merijn: ah yes of course, but that's standard practice in llvm bindings, most languages only wrap the C API |
| 09:41:19 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 09:41:25 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 09:41:43 | <InternetCitizen> | llvm-hs is unique in this regard and the reason I was interested in it |
| 09:42:20 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 09:43:30 | × | chenqisu1 quits (~chenqisu1@183.217.200.249) (Remote host closed the connection) |
| 09:43:37 | × | cynomys quits (~cynomys@user/cynomys) (Quit: Lost terminal) |
| 09:43:48 | × | vglfr quits (~vglfr@coupling.penchant.volia.net) (Read error: Connection reset by peer) |
| 09:43:56 | <merijn> | Right, but that alone would explain why llvm-hs is so much more work to maintain :) |
| 09:44:00 | → | vglfr joins (~vglfr@coupling.penchant.volia.net) |
| 09:44:04 | → | AlexisTP joins (~AlexisTP@92.57.44.63) |
| 09:44:20 | <merijn> | Wrapping C APIs in haskell? Easy peasy! Barely an inconvenience! |
| 09:44:36 | <merijn> | Wrapping C++ APIs in anything (including Haskell)? Please just kill me now |
| 09:45:09 | <merijn> | I would 100% rather stab myself in the leg than wrap C++ code in another language |
| 09:45:17 | <merijn> | At least the pain of stabs is temporary... |
| 09:49:02 | [exa] | mixes in some random macros and templates |
| 09:50:07 | → | wroathe joins (~wroathe@user/wroathe) |
| 09:50:44 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 09:52:04 | → | chenqisu1 joins (~chenqisu1@183.217.200.249) |
| 09:53:01 | × | chenqisu1 quits (~chenqisu1@183.217.200.249) (Max SendQ exceeded) |
| 09:53:28 | → | chenqisu1 joins (~chenqisu1@183.217.200.249) |
| 09:53:55 | → | lavaman joins (~lavaman@98.38.249.169) |
| 09:55:16 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 09:55:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 09:55:38 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 09:55:45 | <tomsmeding> | I wonder if it wouldn't be better for llvm-hs (if only for publicity) if they would just release now, even without full support |
| 09:56:22 | <tomsmeding> | at least then you have a higher chance of people using it, running into limitations (perhaps, if at all), and having a bit of time to help completing functionality (perhaps) |
| 09:56:23 | <[exa]> | reflecting on whether "full support" of LLVM is even achievable in the long term could help, yes |
| 09:56:40 | <tomsmeding> | rather, whether full support is necessary to even cut a first release |
| 09:57:49 | <kuribas> | merijn: wrap it in C, then wrap the C in haskell? |
| 09:57:57 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 09:58:16 | → | ubert joins (~Thunderbi@p200300ecdf0994700e1bfcbc5fe04b55.dip0.t-ipconnect.de) |
| 09:59:58 | → | samtoth joins (~igloo@90.208.227.189) |
| 10:00:20 | <tomsmeding> | InternetCitizen: just for completeness' sake, that llvm-12 dev branch is working perfectly well, it just doesn't have full support for all the new stuff introduced in llvm 12 |
| 10:04:35 | → | marinelli joins (~marinelli@gateway/tor-sasl/marinelli) |
| 10:05:39 | × | marinelli quits (~marinelli@gateway/tor-sasl/marinelli) (Client Quit) |
| 10:06:13 | × | vysn quits (~vysn@user/vysn) (Ping timeout: 240 seconds) |
| 10:08:57 | × | ksqsf quits (~user@134.209.106.31) (Ping timeout: 256 seconds) |
| 10:10:52 | → | DNH joins (~DNH@2a02:8108:1100:16d8:adf2:7fd4:5ba2:8512) |
| 10:13:09 | × | InternetCitizen quits (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) (Ping timeout: 256 seconds) |
| 10:15:34 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 10:18:41 | → | akegalj joins (~akegalj@141-136-168-212.dsl.iskon.hr) |
| 10:20:52 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 10:20:52 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 10:20:52 | → | wroathe joins (~wroathe@user/wroathe) |
| 10:21:25 | × | Tuplanolla quits (~Tuplanoll@91-159-68-166.elisa-laajakaista.fi) (Ping timeout: 240 seconds) |
| 10:24:44 | → | fvr joins (uid503686@id-503686.uxbridge.irccloud.com) |
| 10:25:57 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 10:27:31 | → | rusrushal13 joins (~rusrushal@2405:201:7003:8952:a27c:c592:8e19:8656) |
| 10:29:25 | × | samtoth quits (~igloo@90.208.227.189) (Ping timeout: 240 seconds) |
| 10:30:03 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 10:30:05 | → | jamesmartinez joins (~pepsi@2a02:4780:1:1::1:a856) |
| 10:31:32 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 10:31:36 | → | Codaraxis joins (~Codaraxis@user/codaraxis) |
| 10:31:53 | × | Codaraxis quits (~Codaraxis@user/codaraxis) (Client Quit) |
| 10:33:12 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 10:34:55 | → | Tuplanolla joins (~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) |
| 10:36:05 | → | xkuru joins (~xkuru@user/xkuru) |
| 10:40:06 | ← | jamesmartinez parts (~pepsi@2a02:4780:1:1::1:a856) (WeeChat 1.9.1) |
| 10:40:46 | → | Gurkenglas_ joins (~Guest22@dslb-188-096-121-068.188.096.pools.vodafone-ip.de) |
| 10:41:44 | × | akegalj quits (~akegalj@141-136-168-212.dsl.iskon.hr) (Ping timeout: 256 seconds) |
| 10:41:53 | <Gurkenglas_> | Can GADTs be seen as merely sugar for a transformation like this one? https://gist.github.com/Gurkenglas/137914f5790f0e0390c631f9678832da because it looks more powerful than GADTs are |
| 10:42:01 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 10:42:17 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Ping timeout: 240 seconds) |
| 10:42:42 | → | safinaskar joins (~quassel@109.252.91.116) |
| 10:44:08 | <Gurkenglas_> | (edited in fits and bursts a little just now, reload if it doesn't look like it'd compile.) |
| 10:44:10 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 10:45:32 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 10:46:04 | <Gurkenglas_> | Also, is there a library that provides as-close-as-we-can-get-to type-level lambdas? |
| 10:47:04 | <lortabac> | @hackage first-class-families |
| 10:47:04 | <lambdabot> | https://hackage.haskell.org/package/first-class-families |
| 10:47:19 | <lortabac> | or if you are brave enough, singletons |
| 10:47:28 | <lortabac> | @hackage singletons |
| 10:47:28 | <lambdabot> | https://hackage.haskell.org/package/singletons |
| 10:48:11 | <Gurkenglas_> | Thanks! This must've been what value-level lambdas must have looked like 40 years ago :3 |
| 10:48:12 | <kuribas> | Gurkenglas_: no, that looks weird. |
| 10:48:28 | <kuribas> | Gurkenglas_: what is `f`? |
| 10:48:47 | ← | safinaskar parts (~quassel@109.252.91.116) () |
| 10:48:49 | × | tiferrei quits (~tiferrei@user/tiferrei) (Remote host closed the connection) |
| 10:48:56 | <Gurkenglas_> | kuribas, universally quantified! |
| 10:49:37 | <lortabac> | Gurkenglas_: http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/ |
| 10:49:43 | <Gurkenglas_> | kuribas, you mean, "GADTs can't been seen as merely sugar for that because that looks weird"? |
| 10:50:16 | <lortabac> | Gurkenglas_: your encoding looks very similar to the one described in the post |
| 10:50:22 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 10:50:34 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 10:51:40 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 10:51:40 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 10:51:40 | → | wroathe joins (~wroathe@user/wroathe) |
| 10:52:40 | <kuribas> | Gurkenglas_: I mean, what do you plug in that `f`? |
| 10:52:43 | <kuribas> | Identity? |
| 10:54:10 | × | kilolympus quits (~kilolympu@31.205.200.235) (Quit: Quitting IRC :() |
| 10:55:19 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 10:55:25 | <Gurkenglas_> | kuribas, whatever you need at the time. to get the string out of Foo2 (\bar baz -> baz "asd"), I suppose you could do runIdentity $ runFoo (\bar baz -> baz "asd") error Identity |
| 10:55:48 | <Gurkenglas_> | -error+undefined |
| 10:56:28 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 10:56:47 | <kuribas> | Gurkenglas_: what if it is just a phantom variable? |
| 10:56:55 | <kuribas> | phantom type... |
| 10:57:43 | <Gurkenglas_> | kuribas, then you won't have much luck passing anything to the output of runFoo! |
| 10:58:09 | <kuribas> | indeed, but phantom types are supported by GADTs. |
| 10:59:01 | <Gurkenglas_> | maybe i misunderstood? give me something that GADTs can do with this that my thing can't. |
| 10:59:30 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 11:00:06 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 11:00:43 | <Gurkenglas_> | *googles around* i guessed phantom type means, type without values. if it just means, f a is the same as f b, then there's no problem |
| 11:00:50 | Lord_of_Life_ | is now known as Lord_of_Life |
| 11:01:42 | <Gurkenglas_> | 'runConst $ runFoo (\bar baz -> baz "asd") undefined Const' will also get the string out. |
| 11:01:43 | <merijn> | Gurkenglas_: A phantom type is one without a body (i.e. it only exists in the type, not in the value) |
| 11:02:12 | <merijn> | As in "data Const a b = Const a" 'b' is a phantom type, 'cos no "body" (value) |
| 11:03:22 | <Gurkenglas_> | Okay. So kuribas, what do you mean by f being phantom? it's not appears-left-but-not-right, it's appears-right-but-not-left. |
| 11:03:36 | <kuribas> | yes |
| 11:04:34 | <Gurkenglas_> | You're going to have to give me more than yes! :D |
| 11:04:46 | <kuribas> | I'll have a look later... |
| 11:04:58 | <kuribas> | I have work to do. |
| 11:06:02 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 11:06:16 | → | califax joins (~califax@user/califx) |
| 11:11:29 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 11:11:43 | → | jgeerds joins (~jgeerds@55d4a547.access.ecotel.net) |
| 11:11:53 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 11:17:36 | <Gurkenglas_> | lortabac, that post does something quite different from me, i think - i don't expect any type equality problems. '(\foo2 -> runIdentity $ runFoo2 foo2 Identity Identity) :: Foo2 a -> a' works fine |
| 11:17:54 | <lottaquestions_> | Hi all new guy here |
| 11:18:09 | <lottaquestions_> | How does one create a cabal sandbox? |
| 11:18:43 | <geekosaur> | you don't any more, modern cabal automatically sandboxes |
| 11:19:20 | <Gurkenglas_> | I fear thinking about cabal directly indicates something unusual already? I would install https://docs.haskellstack.org/en/stable/README/ |
| 11:20:06 | <byorgey> | There's nothing wrong with using cabal directly. stack is nice too. It depends on the use case. |
| 11:20:43 | <maerwald> | geekosaur: no it doesn't |
| 11:20:45 | × | wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Remote host closed the connection) |
| 11:20:48 | <lottaquestions_> | I am new to this whole thing and my mentor suggested Doom Emacs and nixos |
| 11:20:59 | → | wyrd joins (~wyrd@gateway/tor-sasl/wyrd) |
| 11:21:05 | <lottaquestions_> | But I want to get to the coding part of the language quickly |
| 11:21:06 | <maerwald> | to emulate sandboxes you have to run: cabal --store-dir=$(pwd)/.sandbox build |
| 11:21:09 | <maerwald> | for example |
| 11:21:16 | <lottaquestions_> | with minimal setup |
| 11:21:22 | <Gurkenglas_> | lortabac, singletons only if brave because it's powerful-but-more-scary in its... likelihood to throw me hard-to-interpret errors? |
| 11:22:10 | <Gurkenglas_> | lottaquestions_, do you use some sort of IDE, like VSCode, or more something like notepad |
| 11:22:11 | → | foul_owl joins (~kerry@23.82.193.78) |
| 11:22:24 | <lottaquestions_> | I am an emacs guy |
| 11:22:39 | <lottaquestions_> | coming from a CL background |
| 11:22:58 | <lottaquestions_> | so was thinking something along the lines of Emacs+Slime but for Haskell |
| 11:23:02 | <yushyin> | lottaquestions_: https://cabal.readthedocs.io/en/3.6/getting-started.html |
| 11:23:24 | <Gurkenglas_> | Common Lisp? Command Line? |
| 11:23:33 | <lottaquestions_> | Common Lisp |
| 11:25:28 | × | DNH quits (~DNH@2a02:8108:1100:16d8:adf2:7fd4:5ba2:8512) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 11:26:01 | <Gurkenglas_> | uhhh maybe this https://github.com/emacs-lsp/lsp-haskell for the "make emacs a haskell ide" |
| 11:26:26 | <lottaquestions_> | yushyin: Thanks. |
| 11:26:42 | <lottaquestions_> | Gurkenglas_: Thanks |
| 11:27:38 | <Gurkenglas_> | In singletons, why is Demote Nat Natural rather than Nat? |
| 11:32:03 | → | jalil joins (~jalil@pop.92-184-110-73.mobile.abo.orange.fr) |
| 11:36:27 | × | foul_owl quits (~kerry@23.82.193.78) (Ping timeout: 256 seconds) |
| 11:36:27 | × | zeenk quits (~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5) (Quit: Konversation terminated!) |
| 11:36:36 | × | jalil quits (~jalil@pop.92-184-110-73.mobile.abo.orange.fr) (Ping timeout: 245 seconds) |
| 11:42:36 | <lortabac> | Gurkenglas_: because Nat used to be a different type, not very useful at runtime |
| 11:43:02 | <lortabac> | but, since base 4.15, type Nat = Natural |
| 11:43:39 | <Gurkenglas_> | phew |
| 11:44:49 | → | Midjak joins (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
| 11:44:52 | → | cynomys joins (~cynomys@user/cynomys) |
| 11:45:10 | <Gurkenglas_> | https://richarde.dev/papers/2012/singletons/paper.pdf <- "Any is an analogue of⊥at the type level" <- huh. I would have identified Any not by "this is in each kind" but by "this is the union of all elements of its kind". does "a is less defined than b" correspond, not to a->b, but to b->a ? |
| 11:45:43 | <dminuoso> | Can you delete a package candidate from hackage? |
| 11:46:16 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 11:46:16 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 11:46:16 | → | wroathe joins (~wroathe@user/wroathe) |
| 11:48:02 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 11:48:19 | <Gurkenglas_> | ...the meaning of "singleton" is coming to me now - this is just for building types with just one element, right? By type-level lambdas, I was looking more for something like being able to say \b a -> b instead of Const b a |
| 11:48:58 | <neverwas> | lottaquestions_: re slime, etc. development on haskell-mode seems to be pretty sleepy these days. I've been using this fella's fork, which favors comint for all interactive REPLing: https://github.com/tonyday567/haskell-mode.git (if you're into that sort of thing) |
| 11:49:17 | <dminuoso> | Gurkenglas_: Right. The idea of singletons is that if a type has just one value, then you can demote/promote between them. |
| 11:49:42 | <dminuoso> | So values can be treated as types and vice-versa |
| 11:50:18 | <dminuoso> | In combination with GADTs, pattern matching and some universal quantification you can pull of some fancy tricks with that |
| 11:50:57 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 11:51:36 | <Gurkenglas_> | So if I have (forall f. f a), how would I apply Const b to that to get out b, by using a type-level lambda instead of Const? |
| 11:51:55 | × | jco quits (~jco@90-228-194-139-no542.tbcn.telia.com) (Quit: leaving) |
| 11:52:21 | <Gurkenglas_> | or perhaps by promoting const to the type level |
| 11:52:26 | <lortabac> | Gurkenglas_: with singletons, you can write normal lambdas and the TH magic will generate the appropriate type families and defunctionalized definitions |
| 11:52:39 | <dminuoso> | Ah you mean you're looking for the type level isomorphism `Const B T ~~~ B`? |
| 11:53:33 | <Gurkenglas_> | lortabac, oh, i should have noticed that my eyes had passed over enough documentation words to deduce that |
| 11:53:34 | <dminuoso> | I dont quite understand the question |
| 11:55:23 | <Gurkenglas_> | dminuoso, the question was merely how to construct, say, foo :: (forall f. f a) -> b without the boilerplate of a custom data type. Where Const counts as custom enough ^^ |
| 11:56:04 | <Gurkenglas_> | You could imagine that the f required for a particular usecase is significantly more complex than Const b. Like half the things edward kmett does |
| 11:56:05 | <dminuoso> | Sorry I gotta pass. I cant quite parse the intent from that |
| 11:56:27 | <Gurkenglas_> | Fair enough, it's answered. |
| 11:56:48 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 11:59:56 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds) |
| 12:01:19 | → | merijn joins (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) |
| 12:01:37 | × | cynomys quits (~cynomys@user/cynomys) (Ping timeout: 240 seconds) |
| 12:03:13 | → | mcgroin joins (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 12:07:36 | <Gurkenglas_> | Oh no, singletons-th can't promote (repeat 2)! i suppose one can promote (2:) and then use its fixed point. Does that solve the entire infinities problem? |
| 12:08:43 | → | vysn joins (~vysn@user/vysn) |
| 12:14:20 | → | DNH joins (~DNH@2a02:8108:1100:16d8:adf2:7fd4:5ba2:8512) |
| 12:22:09 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 12:23:23 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 12:28:16 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 12:44:30 | × | Midjak quits (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Quit: This computer has gone to sleep) |
| 12:52:42 | → | jalil joins (~jalil@lstlambert-656-1-270-247.w90-63.abo.wanadoo.fr) |
| 12:55:58 | → | lavaman joins (~lavaman@98.38.249.169) |
| 12:57:44 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 12:57:49 | × | chenqisu1 quits (~chenqisu1@183.217.200.249) (Quit: Leaving) |
| 12:58:27 | × | jalil quits (~jalil@lstlambert-656-1-270-247.w90-63.abo.wanadoo.fr) (Quit: jalil) |
| 12:58:46 | → | jalil joins (~jalil@lstlambert-656-1-270-247.w90-63.abo.wanadoo.fr) |
| 12:58:59 | × | hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 12:59:36 | → | jlamothe joins (~jlamothe@198.251.61.229) |
| 12:59:49 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 13:00:26 | → | hololeap joins (~hololeap@user/hololeap) |
| 13:04:30 | <merijn> | Gurkenglas_: <clippy>It looks you're trying to write dependent types, have you considered using Idris? :D </clippy> |
| 13:05:19 | → | slack1256 joins (~slack1256@191.125.227.212) |
| 13:06:49 | <Gurkenglas_> | merijn, all I wanted was for code to say the likes of "\f d c -> (f d -> c)" instead of "Costar"! |
| 13:07:49 | × | mvk quits (~mvk@2607:fea8:5cdc:bf00::5483) (Ping timeout: 240 seconds) |
| 13:12:17 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 13:12:27 | × | Flow quits (~none@gentoo/developer/flow) (Ping timeout: 250 seconds) |
| 13:15:02 | <geekosaur> | "all I wanted was…" is how you end up on the road to hell |
| 13:18:41 | × | max22- quits (~maxime@2a01cb088335980044f7b68859555b87.ipv6.abo.wanadoo.fr) (Ping timeout: 252 seconds) |
| 13:18:55 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 13:21:11 | <dminuoso> | Okay, so because you dont like Costar, you're now throwing template haskell to generate absurd singletons code at it instead? |
| 13:21:16 | dminuoso | ponders about that |
| 13:21:27 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 13:24:27 | × | fvr quits (uid503686@id-503686.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:31:17 | → | CiaoSen joins (~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 13:32:01 | → | dschrempf joins (~dominik@mobiledyn-62-240-134-126.mrsn.at) |
| 13:45:56 | → | max22- joins (~maxime@2a01cb0883359800886894252541f01e.ipv6.abo.wanadoo.fr) |
| 13:46:38 | <Gurkenglas_> | Not Costar in particular. Would you rather see \a b c -> a b c or a named function with that definition? |
| 13:47:58 | → | o-90 joins (~o-90@gateway/tor-sasl/o-90) |
| 13:56:06 | → | Flow joins (~none@gentoo/developer/flow) |
| 13:56:20 | <lortabac> | Gurkenglas_: this has been discussed recently on this channel, apparently what you are looking for is possible in Idris |
| 13:57:18 | <lortabac> | however I don't know what the implications are in terms of inference, of code readability etc. |
| 13:58:49 | <lortabac> | in Haskell it requires insane complexity, certainly more than Costar or whatever you are trying to avoid |
| 14:00:27 | × | o-90 quits (~o-90@gateway/tor-sasl/o-90) (Ping timeout: 276 seconds) |
| 14:00:45 | × | hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Quit: WeeChat 2.8) |
| 14:01:34 | <lortabac> | incidentally, the unsaturated type-families proposal has been accepted, I'm curious to see what will come out of it |
| 14:02:15 | <Gurkenglas_> | i can do Stream to, surely this construction has a name https://gist.github.com/Gurkenglas/137914f5790f0e0390c631f9678832da |
| 14:02:19 | <Gurkenglas_> | *too |
| 14:03:08 | → | Guest35 joins (~Guest35@node-126p.pool-125-24.dynamic.totinternet.net) |
| 14:05:07 | → | hughjfchen joins (~hughjfche@vmi556545.contaboserver.net) |
| 14:05:34 | × | hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 14:06:01 | → | slac36430 joins (~slack1256@186.11.25.57) |
| 14:06:43 | × | dschrempf quits (~dominik@mobiledyn-62-240-134-126.mrsn.at) (Quit: WeeChat 3.3) |
| 14:06:55 | → | hololeap joins (~hololeap@user/hololeap) |
| 14:07:57 | × | slack1256 quits (~slack1256@191.125.227.212) (Ping timeout: 240 seconds) |
| 14:09:02 | <Gurkenglas_> | huh, it doesn't fit for "newtype CoStream a = CoStream {runCoStream :: forall f. (f a -> a) -> (f a -> f a) -> f a}" though. |
| 14:09:15 | → | neverfindme joins (~hayden@158.123.160.43) |
| 14:09:21 | × | neverfindme quits (~hayden@158.123.160.43) (Remote host closed the connection) |
| 14:14:24 | → | shriekingnoise joins (~shrieking@201.231.16.156) |
| 14:14:43 | <Guest35> | Any help with where to start?? Newbie here.. |
| 14:14:43 | <Guest35> | Fill in the definition of the following function, using fst and snd: |
| 14:14:44 | <Guest35> | f :: (a, b) -> (c, d) -> ((b, d), (a, c)) |
| 14:14:44 | <Guest35> | f = undefined |
| 14:16:55 | <Gurkenglas_> | Guest35, are you able to write any definition of any function? |
| 14:20:46 | <Guest35> | yes. basics |
| 14:21:05 | <Guest35> | for example. last exercise. |
| 14:21:06 | <Guest35> | isPalindrome :: String->IO() |
| 14:21:06 | <Guest35> | isPalindrome x = |
| 14:21:07 | <Guest35> | if goodness |
| 14:21:07 | <Guest35> | then print "yes" |
| 14:21:08 | <Guest35> | else |
| 14:21:08 | <Guest35> | print "no" |
| 14:21:09 | <Guest35> | where goodness = |
| 14:21:09 | <Guest35> | x == reverse x |
| 14:21:11 | <Andrew> | Don't paste here |
| 14:21:14 | × | zer0bitz quits (~zer0bitz@2001:2003:f74d:b800:2df2:1ec5:8dd3:29f0) (Ping timeout: 260 seconds) |
| 14:21:15 | × | alMalsamo quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 276 seconds) |
| 14:21:25 | → | bontaq joins (~user@ool-45779fe5.dyn.optonline.net) |
| 14:21:36 | <Andrew> | Guest35: That's not a function |
| 14:21:41 | <Andrew> | It's an IO Monad |
| 14:21:49 | <Gurkenglas_> | yes it's a function |
| 14:22:04 | <Andrew> | Oh, my bad. |
| 14:22:11 | <Andrew> | lol silly me |
| 14:22:16 | <Andrew> | |
| 14:22:30 | <Gurkenglas_> | And "an IO Monad" is, uh, not how those words are used :D |
| 14:22:40 | <Andrew> | f (a, b) (c, d) = ((b, d), (a, c))? |
| 14:22:49 | <Andrew> | It returns an IO monad |
| 14:22:55 | <Andrew> | Or, it evaluates to one |
| 14:22:56 | <Andrew> | Better |
| 14:23:03 | × | rusrushal13 quits (~rusrushal@2405:201:7003:8952:a27c:c592:8e19:8656) (Ping timeout: 256 seconds) |
| 14:23:07 | <xsperry> | not sure if types were included in the excercise, but I'd make isPalindrome `String -> Bool' instead |
| 14:23:50 | <Gurkenglas_> | IO is a monad, IO isn't an adjective about monads. |
| 14:23:56 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 14:24:01 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 14:24:17 | <Guest35> | ok. |
| 14:24:23 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 14:24:27 | <Guest35> | any help on where to start |
| 14:24:41 | <Guest35> | and if i dont paste here, then where |
| 14:24:58 | <Gurkenglas_> | Guest35, do you know what the type signature "f :: (a, b) -> (c, d) -> ((b, d), (a, c))" is supposed to tell you? |
| 14:25:42 | <Guest35> | takes a tuple and a tuple and maps it to a tuple? |
| 14:26:10 | <Gurkenglas_> | Sure. Can you write a definition for "g :: a -> b -> (b,a)"? |
| 14:26:45 | → | ystael joins (~ystael@user/ystael) |
| 14:27:23 | → | Ariakenom joins (~Ariakenom@h-82-196-111-63.NA.cust.bahnhof.se) |
| 14:27:50 | → | akegalj joins (~akegalj@141-136-168-212.dsl.iskon.hr) |
| 14:28:37 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 14:28:53 | <merijn> | Gurkenglas_: Here, save yourself the trouble trying to articulate the thing you're trying to articulate: https://blog.jle.im/entry/io-monad-considered-harmful.html |
| 14:29:06 | <merijn> | Andrew: See above ;) |
| 14:29:28 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 14:29:49 | × | slac36430 quits (~slack1256@186.11.25.57) (Ping timeout: 250 seconds) |
| 14:30:11 | → | slack1256 joins (~slack1256@191.125.227.212) |
| 14:30:22 | <Andrew> | :( |
| 14:30:33 | <Andrew> | I use them a lot |
| 14:30:43 | → | haskell_ joins (~haskell@65-102-32-32.ptld.qwest.net) |
| 14:31:01 | <Andrew> | Gurkenglas_: Yeah? IO is an monad, so I call it a IO monad |
| 14:31:04 | × | haskell_ quits (~haskell@65-102-32-32.ptld.qwest.net) (Remote host closed the connection) |
| 14:31:05 | <Andrew> | Whatever, English |
| 14:31:22 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 14:31:22 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 14:31:22 | → | wroathe joins (~wroathe@user/wroathe) |
| 14:31:24 | <merijn> | Andrew: That blog posts clarifies why that's not great usage |
| 14:31:37 | <Andrew> | sure |
| 14:31:50 | <geekosaur> | imo it misleads people into thinking the Monad is what makes IO special, when IO is special because it is IO |
| 14:31:58 | <geekosaur> | all the Monad part does is enforce sequencing |
| 14:32:16 | <Andrew> | Well, yeah |
| 14:32:36 | <Guest35> | g (a,b) = (b,a)? |
| 14:32:36 | <Gurkenglas_> | merijn, not what I meant - i wouldn't have complained if he said that it has something to do with the IO monad, but using "an IO monad" to refer to a value of type `IO ()` confuses the fact that the thing that's supposed to have something to do with the word "monad" there is the one, the only, "IO" |
| 14:33:05 | <geekosaur> | Guest35, almost but not quite. |
| 14:33:18 | <Gurkenglas_> | Guest35, almost. That's (a,b) -> (b,a) |
| 14:33:41 | <Andrew> | g a b = (b,a) |
| 14:33:44 | <Gurkenglas_> | as in, an implementation of g :: (a,b) -> (b,a) |
| 14:34:02 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Ping timeout: 252 seconds) |
| 14:34:18 | <Andrew> | Guest35: (Fake) multiple parameters aren't tuples |
| 14:34:43 | <Gurkenglas_> | Andrew, don't spoil the puzzle :D though it's not much of a puzzle, Guest isn't supposed to have to guess the *syntax* of the language. |
| 14:34:53 | <Andrew> | ... If you put them in tuple-like things that's gonna look weird once you have currying. |
| 14:35:20 | <Andrew> | My fault :D |
| 14:35:29 | <Guest35> | hmmm. |
| 14:36:07 | <Guest35> | so i have no coding experience. just starting reading and trying out exercises the last 3 days. |
| 14:36:16 | <Guest35> | dont get too far ahead of me |
| 14:36:47 | <Andrew> | Guest35: It's okay :) |
| 14:37:00 | <merijn> | Gurkenglas_: That's literally what the blog is about, though ;) |
| 14:37:10 | <Andrew> | Guest35: it's also good to have Haskell as a first language, because you won't be brainwashed by the imperative stuff lol |
| 14:37:16 | <geekosaur> | this is a place where you'reliableto make mistakes because Haskell is unlike most other languages in this regard |
| 14:37:18 | <Gurkenglas_> | Guest35, the implementation of "f :: (a, b) -> (c, d) -> ((b, d), (a, c))" is going to start with "f ab cd = " this time, and you are supposed to use the functions "fst :: (x,y) -> x" and "snd :: (x,y) -> y". Can you assemble the part of f's implementation to the right of =? |
| 14:37:26 | <Andrew> | (Haskell is a functional language) |
| 14:38:01 | <Andrew> | Oh, silly me, I didn't use fst and stuff |
| 14:38:06 | <Andrew> | I always use pattern matching |
| 14:39:13 | <Guest35> | Gurkenglas_: ill try. so what is the f ab cd telling me? same as "f (a,b) (c,d)" just short notation? |
| 14:39:21 | <Gurkenglas_> | Me too, let's hope the exercises he's doing won't instill the habit not to pattern-match in him. |
| 14:39:46 | × | Erutuon quits (~Erutuon@user/erutuon) (Quit: WeeChat 2.8) |
| 14:40:38 | <Gurkenglas_> | Guest35, "f ab cd = " makes it so that instead of having values of type a and b to work with, you only have a value ab of type (a,b). This is worse, since you plan to use a and b for other things. So you'll have to use fst and snd to get them out of the ab. |
| 14:40:45 | <Guest35> | im working from the text. Haskell Programming From First Principles |
| 14:40:45 | <Guest35> | by Christopher Allen https://www.goodreads.com/en/book/show/25587599-haskell-programming-from-first-principles |
| 14:41:17 | → | alMalsamo joins (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 14:41:34 | <Andrew> | I think that book is a good one |
| 14:43:33 | <Gurkenglas_> | merijn, I disagree! The blog tells people not to mention the word monad to newbies, my nitpick was that the usage of the term monad was technically incorrect. |
| 14:44:44 | Andrew | agrees with Gurkenglas_ on this point |
| 14:49:36 | <Guest35> | ok just showing my thinking. i know this is wrong. but i want to type. g :: (a,b) -> (b,a) g ab = snd g, fst g |
| 14:49:52 | <ski> | you're almost there |
| 14:49:53 | <Andrew> | tuples? |
| 14:49:58 | <Andrew> | They need (parens) |
| 14:50:13 | <Andrew> | g a b = (snd g, fst g) |
| 14:50:40 | <Gurkenglas_> | Andrew, typos. |
| 14:50:44 | <ski> | what is `g' in `snd g' ? |
| 14:51:18 | <Andrew> | xD |
| 14:51:35 | <Andrew> | Wasn't paying attentions |
| 14:51:47 | <Andrew> | ~~you might do that with lisp macros~~ |
| 14:51:52 | → | jao joins (~jao@66.63.167.168) |
| 14:52:06 | → | fef joins (~thedawn@user/thedawn) |
| 14:52:13 | ski | looks at Guest35 |
| 14:53:47 | <Guest35> | ab? |
| 14:55:06 | <ski> | what is `ab' ? |
| 14:56:21 | × | alMalsamo quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 276 seconds) |
| 14:56:52 | → | slack1135 joins (~slack1256@186.11.25.57) |
| 14:57:15 | <Guest35> | the parameters of g? |
| 14:57:27 | <akhesacaro> | Gurkenglas_: With my student I use the word "Chainable" instead of Monad :p |
| 14:57:36 | → | alMalsamo joins (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 14:57:51 | → | pavonia joins (~user@user/siracusa) |
| 14:58:41 | <Gurkenglas_> | akhesacaro, you misunderstand. I would also complain if someone called "print 12" "an IO Chainable" |
| 14:58:59 | <janus> | i think ab is a value of type (a,b) that Gurkenglas_ describes |
| 14:59:19 | × | akegalj quits (~akegalj@141-136-168-212.dsl.iskon.hr) (Quit: leaving) |
| 14:59:20 | × | slack1256 quits (~slack1256@191.125.227.212) (Ping timeout: 252 seconds) |
| 15:00:58 | <Gurkenglas_> | Maybe it would have been prudent not to use exactly the same names for a variable and its type ._. |
| 15:00:59 | <ski> | Guest35 : that's what `ab' is, in the context of `g ab'. it's what rôle it fills, in this context. it's not what it is, in itself |
| 15:01:04 | <merijn> | akhesacaro: The thing is that "being a Monad" is a property of a type (like 'IO') it doesn't say anything useful about *values* |
| 15:01:40 | <merijn> | akhesacaro: getLine is "an IO action" monads play no role there |
| 15:01:46 | <ski> | Guest35 : `ab' is a pair |
| 15:01:50 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 15:04:06 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 15:04:16 | <Gurkenglas_> | merijn, IO isn't a type, types are that which has kind * :P. IO has kind *->* |
| 15:04:39 | ski | glances around nervously |
| 15:04:46 | <Guest35> | let me ask the original q again. i think maybe my goal isnt obvious anymore. |
| 15:04:46 | <Guest35> | Fill in the definition of the following function, using fst and snd: |
| 15:04:47 | <Guest35> | f :: (a, b) -> (c, d) -> ((b, d), (a, c)) |
| 15:04:47 | <Guest35> | f = |
| 15:05:24 | <ski> | so, what is *your* question, at the moment ? |
| 15:05:50 | <Gurkenglas_> | Guest35, Note that you are also supposed to write something to the left of that = |
| 15:05:52 | <Guest35> | any hints without giving it away lol |
| 15:06:00 | ski | also agrees with `IO' being a type |
| 15:06:14 | <ski> | Guest35 : which was your latest attempt ? |
| 15:06:44 | <Guest35> | f :: (a,b)->(c,d)->((b,d),(a,c)) |
| 15:06:45 | <Guest35> | f (a, b) (c, d) = ((b, d), (a, c)) |
| 15:06:50 | <Guest35> | but this doesnt use fst or snd |
| 15:06:53 | <ski> | yea |
| 15:07:13 | <ski> | i didn't see you finish the `g :: (a,b) -> (b,a)' one |
| 15:07:18 | <ski> | did you ? |
| 15:07:28 | <Gurkenglas_> | Huh, I didn't know people disagree that * is the kind of types. I suppose it's good to have a name for the union of those kinds. |
| 15:07:43 | <Gurkenglas_> | ski, are constraints also types? |
| 15:08:14 | × | jao quits (~jao@66.63.167.168) (Remote host closed the connection) |
| 15:08:24 | <akhesacaro> | Guest35, you've deconstructed the tuple too much |
| 15:08:38 | <ski> | Gurkenglas_ : sure, at least with `ConstraintKinds' |
| 15:08:42 | × | wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 276 seconds) |
| 15:08:43 | <geekosaur> | the problem with * being the kind of types is that it takes away * as a type operator, so people prefer Type these days |
| 15:09:07 | → | jao joins (~jao@66.63.167.168) |
| 15:09:34 | <Gurkenglas_> | geekosaur, uh. Does Type contain IO? |
| 15:09:38 | → | n3rdy1 joins (~n3rdy1@2600:1700:4570:3480::41) |
| 15:09:52 | <geekosaur> | no,IO is Type -> Type |
| 15:09:56 | <merijn> | Gurkenglas_: Hard disagree |
| 15:10:00 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 15:10:00 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 15:10:00 | → | wroathe joins (~wroathe@user/wroathe) |
| 15:10:04 | <merijn> | Gurkenglas_: IO very much is a type |
| 15:10:04 | <ski> | Gurkenglas_ : anyway, people used to say that `Either String' is not a type, but a type constructor. hence `Functor' is not a type class, but a constructor class. however, i think it's more useful to regard it as a type (and i use "type constructor" to not include `Either String') |
| 15:10:15 | <Guest35> | no. |
| 15:10:28 | <merijn> | I don't acknowledge Type as a thing anyway, because TypeInType is lunacy |
| 15:10:29 | <geekosaur> | guess there's still terminology disagreement |
| 15:10:31 | <Guest35> | bc im stuck lol |
| 15:10:31 | → | slack1256 joins (~slack1256@191.125.227.212) |
| 15:11:04 | <ski> | Guest35 : it might help you if you finish this `g' first |
| 15:11:09 | <ski> | last i saw was |
| 15:11:17 | <ski> | <Guest35> ok just showing my thinking. i know this is wrong. but i want to type. g :: (a,b) -> (b,a) g ab = snd g, fst g |
| 15:11:28 | <ski> | which is close but no chocolate yet |
| 15:11:46 | <Guest35> | but i want chocolate |
| 15:11:50 | ski | smile |
| 15:12:12 | <ski> | <ski> what is `g' in `snd g' ? |
| 15:12:21 | <ski> | Guest35 : what about this question ^ ? |
| 15:12:25 | <Guest35> | i need a where statement? where g = |
| 15:12:37 | <ski> | no, you don't need that here |
| 15:12:41 | <akhesacaro> | Guest35 no need a where here :p |
| 15:12:44 | <merijn> | Gurkenglas_: Consider this: Would you argue that 'f' (with "f :: Foo -> Bar") is not a value, because 'bar' (with 'bar :: Bar') is a value? |
| 15:12:55 | × | slack1135 quits (~slack1256@186.11.25.57) (Ping timeout: 256 seconds) |
| 15:13:07 | <Gurkenglas_> | I'm willing to accept that we call IO a type, I'd also be willing to say Type instead of *, but both of those doesn't work, there needs to be some name for * is |
| 15:13:20 | <Gurkenglas_> | -is |
| 15:13:35 | ski | tends to call it "concrete type" .. but some people don't like that term |
| 15:13:41 | <merijn> | Like me ;) |
| 15:13:44 | ski | smiles |
| 15:14:18 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 15:14:22 | <merijn> | tbh, I dislike the use of Type and find the lack of * as type level operator acceptable, so I will just be a Luddite and stick to * |
| 15:14:44 | <ski> | o/ |
| 15:15:10 | <merijn> | And much like Luddites are portrayed as "backwards" while really having pretty sensible ideas/motivations for their behaviour, so do I ;) |
| 15:15:34 | <Gurkenglas_> | just like presheaves |
| 15:15:48 | ski | looks at Guest35 |
| 15:15:54 | <akhesacaro> | Guest35, if the functions _fst_ and _snd_ take a tuple as parameter, you need to not deconstruct it and put it into a variable to pass it to your functions. |
| 15:16:47 | <Guest35> | what would it look like in my terminal. g "high" 5 would return (5, "high") |
| 15:17:05 | <ski> | g ("high,5) -- rather |
| 15:17:36 | <Guest35> | g("high",5)? |
| 15:17:39 | <Ariakenom> | I don't care about using up * as an operator. I think * is a bad name though. |
| 15:18:08 | <ski> | i prefer it with a space, `g ("high",5)' . you're not passing two parameters to `g', you're passing a single one, which happens to be a pair |
| 15:18:23 | <ski> | so, for that call, `ab' would become the pair `("high",5)' |
| 15:18:30 | <merijn> | Ariakenom: Why? Most of the literature uses it |
| 15:18:50 | <Gurkenglas_> | Ariakenom, what pair of names do you suggest for * and the thing that both Int and IO are? |
| 15:19:18 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:19:34 | <ski> | Gurkenglas_ : now, for `g ab = snd g, fst g', if `ab' becomes `("high",5)', how could the result (which you've written as `snd g, fst g') become the pair `(5,"high")' ? |
| 15:19:39 | <ski> | er, Guest35 ^ |
| 15:20:40 | Gurkenglas_ | .oO(type-level value) |
| 15:21:10 | <merijn> | Gurkenglas_: IO isn't *, though :p It's * -> * :p |
| 15:21:14 | → | k8yun joins (~k8yun@user/k8yun) |
| 15:21:32 | <Gurkenglas_> | merijn, I didn't claim otherwise, i asked for a pair of names for those two separate concepts |
| 15:22:15 | <Ariakenom> | I just don't like that it isn't alphanumerical. Star would be fine by me. |
| 15:22:19 | <merijn> | If you wanna solve the hierarchy problem, you should just go the stratification solution from Extended CoC (like Coq and (I think?) Agda use) |
| 15:22:34 | <merijn> | TypeInType is a stupid shortcut that confuses human brains |
| 15:22:40 | <merijn> | At least mine :p |
| 15:23:07 | geekosaur | wonders how Ωmega solves this |
| 15:23:08 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 250 seconds) |
| 15:23:24 | <Ariakenom> | alphanumerical isn't quite right but you get the point. not what would be an operator on the value level |
| 15:23:33 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 15:23:36 | <merijn> | Easy, unicode star :p |
| 15:23:53 | <Ariakenom> | -.- |
| 15:24:02 | ski | uses a five-pointed star, in hand-writing |
| 15:24:41 | <Gurkenglas_> | use x >:D |
| 15:24:59 | <Ariakenom> | I don't dislike type in type. Can I get an example for when it's terrible? |
| 15:25:15 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 15:25:46 | <merijn> | Ariakenom: It makes reading type level stuff very confusing because it ends up all being Type |
| 15:25:54 | <Gurkenglas_> | Ariakenom, the basic argument against is russel's paradox |
| 15:26:15 | <merijn> | Ariakenom: The "proper" solution is to (instead of collapsing everything into types) is to have an infinite hierarchy of types |
| 15:26:36 | → | yauhsien joins (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) |
| 15:27:37 | ski | idly wonders how Guest35 is faring with the problem |
| 15:27:38 | <merijn> | Ariakenom: So values have types, the "type" of Type_0, then an Type_1 is "all of Type_0 *plus* things that include Type_0 itself) |
| 15:27:39 | <Gurkenglas_> | (i'd guess you can also prevent russel's paradox by not letting people define subtypes via predicates) |
| 15:27:49 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) (Ping timeout: 240 seconds) |
| 15:27:55 | <merijn> | and Type_2 is Type_1 *plus* all things using Type_1 itself |
| 15:28:09 | <Gurkenglas_> | merijn, why plus instead of making them all disjoint? |
| 15:28:11 | <Ariakenom> | example pls |
| 15:28:52 | <merijn> | Ariakenom: ok, so suppose we have "data Foo (f :: * -> *) = ..." |
| 15:29:01 | <ski> | well, one might want to be able to say things like `Integer -> Type_0' |
| 15:29:15 | <merijn> | Now, say we use Type_0 instead of * |
| 15:29:35 | <merijn> | so "data Foo (f :: Type_0 -> Type_0)" |
| 15:29:43 | <merijn> | With "Int :: Type_0" |
| 15:30:38 | <merijn> | So "Foo :: (Type_0 -> Type_0) -> Type_0" |
| 15:30:57 | <merijn> | But "(Type_0 -> Type_0) -> Type_0 :: Type_1" |
| 15:31:20 | <merijn> | Gurkenglas_: What ski said, yes |
| 15:31:35 | <janus> | will haskell get a universe hierarchy too? |
| 15:32:01 | <Gurkenglas_> | ski, then you should work with a surjection Type_1 -> Type_0, right? To forget the Type_1 structure of Tupe_0 so you can let it play in the Type_0 pool with Integer |
| 15:33:07 | <ski> | i don't see how that surjection would work |
| 15:33:10 | <merijn> | janus: No |
| 15:33:11 | <Gurkenglas_> | rather than an injection Type_0 -> Type_1 |
| 15:33:23 | <ski> | what would that surjection, applied to `Type_0', yield ? |
| 15:33:34 | <ski> | yea, that's better, then |
| 15:33:39 | <janus> | merijn: what you're talking about, is a universe hierarchy, right? why would haskell not get one if it gets DT? |
| 15:34:19 | <ski> | Gurkenglas_ : so one can either use such implicit injections, or use cumulative hierarchy |
| 15:34:19 | <merijn> | janus: Because GHC currently has TypeInType instead of universe hierarchy |
| 15:34:24 | <merijn> | janus: aka the hacky solution |
| 15:34:36 | <janus> | ah, but if it's hacky, surely they will get rid of it |
| 15:34:38 | <merijn> | janus: And it makes no sense to build that if you plan to do it properly later |
| 15:34:44 | <janus> | oh my |
| 15:34:57 | <Gurkenglas_> | ski, it would yield the type_0 of type_0s, which has all the objects in it and none of the functions |
| 15:34:59 | <merijn> | janus: Doubt it, it's not like the universe approach is a new solution |
| 15:35:05 | <geekosaur> | thing also is, ghc used to do it properly |
| 15:35:07 | <merijn> | janus: Also, depends on how you view "Haskell" |
| 15:35:16 | <geekosaur> | kinds were a thing but not conflated with types |
| 15:35:18 | → | zer0bitz joins (~zer0bitz@2001:2003:f74d:b800:a89e:b347:cccb:c7e5) |
| 15:35:21 | <janus> | merijn: haskell is coq, but different |
| 15:35:23 | <merijn> | janus: The odds of *Haskell* getting dependent types are near 0 |
| 15:35:29 | <geekosaur> | and sorts were at least conceptually a thing |
| 15:35:39 | <Gurkenglas_> | (or am i wrongly imagining the analogy Type_0 vs. Set as Type_1 vs. Cat?) |
| 15:35:40 | <ski> | Gurkenglas_ : i don't follow what that means |
| 15:35:42 | <merijn> | janus: GHC *may* get Dependent Types (although it's debatable whether that's a good thing) |
| 15:35:44 | <geekosaur> | (they kept changing though) |
| 15:35:51 | <ski> | (are you still talking about the surjection ?) |
| 15:36:04 | <geekosaur> | at one point there was BOX |
| 15:36:08 | × | shailangsa quits (~shailangs@host86-185-98-37.range86-185.btcentralplus.com) (Remote host closed the connection) |
| 15:36:09 | <merijn> | janus: GHC uses to have types :: kinds, kinds :: sort (but only one sort BOX) |
| 15:36:28 | <merijn> | janus: TypeInType was introduced to eliminate that to make room for various dependent Haskell experiments |
| 15:37:03 | <janus> | but maybe the experiements will fail and they will decide the universe hierarchy is the best way to go? |
| 15:37:23 | <Gurkenglas_> | geekosaur, why should ghc treat types differently from kinds at all? of course one needs to track which one one currently is looking at to prevent paradox, but shouldnt one be able to use all the same code in each case |
| 15:37:49 | <geekosaur> | "track which one one currently is looking at" |
| 15:38:17 | <geekosaur> | ghc even conflates to some extent values with types by not requiring ticks on promoted DataKinda |
| 15:38:21 | <geekosaur> | *DataKinds |
| 15:38:41 | <geekosaur> | it's *really* confusing for someone trying to keep track of what level each thing is |
| 15:38:56 | <Ariakenom> | hm was the example finished? |
| 15:38:58 | <Gurkenglas_> | for tracking, i'd think all you need to do is have an integer attached that says what level of the hierarchy this is |
| 15:39:05 | × | Guest35 quits (~Guest35@node-126p.pool-125-24.dynamic.totinternet.net) (Quit: Client closed) |
| 15:39:37 | <janus> | geekosaur: there is -Wunticked-promoted-constructors and it is part of -Wall |
| 15:39:48 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 15:39:58 | <geekosaur> | we had someone in here yesterday who got caught by this, they were working with a promoted type but kept trying to treat its promoted type constructors as data constructors and couldn't understand ghc's error messages |
| 15:40:08 | <merijn> | Gurkenglas_: Yes, which is exactly what the *right* solution is, in a mathematical sense |
| 15:40:14 | <merijn> | Gurkenglas_: But that's not what GHC does |
| 15:41:46 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 15:41:52 | → | sleblanc joins (~sleblanc@user/sleblanc) |
| 15:42:34 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 15:43:16 | <Gurkenglas_> | and then there's the language Haskell_o for every ordinal number o, and GHC_{o+1} can't compile itself but can compile GHC_o. And then eventually we run out of descent, and someone panics and tries to use that it works for all the ordinals anyway, and then we're back to inconsistency |
| 15:43:48 | → | tdammers joins (~tdammers@77.109.72.177.res.static.edpnet.net) |
| 15:45:47 | <Gurkenglas_> | ski, Type_0 would presumably be mapped to a Type_0 that contains such values as String, Int, [a] for every element, and so on |
| 15:47:03 | → | mvk joins (~mvk@2607:fea8:5cdc:bf00::5483) |
| 15:47:53 | <Gurkenglas_> | Ohh, you presumably want to then use the outputs of Integer -> Type_0 as types. Yeah, that'll need the injection. |
| 15:49:12 | <Gurkenglas_> | merijn, sounds easy to go from TypeInType to that *right* solution, so we should promote TypeInType at the expense of all the code duplication, right? |
| 15:49:39 | <Gurkenglas_> | And then eventually someone adds ordinals with a 7-line patch |
| 15:50:56 | → | shapr` joins (~user@pool-173-73-44-186.washdc.fios.verizon.net) |
| 15:52:17 | × | shapr quits (~user@pool-173-73-44-186.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 15:52:53 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 15:55:03 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:55:18 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:55:24 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:55:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:55:46 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:56:02 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:56:09 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:56:17 | × | n3rdy1 quits (~n3rdy1@2600:1700:4570:3480::41) (Ping timeout: 240 seconds) |
| 15:56:23 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:56:30 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:56:44 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:56:52 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:57:07 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:57:13 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:57:27 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:57:35 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:57:48 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:57:56 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:58:11 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:58:18 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:58:32 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:58:39 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:58:54 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:59:02 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:59:17 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:59:24 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 15:59:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 15:59:46 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:00:01 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:00:09 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:00:24 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:00:31 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:00:45 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:00:52 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:01:06 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:01:14 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:01:30 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:01:36 | <[exa]> | lavaman: your connection seems to be breaking |
| 16:01:37 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:01:52 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:02:00 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:02:01 | → | __monty__ joins (~toonn@user/toonn) |
| 16:02:02 | ChanServ | sets mode +o geekosaur |
| 16:02:11 | → | cstml joins (~cstml@user/cstml) |
| 16:02:15 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:02:18 | geekosaur | sets mode +b *!*@98.38.249.169 |
| 16:02:22 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 16:03:51 | × | merijn quits (~merijn@c-001-001-018.client.esciencecenter.eduvpn.nl) (Ping timeout: 250 seconds) |
| 16:04:41 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:cb78:26c4:6167:fc4) (Quit: WeeChat 2.8) |
| 16:05:01 | → | wroathe joins (~wroathe@user/wroathe) |
| 16:06:01 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 16:09:27 | → | n3rdy1 joins (~n3rdy1@2600:1700:4570:3480:1b88:50f:dae0:9293) |
| 16:09:50 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 16:14:08 | × | xff0x quits (~xff0x@2001:1a81:5384:400:cf7c:5041:a517:d608) (Ping timeout: 252 seconds) |
| 16:14:51 | → | xff0x joins (~xff0x@2001:1a81:5384:400:77b6:98fb:61ba:7d90) |
| 16:17:24 | ChanServ | sets mode +o litharge |
| 16:17:25 | litharge | sets mode -bo *!*@98.38.249.169 litharge |
| 16:17:57 | × | AlexisTP quits (~AlexisTP@92.57.44.63) (Ping timeout: 240 seconds) |
| 16:19:19 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 16:20:34 | × | mbuf quits (~Shakthi@171.61.235.32) (Quit: Leaving) |
| 16:21:03 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 16:25:27 | × | jgeerds quits (~jgeerds@55d4a547.access.ecotel.net) (Ping timeout: 256 seconds) |
| 16:28:45 | × | CiaoSen quits (~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 16:31:03 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 16:31:16 | → | lavaman joins (~lavaman@98.38.249.169) |
| 16:34:51 | × | caubert_ quits (~caubert@136.244.111.235) (Quit: WeeChat 3.4) |
| 16:35:00 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 16:35:06 | → | caubert joins (~caubert@136.244.111.235) |
| 16:35:30 | × | son0p quits (~ff@181.136.122.143) (Remote host closed the connection) |
| 16:44:11 | → | jinsun__ joins (~quassel@user/jinsun) |
| 16:44:43 | × | jinsun quits (~quassel@user/jinsun) (Ping timeout: 256 seconds) |
| 16:47:14 | → | slac66959 joins (~slack1256@186.11.25.249) |
| 16:48:09 | × | fef quits (~thedawn@user/thedawn) (Ping timeout: 276 seconds) |
| 16:49:10 | × | ph88 quits (~ph88@2a02:8109:9e00:71d0:713a:ad1d:dd0:bdcc) (Remote host closed the connection) |
| 16:49:17 | × | slack1256 quits (~slack1256@191.125.227.212) (Ping timeout: 240 seconds) |
| 16:49:28 | → | ph88 joins (~ph88@2a02:8109:9e00:71d0:980:dccb:621a:6731) |
| 16:49:32 | → | zebrag joins (~chris@user/zebrag) |
| 16:49:56 | × | waleee quits (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 245 seconds) |
| 16:52:42 | → | Akiva joins (~Akiva@user/Akiva) |
| 16:56:04 | → | safinaskar joins (~quassel@109.252.91.116) |
| 16:56:44 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 16:57:39 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) (Remote host closed the connection) |
| 16:57:42 | <justsomeguy> | What's an easy way to pretty print a list? |
| 16:58:11 | → | wombat875 joins (~wombat875@pool-72-89-24-154.nycmny.fios.verizon.net) |
| 16:58:31 | <safinaskar> | is there some tool in wide use for sharing reproducible environments? i. e. i want to write some code snippet, share it on IRC or some bug report and be sure that receiver will run this code in the same environment with same tools installed. Theoretically, I can use docker for this. I. e. write dockerfile, paste it to pastebin and share in irc. But it seems nobody does this. Why? People use some other tool? |
| 16:58:52 | <safinaskar> | justsomeguy: "show"? |
| 16:59:07 | <c_wraith> | safinaskar: in theory, nix does that |
| 17:00:20 | <[exa]> | justsomeguy: how much pretty do you want it? `pretty` package does it nice, there's even generics support so that you don't need to instance everything |
| 17:00:35 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 17:00:36 | → | biberu joins (~biberu@user/biberu) |
| 17:01:09 | <[exa]> | safinaskar: most code snippets are either sufficiently reproducible by itself, or fixed when the person tries to create the reproducible environment. |
| 17:01:49 | <justsomeguy> | It will be nice if I can control the layout a little - like setting the max width so it fits in my terminal emulator, and if the list elements can be aligned. I'm looking at the docs for pretty now... |
| 17:01:55 | <geekosaur> | there are online environments like repl.it |
| 17:02:14 | <DigitalKiwi> | doesn't repl.it use nix or am i thinking of something else |
| 17:02:31 | DigitalKiwi | saw a tweet a few days ago |
| 17:02:47 | <geekosaur> | or godbolt.org |
| 17:02:58 | <geekosaur> | they generally require accounts though |
| 17:03:08 | <safinaskar> | ok, thanks |
| 17:04:20 | <DigitalKiwi> | https://gist.github.com/Kiwi/ffc08bffb15798dc4b1ec2a1c47c6191#file-program-cabal-hs |
| 17:04:22 | <geekosaur> | docker's really heavyweight for this kind of thing. a nix expression would probably work |
| 17:04:44 | <DigitalKiwi> | this can be modified to use a specific channel or pinned |
| 17:06:11 | <DigitalKiwi> | https://gist.github.com/Kiwi/92415b46d58bfce34f7773944b6dcc67 early version of my paste client when it was only one file lol |
| 17:07:31 | × | jalil quits (~jalil@lstlambert-656-1-270-247.w90-63.abo.wanadoo.fr) (Quit: jalil) |
| 17:07:51 | × | jinsun__ quits (~quassel@user/jinsun) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 17:08:42 | <DigitalKiwi> | https://mostlyabsurd.com/files/snake_ToTitle |
| 17:09:10 | <DigitalKiwi> | https://dpaste.com/3CZMFPQH7 |
| 17:11:17 | → | jinsun joins (~quassel@user/jinsun) |
| 17:13:16 | → | zopsi joins (~zopsi@104-237-136-227.ip.linodeusercontent.com) |
| 17:14:15 | × | MajorBiscuit quits (~MajorBisc@c-001-013-035.client.tudelft.eduvpn.nl) (Ping timeout: 250 seconds) |
| 17:17:37 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Ping timeout: 240 seconds) |
| 17:17:48 | → | whound joins (~dust@2409:4071:d13:8d27:350a:4519:8215:43f8) |
| 17:21:09 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 17:23:30 | × | Akiva quits (~Akiva@user/Akiva) (Ping timeout: 256 seconds) |
| 17:25:07 | → | jgeerds joins (~jgeerds@55d4a547.access.ecotel.net) |
| 17:29:14 | × | dajoer quits (~david@user/gvx) (Quit: leaving) |
| 17:31:01 | → | reactormonk[m] joins (~reactormo@2001:470:69fc:105::3c24) |
| 17:32:27 | <reactormonk[m]> | I have a pretty standard query `select ( id, data, terms ) from config where id = ?` I run via postgresql-simple, where id is a uuid - however, when I try to extract the data, I get Incompatible {errSQLType = "record", errSQLTableOid = Nothing, errSQLField = "row", errHaskellType = "Text", errMessage = "types incompatible"} |
| 17:33:57 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:34:01 | × | ss4 quits (~wootehfoo@user/wootehfoot) (Ping timeout: 256 seconds) |
| 17:34:29 | → | little_mac joins (~little_ma@2601:410:4300:3ce0:89bd:bcbb:df15:8e9a) |
| 17:34:35 | → | Nendi joins (~Nendi@195.224.166.74) |
| 17:34:36 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 17:34:48 | → | jalil joins (~jalil@2a01:e0a:277:4100:df65:87a3:4ed7:bb61) |
| 17:35:20 | <safinaskar> | how to make singletons work with "String"s? |
| 17:35:45 | → | merijn joins (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) |
| 17:35:45 | <safinaskar> | i do "singletons [d|data X = Y String]" and it doesn't work |
| 17:35:59 | → | econo joins (uid147250@user/econo) |
| 17:36:48 | <Nendi> | https://stackoverflow.com/questions/31875/is-there-a-simple-elegant-way-to-define-singletons check this one should solve your problem |
| 17:39:44 | <safinaskar> | Nendi: ?!?!?!? you give me link about python |
| 17:39:58 | <safinaskar> | Nendi: my question is about haskell. and about haskell's lib "singletons" |
| 17:40:24 | → | zincy joins (~zincy@2a00:23c8:970c:4801:68f0:cbbd:5b77:19e4) |
| 17:40:30 | × | merijn quits (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds) |
| 17:42:51 | × | alp quits (~alp@user/alp) (Ping timeout: 250 seconds) |
| 17:43:04 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:44:35 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 17:44:35 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 17:44:35 | → | wroathe joins (~wroathe@user/wroathe) |
| 17:44:57 | → | InternetCitizen joins (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) |
| 17:46:48 | ← | chir4gm parts (~chirag@user/chir4gm) (WeeChat 3.4) |
| 17:48:25 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 17:49:17 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 17:49:25 | → | Topsi joins (~Tobias@dyndsl-091-249-082-173.ewe-ip-backbone.de) |
| 17:49:31 | <janus> | justsomeguy: there are multiple prettyprinter libraries |
| 17:49:34 | <janus> | @package pretty |
| 17:49:34 | <lambdabot> | https://hackage.haskell.org/package/pretty |
| 17:50:00 | <Cheery> | are there examples of implementing larger subsets of haskell? |
| 17:50:05 | <janus> | justsomeguy: that package is the 'official' one, i guess |
| 17:50:20 | × | Jing quits (~hedgehog@240e:390:7c53:a7e1:dc0:c5aa:294f:7621) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 17:50:26 | <janus> | but more people are using |
| 17:50:27 | × | mcgroin quits (~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 256 seconds) |
| 17:50:32 | <janus> | @package prettyprinter |
| 17:50:32 | <lambdabot> | https://hackage.haskell.org/package/prettyprinter |
| 17:50:40 | <Cheery> | I find difficulties with just data/codata. |
| 17:51:29 | <awpr> | ooh someone asked about pretty-printing? I second prettyprinter as a nicer rendering engine, but I have my own entry for the typeclass carrying pretty-printability-as-Haskell-syntax: https://hackage.haskell.org/package/portray |
| 17:51:29 | <tomsmeding> | Cheery: not sure if this is what you're looking for, but this exists https://github.com/Helium4Haskell/helium |
| 17:53:32 | × | InternetCitizen quits (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) (Ping timeout: 256 seconds) |
| 17:53:42 | <awpr> | (I'm not sure `pretty` is "official", but it is older and more venerable, and I think bundled with GHC. but that doesn't necessarily mean it's the one true package, just that GHC uses it) |
| 17:54:32 | → | waleee joins (~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) |
| 17:54:33 | <janus> | but it is in the official haskell org on github |
| 17:54:50 | <geekosaur> | that's because ghc usesit |
| 17:55:03 | <janus> | would be weird if https://github.com/haskell is official but the projects within are not |
| 17:55:06 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 17:55:18 | <awpr> | well, what does it mean for a package to be "official"? |
| 17:56:22 | <Cheery> | tomsmeding: I feel I'd need a paper that describes how to implement things. :) |
| 17:56:44 | × | kuribas quits (~user@ptr-25vy0i7qdirbfvrk27x.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 17:56:51 | <geekosaur> | parsec's mirrored there too, I think, because of cabal. but attoparsec and megaparsec get more use |
| 17:56:56 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 17:56:57 | <Cheery> | for instance, operational semantics for CHR were real useful. |
| 17:57:20 | <janus> | geekosaur: attoparsec is in there too https://github.com/haskell/attoparsec |
| 17:57:59 | <awpr> | being in the Haskell org certainly does give it some level of trustworthiness, but I don't think that constitutes an official stance by the Haskell org that it should be preferred over alternatives |
| 17:58:33 | <janus> | what is 'the Haskell org'? |
| 17:58:37 | <sclv> | libraries in the github haskell organization are those that have been passed over to general maintainership by their authors |
| 17:59:02 | <sclv> | its status is that it hosts github repos for widely used packages whose maintainers want to share ownership broadly |
| 17:59:27 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 17:59:37 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) |
| 17:59:42 | <janus> | but why was tasty made instead of getting updated at https://github.com/haskell/test-framework then? |
| 17:59:45 | × | zincy quits (~zincy@2a00:23c8:970c:4801:68f0:cbbd:5b77:19e4) (Remote host closed the connection) |
| 18:01:58 | <geekosaur> | [09 17:54:33] <janus> but it is in the official haskell org on github |
| 18:02:03 | <geekosaur> | [09 17:58:33] <janus> what is 'the Haskell org'? |
| 18:02:06 | <geekosaur> | make up your mind |
| 18:02:56 | <janus> | those are not the same 'org', the first usage of org is in the context of github. the second reference was not made by me and doesn't seem like it referred to github |
| 18:03:26 | <awpr> | right, I meant whoever owns that GitHub org. I don't actually know, perhaps the HF or the GHC maintainers |
| 18:03:49 | <EvanR> | the haskell shadow council |
| 18:04:46 | × | Gurkenglas_ quits (~Guest22@dslb-188-096-121-068.188.096.pools.vodafone-ip.de) (Quit: Client closed) |
| 18:07:59 | <awpr> | anyway this is kind of going off course, so let's re-center: `pretty` and `prettyprinter` both exist, `pretty` is older, used by GHC, and maintained in the GH Haskell org; `prettyprinter` is newer, a bit different, also widely used, and has coloring support |
| 18:09:16 | <sclv> | tasty was made because someone thought they could do better than test-framework |
| 18:09:37 | × | Nendi quits (~Nendi@195.224.166.74) (Remote host closed the connection) |
| 18:10:05 | <sclv> | also i believe test-framework was transferred to the github org just for maintenance purposes well after tasty was made |
| 18:11:54 | <janus> | but who maintains test-framework? because the latest release had 8 revisions. if somebody maintained it, surely it wouldn't get so many revisions, but would get a new version. |
| 18:12:11 | <janus> | it says libraries list, but is that really true? |
| 18:12:25 | <awpr> | revisions /= unmaintained |
| 18:13:17 | <awpr> | if a package just needs a version bounds bump, it needs a revision and not a new version. package maintainers can and do make metadata revisions to their own packages |
| 18:14:19 | <janus> | but also PRs like this sit unreviewed: https://github.com/haskell/test-framework/pull/51 |
| 18:14:57 | <awpr> | ah, that does seem like a maintainership question |
| 18:15:01 | <sm> | it's dead (sleeping) I think |
| 18:19:17 | × | whound quits (~dust@2409:4071:d13:8d27:350a:4519:8215:43f8) (Quit: Konversation terminated!) |
| 18:19:22 | → | CiaoSen joins (~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 18:21:23 | × | sprout_ quits (~quassel@2a02:a467:ccd6:1:a85e:5217:60c2:bcc7) (Ping timeout: 256 seconds) |
| 18:25:45 | → | f-a joins (f2a@f2a.jujube.ircnow.org) |
| 18:27:47 | ← | safinaskar parts (~quassel@109.252.91.116) () |
| 18:29:04 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 18:29:14 | → | haskellberryfinn joins (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 18:30:03 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4) |
| 18:34:30 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.3) |
| 18:39:37 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 240 seconds) |
| 18:40:57 | → | Unicorn_Princess joins (~Unicorn_P@93-103-228-248.dynamic.t-2.net) |
| 18:42:28 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection) |
| 18:43:48 | → | emf_ joins (~emf@2620:10d:c090:400::5:c6d7) |
| 18:44:20 | <Unicorn_Princess> | i need to brush up on my haskell, stack/build system and all. what's the currently most up-to-date/recommended resource for that? |
| 18:44:32 | × | cstml quits (~cstml@user/cstml) (Ping timeout: 256 seconds) |
| 18:44:50 | <maerwald> | resource for? |
| 18:44:52 | <Unicorn_Princess> | (don't need to do anything fancy with the build system, just basic usage) |
| 18:45:01 | <Unicorn_Princess> | for learning that :) |
| 18:45:09 | <maerwald> | learning stack? |
| 18:45:17 | × | emf quits (~emf@2620:10d:c090:400::5:c6d7) (Ping timeout: 240 seconds) |
| 18:45:36 | <Unicorn_Princess> | if stack is still the recommended way to set up a project, then yes |
| 18:45:41 | <EvanR> | have you heard the good news about cabal |
| 18:45:56 | <EvanR> | come to the dark side |
| 18:46:07 | <Unicorn_Princess> | but i'm scared |
| 18:47:39 | <f-a> | https://cabal.readthedocs.io/en/latest/getting-started.html ← a good quickstart for cabal |
| 18:47:47 | <carbolymer> | Unicorn_Princess: http://dev.stephendiehl.com/hask/ |
| 18:47:59 | <carbolymer> | Unicorn_Princess: good tl;dr |
| 18:48:33 | × | haskellberryfinn quits (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Remote host closed the connection) |
| 18:48:39 | <f-a> | I am getting this error clip-ariis: /home/f/francesco/progetti/ariisit/./syncSite.sh: rawSystem: posix_spawnp: invalid argument (Exec format error) |
| 18:48:48 | <f-a> | on this line rawSystem "/home/f/francesco/progetti/ariisit/./syncSite.sh" [] >> |
| 18:49:08 | <f-a> | why does rawSystem like it no more? |
| 18:49:32 | <Unicorn_Princess> | thanks y'all |
| 18:50:04 | → | vandito joins (~vandito@131.0.224.113) |
| 18:52:03 | <maerwald> | f-a: posix_spawnp expects a filename |
| 18:52:16 | × | vandito quits (~vandito@131.0.224.113) (Client Quit) |
| 18:52:23 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 18:52:41 | <maerwald> | rawSystem "sh" ["-c", "/home/f..."] |
| 18:54:16 | <f-a> | thanks |
| 18:54:40 | → | safinaskar joins (~quassel@109.252.91.116) |
| 18:55:41 | × | cosimone quits (~user@93-34-133-254.ip49.fastwebnet.it) (Remote host closed the connection) |
| 18:56:02 | → | vicfred joins (~vicfred@user/vicfred) |
| 18:56:55 | <safinaskar> | is there some programming language with prover with these properties: 1) the language is practical, i. e. it has some minimal set of packages useful in practice, at very least some general purpose parser lib and json parser and printer, 2) the prover is sound, i. e. termination checker should be included and there should no be type-in-type |
| 18:58:09 | <EvanR> | UrWeb maybe |
| 18:58:56 | → | slack1256 joins (~slack1256@191.126.227.212) |
| 18:59:02 | → | cosimone joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) |
| 19:00:05 | <d34df00d> | idris sounds kinda related. |
| 19:01:17 | × | slac66959 quits (~slack1256@186.11.25.249) (Ping timeout: 250 seconds) |
| 19:01:36 | <janus> | Unicorn_Princess: you should use ghcup to get ghc and cabal |
| 19:02:43 | <janus> | d34df00d: idris still has type-in-type though, i think |
| 19:02:44 | <Unicorn_Princess> | i thought stack was the more easy to use one |
| 19:02:52 | <Unicorn_Princess> | why would i wanna use cabal instead |
| 19:02:56 | <janus> | Unicorn_Princess: it is easy but it is unmaintained, so better not invest in it |
| 19:03:30 | <EvanR> | I'm skeptical that you don't need to know cabal at all to use stack |
| 19:03:35 | <Unicorn_Princess> | oh really? darn |
| 19:03:41 | <d34df00d> | janus: nope. They have Type (which is equialent to Type 1) : Type 2 : Type 3 ... |
| 19:03:55 | <d34df00d> | Or it might starting from 0, I don't remember, but the idea is the same. |
| 19:04:01 | <EvanR> | (I thought Type : Type 1) |
| 19:04:12 | <awpr> | last I looked, Idris had cumulative universes and not TypeInType, but that was before Idris 2, so I'm not sure what it does today. it does (did) have `trust_me` and termination-checker escape hatches, though, so there are compromises to practicality |
| 19:04:43 | <janus> | Unicorn_Princess: cabal has a solver which stack hasn't. so it helps you to find a working set of dependencies. stack will ask you to add extra-deps that won't actually build with your snapshot |
| 19:04:49 | <EvanR> | safinaskar probably knows about idris that's why I didn't go into it |
| 19:04:56 | <d34df00d> | I hope it'll eventually have something like agda's {-# OPTIONS --safe #-} which forbids that. |
| 19:05:17 | <janus> | oh yeah i am not talking to safinaskar, since they are malicious |
| 19:05:46 | <janus> | but still wanted to reply to d34df00d. good to know it has the hierarchy, i wasn't aware |
| 19:06:50 | <d34df00d> | EvanR: you very well might be right about Type : Type 1 — last time I touched idris was about 1.5 years ago. Mostly agda that's never intended to run since then. |
| 19:06:56 | <janus> | Unicorn_Princess: it's not that much harder to use cabal and it's gonna save you a headache when you avoid a bug in stack |
| 19:07:25 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 19:08:03 | <janus> | and the remote freeze files are slated for addition, which should bring the package sets you may miss |
| 19:08:49 | × | jalil quits (~jalil@2a01:e0a:277:4100:df65:87a3:4ed7:bb61) (Quit: jalil) |
| 19:09:11 | → | jalil joins (~jalil@2a01:e0a:277:4100:df65:87a3:4ed7:bb61) |
| 19:09:12 | <Unicorn_Princess> | i guess i'll bite the bullet then |
| 19:09:13 | × | mon_aaraj quits (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 256 seconds) |
| 19:09:40 | <janus> | yes, eat all of the u238 |
| 19:10:02 | <Unicorn_Princess> | surely a bullet would be depleted, not enriched! |
| 19:10:05 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 19:10:30 | <janus> | u238 is depleted afaik |
| 19:10:34 | <EvanR> | u238 is the garbage isotope |
| 19:10:38 | <Unicorn_Princess> | oh, wait, how embarassing, i confused u238 for u235 :( |
| 19:10:45 | Unicorn_Princess | runs away in shame |
| 19:10:51 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 19:10:57 | <EvanR> | turn in your factorio license and weapon now |
| 19:11:06 | <awpr> | is stack actually unmaintained? or is this sort of a sensationalized headline about people being unsatisfied with how active it is? |
| 19:11:15 | → | mon_aaraj joins (~MonAaraj@user/mon-aaraj/x-4416475) |
| 19:11:37 | <maerwald> | awpr: Snoyman put out a call for maintainers, because he's not developing it anymore |
| 19:12:05 | <maerwald> | and most of the PRs there are just ignored |
| 19:12:18 | <janus> | awpr: "none of the maintainers are spending a significant amount of time on it." https://www.snoyman.com/blog/babies-oss-maintenance/ |
| 19:12:33 | <EvanR> | is it just "done" then |
| 19:12:46 | <EvanR> | software that is done |
| 19:13:33 | <awpr> | interesting, I hadn't heard that. I guess I'll file away "port builds to cabal v2-*" as a thing I might need to do in the medium term if it breaks |
| 19:13:47 | × | wavemode quits (~wavemode@2601:241:0:fc90:2892:d0:a7ec:bc11) (Quit: Client closed) |
| 19:14:14 | <d34df00d> | Or software maintainers that are done with the software. |
| 19:14:39 | <EvanR> | that's automatic when software is done |
| 19:14:42 | → | doyougnu joins (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) |
| 19:14:56 | <EvanR> | you don't hear about done software too much but it's possible in principle |
| 19:15:36 | <maerwald> | one of the arguments was that Cabal (the library) is going too fast, without coordination with stack maintainers |
| 19:16:22 | <sclv> | it is a silly argument. there are features Cabal the library released four years ago that are still not supported |
| 19:16:35 | → | slac27834 joins (~slack1256@186.11.25.249) |
| 19:16:38 | <sclv> | no maintainer did the work to support them. They just weren't interested in keeping up! |
| 19:16:53 | <EvanR> | I retract that theory then |
| 19:17:11 | <d34df00d> | I'd say things like `cp` or `more` are more or less done, modulo occasional bitrot avoidance. |
| 19:17:18 | <safinaskar> | EvanR: thanks for mentioning UrWeb. cool project. i slightly have read the manual, and i think UrWeb doesn't include prover. it seems its type system is less powerful (not more powerful) than current ghc's type system. it seems there is no dependent types |
| 19:17:28 | <d34df00d> | But that's boring, and you can rewrite that in ~~rust~~ haskell anyway. |
| 19:17:37 | <maerwald> | sclv: I dunno... I think they even refused to talk to Cabal maintainers? So the argument is weird anyway :) |
| 19:17:39 | <EvanR> | full dependent types really is a tall order |
| 19:17:47 | <sclv> | also i would argue that build software in particular can't stay "done". the systems change out from underneath it, and they need to update based on that. There's a lot of churn from windows changing APIs, mac changing security policies, and now architectures. |
| 19:17:48 | <safinaskar> | d34df00d: as well as i understand in idris 2 we have type in type, right? |
| 19:17:58 | <EvanR> | it's not clear at all that "practical" requires full dependent types |
| 19:18:17 | <sclv> | Higher level libraries that give data structures and the like can stay "done" much more effectively than anything that needs to make even elementary syscalls |
| 19:18:19 | <sm> | the blog post suggests that more communication/collaboration between projects would have helped. But of course that is hard |
| 19:18:25 | <d34df00d> | safinaskar: I think they'll eventually have a proper hierarchy. Idris 2 is still in its 0.x years. |
| 19:18:37 | <maerwald> | sm: there were offers, but they declined (to my knowledge) |
| 19:18:51 | × | slack1256 quits (~slack1256@191.126.227.212) (Ping timeout: 256 seconds) |
| 19:18:55 | <d34df00d> | Dang sounds like I should learn cabal finally. |
| 19:19:01 | → | zincy joins (~zincy@2a00:23c8:970c:4801:68f0:cbbd:5b77:19e4) |
| 19:19:34 | <maerwald> | and they also declined to collaborate with ghcup, although stack was added to ghcup as per their request, basically |
| 19:20:13 | → | slack1256 joins (~slack1256@191.125.227.197) |
| 19:20:23 | × | doyougnu quits (~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Remote host closed the connection) |
| 19:20:27 | <sm> | at bottom line, changes in the foundations of haskell tools (GHC, Cabal) are indeed a constant treadmill, so it's got be costly / fatiguing to keep up |
| 19:20:51 | <sm> | and dude has a job and new babies |
| 19:21:11 | <Unicorn_Princess> | sounds like a case of misplaced priorities... |
| 19:21:21 | <sm> | i know right |
| 19:21:26 | <ski> | Unicorn_Princess : did you see <https://gist.github.com/merijn/8152d561fb8b011f9313c48d876ceb07> ? |
| 19:21:30 | <sm> | :-) |
| 19:21:57 | <Unicorn_Princess> | babies come and go, but haskell build systems are forever |
| 19:22:08 | <maerwald> | sm: I find it hard to believe that they find time to argue about Haskell installers for half a year, but then don't have time to communicate with either cabal or ghcup teams... and that because of babies |
| 19:22:14 | <EvanR> | I vaguely understand that stack was created in an environment where cabal kind of sucked, long ago |
| 19:22:30 | × | slac27834 quits (~slack1256@186.11.25.249) (Ping timeout: 256 seconds) |
| 19:22:31 | <EvanR> | environment changed? |
| 19:22:38 | <Unicorn_Princess> | ski, maybe, long ago. probably a good idea i read it again, thanks :) |
| 19:22:43 | <sclv> | basically its a lot easier to greenfield something that solves _some_ problems than to maintain something that solves a _lot_ of problems |
| 19:22:52 | <ski> | np :) |
| 19:23:27 | <janus> | Unicorn_Princess: that document was last modified in 2019. so it was written before the baby |
| 19:23:30 | <sm> | maerwald: you always complain about this, but I don't hear much empathy so it doesn't really carry that much weight |
| 19:23:43 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 256 seconds) |
| 19:23:47 | <maerwald> | sm: huh? |
| 19:23:48 | <sclv> | i mean empathy or blame or whatever is besides the point. the situation is what it is. |
| 19:24:13 | <sclv> | people should make choices based on how things actually are, whatever reasons in the past there may be |
| 19:24:47 | <sm> | bery true |
| 19:24:51 | <EvanR> | safinaskar, but you're right UrWeb does look cool. Not sure if it even works though |
| 19:25:23 | <maerwald> | sm: I don't understand what you mean by that |
| 19:26:33 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 19:26:34 | ski | idly wonders if Smerdyakov is even on Libera |
| 19:26:56 | → | alp joins (~alp@user/alp) |
| 19:26:56 | <ski> | (well, there's a new user, who grabbed that nickname, in any case) |
| 19:27:24 | <sm> | maerwald: I mean no offense. Just that you never miss a chance to remind us how stack/snoyman didn't respond to your PR or whatever, and therefore (implied) they suck.. but I'm sure there was a reason. Ultimately noone has unlimited time for communication and argument with all parties |
| 19:27:36 | <ski> | (hm .. or maybe they dropped it, now ?) |
| 19:27:48 | <maerwald> | sm: I'm not implying that at all |
| 19:27:53 | <EvanR> | their ears were burning |
| 19:28:00 | <maerwald> | sm: but I'm pretty confident it is *not* lack of time |
| 19:28:00 | <sm> | simple fatigue/burnout/other priorities I expect |
| 19:28:05 | <sm> | I can't even keep up with my own one project |
| 19:28:47 | <maerwald> | asking for maintainers and then not caring when people fix your code doesn't align |
| 19:28:53 | → | slac52342 joins (~slack1256@186.11.25.249) |
| 19:29:09 | <EvanR> | wait isn't that consistent AF |
| 19:29:12 | <sm> | I think that's oversimplifying |
| 19:29:14 | → | cynomys joins (~cynomys@user/cynomys) |
| 19:30:08 | <sm> | but you could be right, and he is inconsistent and screwed up in this case. I don't know everybody's motivations. I try to assume the best. |
| 19:30:23 | <sm> | based on my own failings :) |
| 19:30:41 | <janus> | d34df00d: where did you read about Type 0 : Type 1? my idris2 repl says 'Type : Type' |
| 19:31:07 | <EvanR> | mine said Type : Type 1 back in the day (idris 1) |
| 19:31:07 | <maerwald> | sm: I just get annoyed when people paint him as a victim, while others did considerable work to support stack |
| 19:31:18 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 19:31:31 | <awpr> | https://idris2.readthedocs.io/en/latest/tutorial/miscellany.html#cumulativity seems to give a definitive answer: cumulativity is how they want it to work, but Idris 2 doesn't have it yet |
| 19:31:43 | <EvanR> | also I never ran into a case where this hierarchy of types, real or imagined, actually mattered |
| 19:31:53 | × | slack1256 quits (~slack1256@191.125.227.197) (Ping timeout: 256 seconds) |
| 19:32:15 | <janus> | awpr: oh ok thanks, that explains it |
| 19:32:58 | <janus> | EvanR: but would you necessarily realize if you relied on an invalid proof? you may just have been lucky |
| 19:33:22 | <EvanR> | no it's apparently very hard to stumble upon something that exploits type in type |
| 19:35:46 | <EvanR> | "a simplification of girard's paradox" https://www.cs.cmu.edu/~kw/research/hurkens95tlca.elf xD |
| 19:36:45 | → | merijn joins (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) |
| 19:36:47 | × | jgeerds quits (~jgeerds@55d4a547.access.ecotel.net) (Remote host closed the connection) |
| 19:37:19 | <dolio> | The assumptions of Girard's paradox are weaker than type-in-type, so it might be easier to exploit the latter. |
| 19:37:25 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 19:38:03 | × | max22- quits (~maxime@2a01cb0883359800886894252541f01e.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 19:38:11 | → | mmhat joins (~mmh@55d4f954.access.ecotel.net) |
| 19:39:13 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 250 seconds) |
| 19:40:59 | → | mikoto-chan joins (~mikoto-ch@213.177.151.239) |
| 19:41:31 | × | jalil quits (~jalil@2a01:e0a:277:4100:df65:87a3:4ed7:bb61) (Quit: jalil) |
| 19:43:20 | → | max22- joins (~maxime@2a01cb088335980012c6117e30bee14c.ipv6.abo.wanadoo.fr) |
| 19:43:53 | × | cosimone quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Quit: ERC (IRC client for Emacs 27.1)) |
| 19:45:20 | × | vysn quits (~vysn@user/vysn) (Ping timeout: 252 seconds) |
| 19:46:41 | → | cosimone joins (~user@93-34-133-254.ip49.fastwebnet.it) |
| 19:48:38 | × | little_mac quits (~little_ma@2601:410:4300:3ce0:89bd:bcbb:df15:8e9a) (Ping timeout: 252 seconds) |
| 19:50:03 | × | ubert quits (~Thunderbi@p200300ecdf0994700e1bfcbc5fe04b55.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 19:56:13 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 19:56:13 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 19:56:13 | → | wroathe joins (~wroathe@user/wroathe) |
| 19:58:48 | → | jalil joins (~jalil@2a01:e0a:277:4100:8718:f702:59d2:5fba) |
| 19:59:34 | shapr` | is now known as shapr |
| 20:00:47 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 20:01:07 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 256 seconds) |
| 20:02:49 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 20:04:22 | × | Inst quits (~delicacie@2601:6c4:4080:3f80:1d81:9f23:5ac8:407a) (Ping timeout: 250 seconds) |
| 20:04:59 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 20:05:02 | × | juhp quits (~juhp@128.106.188.82) (Ping timeout: 240 seconds) |
| 20:06:07 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.4) |
| 20:06:35 | × | mikoto-chan quits (~mikoto-ch@213.177.151.239) (Quit: mikoto-chan) |
| 20:06:48 | → | mikoto-chan joins (~mikoto-ch@213.177.151.239) |
| 20:06:58 | → | juhp joins (~juhp@128.106.188.82) |
| 20:07:12 | → | notzmv joins (~zmv@user/notzmv) |
| 20:07:56 | → | ProfSimm joins (~ProfSimm@87.227.196.109) |
| 20:09:45 | × | k8yun quits (~k8yun@user/k8yun) (Quit: Leaving) |
| 20:10:38 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) (Remote host closed the connection) |
| 20:10:52 | × | merijn quits (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) (Ping timeout: 250 seconds) |
| 20:15:00 | × | jalil quits (~jalil@2a01:e0a:277:4100:8718:f702:59d2:5fba) (Quit: jalil) |
| 20:15:31 | × | jao quits (~jao@66.63.167.168) (Ping timeout: 256 seconds) |
| 20:15:53 | → | Hildegunst joins (~luc@80.248.12.109.rev.sfr.net) |
| 20:16:01 | × | motherfsck quits (~motherfsc@user/motherfsck) (Remote host closed the connection) |
| 20:17:07 | → | ehammarstrom joins (~ehammarst@62-20-203-39-no182.tbcn.telia.com) |
| 20:17:08 | × | ehammarstrom quits (~ehammarst@62-20-203-39-no182.tbcn.telia.com) (Client Quit) |
| 20:17:53 | <monochrom> | janus: BTW even in Coq, the notation "Type : Type" is just shorthand for the anti-climatic "Type n : Type (n+1) but since the indexes are clear from the context we will omit them". |
| 20:18:57 | → | ehammarstrom joins (~ehammarst@62-20-203-39-no182.tbcn.telia.com) |
| 20:26:02 | <ehammarstrom> | Is there something like `cargo watch` for haskell? I'd like to get immediate type feedback after each file save in a separate terminal window |
| 20:26:18 | <monochrom> | ghcid |
| 20:26:55 | <monochrom> | https://hackage.haskell.org/package/ghcid |
| 20:27:20 | <byorgey> | ehammarstrom: also `stack build --file-watch` |
| 20:27:54 | <EvanR> | stack is dead, long live stack |
| 20:28:19 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 20:28:30 | <ehammarstrom> | EvanR: byorgey: i was told not to use stack, so i only use cabal :) |
| 20:29:41 | <ehammarstrom> | monochrom: thanks, works great |
| 20:33:53 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 20:34:25 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 20:38:41 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:38:55 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:39:03 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:39:17 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:39:24 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:39:39 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:39:46 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:39:49 | × | yauhsien quits (~yauhsien@61-231-29-69.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
| 20:40:00 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:40:07 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:40:21 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:40:29 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:40:43 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:40:50 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:41:04 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:41:05 | → | yauhsien joins (~yauhsien@61-231-45-223.dynamic-ip.hinet.net) |
| 20:41:12 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:41:24 | → | little_mac joins (~little_ma@2601:410:4300:3ce0:89bd:bcbb:df15:8e9a) |
| 20:41:26 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:41:33 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:41:47 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:41:55 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:42:10 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:42:17 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:42:32 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:42:39 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:42:53 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:43:01 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:43:14 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:43:22 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:43:37 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:43:44 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:43:57 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:44:05 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:44:20 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:44:27 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:44:41 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:44:49 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:45:04 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:45:11 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:45:22 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 20:45:25 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:45:32 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:45:47 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:45:54 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:46:06 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 20:46:08 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:46:15 | ← | safinaskar parts (~quassel@109.252.91.116) () |
| 20:46:16 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:46:30 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:46:35 | <ehammarstrom> | Is there more well-typed version of readFile? One that evaluates to a Maybe perhaps |
| 20:46:37 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:46:52 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:47:00 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:47:15 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:47:20 | <EvanR> | what does Nothing represent, failure to open it? |
| 20:47:23 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:47:37 | → | lavaman joins (~lavaman@98.38.249.169) |
| 20:47:44 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 20:47:46 | <EvanR> | that and other issues are covered under Control.Exception s |
| 20:48:21 | <Hecate> | ehammarstrom: considering the amount of posible POSIX *or* Win32 error modes, I'm pretty sure you either want something that gives you the error |
| 20:48:40 | <Hecate> | no the way you get the error has to be ergonomic, and an ADT is not going to be alright :') |
| 20:48:55 | <d34df00d> | janus: that was about idris 1. I wouldn't take idris 2's behaviour as set in stone for now given it's still in its pre-release ages. |
| 20:48:59 | <EvanR> | an indexed monad might be an overengineered way to express the dance of opening reading and closing a file |
| 20:49:14 | <EvanR> | (a single file) |
| 20:49:15 | <Hecate> | EvanR: wat :'D |
| 20:49:40 | <dminuoso> | Dont underestimate the power of `withFile`? |
| 20:50:07 | <ehammarstrom> | And the pragmatic answer? |
| 20:50:13 | → | wyrd joins (~wyrd@gateway/tor-sasl/wyrd) |
| 20:50:15 | <EvanR> | use exceptions xD |
| 20:50:21 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) (Remote host closed the connection) |
| 20:50:22 | <EvanR> | (and not lazy readFile) |
| 20:50:36 | <dminuoso> | Yes, use exceptions. |
| 20:50:45 | <ehammarstrom> | Cheers, I've done that once before. Never again |
| 20:51:08 | → | zeenk joins (~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5) |
| 20:51:08 | <dminuoso> | ehammarstrom: I say get comfortable with them, they aren't unpleasant to work with. |
| 20:51:20 | <awpr> | I feel like file handle lifecycles and door open/close states are to indexed monads as `class Bicycle : Vehicle` and `class Weevil : Animal` are to OOP inheritance |
| 20:51:28 | → | _ht joins (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 20:51:43 | <dminuoso> | It's async exceptions that can cause most headaches, but exceptions - especially with the subtyping tricks we can use - are really nice. |
| 20:52:18 | → | jao joins (~jao@static-68-235-44-24.cust.tzulo.com) |
| 20:52:53 | <ehammarstrom> | dminuoso: I'll go ahead an use exceptions, the subtyping stuff is over my head at the moment :) |
| 20:53:15 | <EvanR> | it's true that working with files and catching their specific exceptions isn't really type safe, at least, the compiler doesn't know or tell you what exception types are possible. It's trial and error afaict |
| 20:54:02 | <dminuoso> | ehammarstrom: it's super easy. :) |
| 20:54:36 | <monochrom> | You can use try to convert exceptions to Either. http://www.vex.net/~trebla/haskell/exception-tutorial.xhtml |
| 20:55:09 | <dminuoso> | And its also widely underused. |
| 20:55:16 | <EvanR> | you still need to name the exception type like rumplestiltskin |
| 20:55:19 | × | alp quits (~alp@user/alp) (Ping timeout: 268 seconds) |
| 20:55:30 | <monochrom> | The attraction of an exception system though is you can choose how large your lexical scope of your "try" is. |
| 20:56:15 | <monochrom> | For example my opening example there can't be bothered to have 3 try's for 3 IO operations. 1 is quite enough. |
| 20:57:32 | <monochrom> | http://www.vex.net/~trebla/haskell/exception.xhtml is my satire to anti-exception FUD. |
| 20:57:44 | <ehammarstrom> | monochrom: Reducing a larger set of exceptions to a set of fewer Errors as a type would be preferrable |
| 20:59:16 | <EvanR> | you basically need to learn the exception associated with file ops |
| 20:59:44 | <EvanR> | or really the specific ones that you are interested in detecting |
| 21:03:36 | → | slack1256 joins (~slack1256@191.126.227.70) |
| 21:04:29 | <EvanR> | https://i.imgur.com/IQ6OcWF.png enjoy |
| 21:05:37 | × | slac52342 quits (~slack1256@186.11.25.249) (Ping timeout: 240 seconds) |
| 21:05:59 | → | chessai joins (sid225296@id-225296.lymington.irccloud.com) |
| 21:07:37 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 21:08:03 | <janus> | how do you limit the scope of exceptions with lexical constructs? i thought exceptions do not care about syntactical constructs? |
| 21:10:07 | <dminuoso> | janus: We're talking about IO exceptions. |
| 21:10:20 | <EvanR> | the catch primitives scope over some lexical scope |
| 21:10:43 | <EvanR> | what they catch is up to the type system though |
| 21:10:45 | × | alMalsamo quits (~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 276 seconds) |
| 21:10:51 | <EvanR> | (dynamic types) |
| 21:11:24 | <EvanR> | and yeah this is IO onlty |
| 21:11:42 | → | burnsidesLlama joins (~burnsides@dhcp168-051.wadham.ox.ac.uk) |
| 21:12:31 | → | dsrt^ joins (~dsrt@128-092-160-106.biz.spectrum.com) |
| 21:15:19 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 21:16:43 | × | mikoto-chan quits (~mikoto-ch@213.177.151.239) (Ping timeout: 256 seconds) |
| 21:18:16 | → | lavaman joins (~lavaman@98.38.249.169) |
| 21:21:26 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 21:22:41 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 252 seconds) |
| 21:26:20 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 21:28:26 | × | Hildegunst quits (~luc@80.248.12.109.rev.sfr.net) (Quit: leaving) |
| 21:28:55 | <ehammarstrom> | I am using this to catch file read exceptions (it's used in a `catch` expression): https://paste.tomsmeding.com/dlyRWQ52 how do I know that the evaluation is strict, can I verify it somehow? |
| 21:30:18 | → | wavemode joins (~wavemode@2601:241:0:fc90:2892:d0:a7ec:bc11) |
| 21:31:03 | <ehammarstrom> | I am using the BangPatterns language extension; forgot to include that |
| 21:31:33 | <EvanR> | oh, don't use readFile for that |
| 21:31:51 | × | zincy quits (~zincy@2a00:23c8:970c:4801:68f0:cbbd:5b77:19e4) (Remote host closed the connection) |
| 21:31:53 | <EvanR> | there are variants that are just strict already |
| 21:32:06 | <EvanR> | e.g. Data.ByteString, Data.Text have readFile |
| 21:32:26 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 21:32:35 | <EvanR> | presumably you also would catch an exception too |
| 21:32:46 | <ehammarstrom> | How do I "exclude" my current readFile? |
| 21:33:07 | <EvanR> | you can speak of the other versions qualified like T.readFile or import Prelude reading hiding if you want |
| 21:33:21 | <EvanR> | import Prelude hiding (readFile) |
| 21:33:51 | <EvanR> | qualifying the other one is more conventional I think |
| 21:34:17 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 21:37:42 | <ehammarstrom> | Is it preferrable to work with Text instead of String? |
| 21:37:56 | <EvanR> | for large amount of text yes |
| 21:38:03 | <EvanR> | (at a time) |
| 21:38:29 | <EvanR> | consider if you're trying to work Char by Char or.. .basically any other pattern |
| 21:38:51 | <EvanR> | String = [Char] |
| 21:39:57 | <ehammarstrom> | Do I have to `pack` every string in my program or is there some way to infer Text from my "current strings"? |
| 21:40:23 | <EvanR> | OverloadedStrings extension interprets string literals using a type class |
| 21:40:33 | <EvanR> | as long as it's unambiguous it's pretty nice |
| 21:41:06 | → | ober joins (~ober@c-73-68-74-41.hsd1.ma.comcast.net) |
| 21:41:45 | <EvanR> | you could also load your file as Text, then work with the unpacked stream of Char sourced from it |
| 21:42:33 | → | tzh_ joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 21:42:55 | × | Topsi quits (~Tobias@dyndsl-091-249-082-173.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 21:42:57 | <ober> | How do I create a file? |
| 21:42:59 | × | mmhat quits (~mmh@55d4f954.access.ecotel.net) (Quit: WeeChat 3.4) |
| 21:43:16 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Ping timeout: 245 seconds) |
| 21:45:35 | <EvanR> | :t writeFile |
| 21:45:36 | <lambdabot> | FilePath -> String -> IO () |
| 21:47:18 | <ober> | So I can just pass an empty string to writeFile? |
| 21:47:25 | <EvanR> | yeah |
| 21:48:03 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 21:49:42 | → | tiferrei joins (~tiferrei@user/tiferrei) |
| 21:50:44 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 21:51:48 | → | alp joins (~alp@user/alp) |
| 21:54:57 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) (Ping timeout: 240 seconds) |
| 21:56:17 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:03:18 | × | tiferrei quits (~tiferrei@user/tiferrei) (Remote host closed the connection) |
| 22:04:30 | → | lavaman joins (~lavaman@98.38.249.169) |
| 22:05:17 | → | Midjak joins (~Midjak@may53-1-78-226-116-92.fbx.proxad.net) |
| 22:06:01 | × | deadmarshal quits (~deadmarsh@95.38.116.14) (Ping timeout: 256 seconds) |
| 22:06:47 | → | tiferrei joins (~tiferrei@user/tiferrei) |
| 22:07:23 | → | merijn joins (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) |
| 22:08:37 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 22:13:02 | × | ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 22:13:20 | → | ProfSimm joins (~ProfSimm@87.227.196.109) |
| 22:15:31 | <maerwald> | do we have a good HTML parser? |
| 22:17:45 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:20:14 | → | ober_ joins (~ober@c-73-68-74-41.hsd1.ma.comcast.net) |
| 22:20:24 | <dminuoso> | For potentially malformed tagsoup is your best bet I think. |
| 22:20:31 | <dminuoso> | If you expect it to be well formed, no clue |
| 22:20:34 | <maerwald> | I tried tagsoup, it has bugs |
| 22:22:47 | × | ober quits (~ober@c-73-68-74-41.hsd1.ma.comcast.net) (Ping timeout: 256 seconds) |
| 22:24:53 | × | ProfSimm quits (~ProfSimm@87.227.196.109) (Remote host closed the connection) |
| 22:25:13 | → | ProfSimm joins (~ProfSimm@87.227.196.109) |
| 22:26:17 | × | wavemode quits (~wavemode@2601:241:0:fc90:2892:d0:a7ec:bc11) (Quit: Client closed) |
| 22:26:36 | × | alx741 quits (~alx741@157.100.197.240) (Quit: alx741) |
| 22:27:19 | × | wombat875 quits (~wombat875@pool-72-89-24-154.nycmny.fios.verizon.net) (Ping timeout: 256 seconds) |
| 22:28:52 | → | wavemode joins (~wavemode@2601:241:0:fc90:2892:d0:a7ec:bc11) |
| 22:29:20 | × | cosimone quits (~user@93-34-133-254.ip49.fastwebnet.it) (Quit: ERC (IRC client for Emacs 27.1)) |
| 22:30:07 | <maerwald> | can only find projects that are half done, don't support the HTML5 parsing algorithm or are just buggy |
| 22:32:15 | → | jgeerds joins (~jgeerds@55d4a547.access.ecotel.net) |
| 22:32:23 | × | michalz quits (~michalz@185.246.204.65) (Remote host closed the connection) |
| 22:33:37 | <EvanR> | I wonder what the proper interface for an HTML parser is |
| 22:33:49 | × | ec quits (~ec@gateway/tor-sasl/ec) (Quit: ec) |
| 22:35:00 | × | erisco quits (~erisco@d24-57-249-233.home.cgocable.net) (Quit: ZNC 1.8.2+cygwin2 - https://znc.in) |
| 22:35:48 | → | erisco joins (~erisco@d24-57-249-233.home.cgocable.net) |
| 22:35:48 | → | deadmarshal joins (~deadmarsh@95.38.117.25) |
| 22:37:42 | × | erisco quits (~erisco@d24-57-249-233.home.cgocable.net) (Read error: Connection reset by peer) |
| 22:38:03 | → | erisco joins (~erisco@d24-57-249-233.home.cgocable.net) |
| 22:38:13 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 240 seconds) |
| 22:38:41 | × | little_mac quits (~little_ma@2601:410:4300:3ce0:89bd:bcbb:df15:8e9a) (Ping timeout: 245 seconds) |
| 22:40:21 | × | deadmarshal quits (~deadmarsh@95.38.117.25) (Ping timeout: 256 seconds) |
| 22:41:14 | × | merijn quits (~merijn@c-001-001-027.client.esciencecenter.eduvpn.nl) (Ping timeout: 250 seconds) |
| 22:42:57 | → | Pickchea joins (~private@user/pickchea) |
| 22:43:03 | × | wyrd quits (~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 276 seconds) |
| 22:43:08 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:46:16 | × | max22- quits (~maxime@2a01cb088335980012c6117e30bee14c.ipv6.abo.wanadoo.fr) (Quit: Leaving) |
| 22:46:27 | × | bontaq quits (~user@ool-45779fe5.dyn.optonline.net) (Remote host closed the connection) |
| 22:51:43 | × | slack1256 quits (~slack1256@191.126.227.70) (Remote host closed the connection) |
| 22:55:51 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:30cc:b923:a3cb:c39c) |
| 22:56:25 | → | foul_owl joins (~kerry@71.212.148.11) |
| 22:56:35 | → | zincy joins (~zincy@host86-151-99-97.range86-151.btcentralplus.com) |
| 22:56:39 | → | deadmarshal joins (~deadmarsh@95.38.117.25) |
| 22:58:12 | × | Ariakenom quits (~Ariakenom@h-82-196-111-63.NA.cust.bahnhof.se) (Quit: Leaving) |
| 22:59:00 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 250 seconds) |
| 22:59:45 | → | ober__ joins (~ober@c-73-68-74-41.hsd1.ma.comcast.net) |
| 23:01:14 | × | zincy quits (~zincy@host86-151-99-97.range86-151.btcentralplus.com) (Ping timeout: 256 seconds) |
| 23:02:07 | × | ober_ quits (~ober@c-73-68-74-41.hsd1.ma.comcast.net) (Ping timeout: 256 seconds) |
| 23:04:27 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 23:06:21 | × | foul_owl quits (~kerry@71.212.148.11) (Ping timeout: 250 seconds) |
| 23:06:35 | × | zeenk quits (~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5) (Quit: Konversation terminated!) |
| 23:08:57 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 23:13:36 | → | slim joins (uid300876@id-300876.lymington.irccloud.com) |
| 23:13:37 | × | lechner quits (~lechner@debian/lechner) (Ping timeout: 240 seconds) |
| 23:14:46 | × | domcornloan quits (~mike@user/feetwind) (Quit: WeeChat 3.1) |
| 23:14:50 | × | deadmarshal quits (~deadmarsh@95.38.117.25) (Ping timeout: 256 seconds) |
| 23:15:09 | → | feetwind joins (~mike@user/feetwind) |
| 23:22:05 | → | foul_owl joins (~kerry@94.140.8.52) |
| 23:23:57 | × | lottaquestions quits (~nick@2607:fa49:5041:a200:4100:dd4:ee5e:72a7) (Ping timeout: 240 seconds) |
| 23:24:57 | × | mvk quits (~mvk@2607:fea8:5cdc:bf00::5483) (Ping timeout: 240 seconds) |
| 23:25:04 | → | paddymahoney joins (~paddymaho@cpe9050ca207f83-cm9050ca207f80.cpe.net.cable.rogers.com) |
| 23:25:20 | → | alMalsamo joins (~alMalsamo@gateway/tor-sasl/almalsamo) |
| 23:25:24 | → | mvk joins (~mvk@2607:fea8:5cdc:bf00::5483) |
| 23:32:39 | × | ardell quits (~ardell@user/ardell) (Quit: Konversation terminated!) |
| 23:38:43 | × | ober__ quits (~ober@c-73-68-74-41.hsd1.ma.comcast.net) (Quit: Leaving) |
| 23:40:09 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 250 seconds) |
| 23:43:49 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 23:47:57 | × | alp quits (~alp@user/alp) (Ping timeout: 250 seconds) |
| 23:48:21 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 256 seconds) |
| 23:49:17 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 23:50:04 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 23:50:21 | → | little_mac joins (~little_ma@2601:410:4300:3ce0:89bd:bcbb:df15:8e9a) |
| 23:52:04 | → | Shiranai joins (~Shiranai@190.237.13.188) |
| 23:52:40 | → | lechner joins (~lechner@debian/lechner) |
| 23:53:22 | <Shiranai> | hello, any natural ways to make an `m [m a]` into an `[m a]`? Here `m` is a monad but I could strengthen that assumption if needed |
| 23:53:38 | <dminuoso> | Shiranai: What would you expect that to do? |
| 23:53:54 | <dminuoso> | And no, in general that transformation is impossible |
| 23:53:57 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 240 seconds) |
| 23:54:14 | <dminuoso> | Well what you can do is |
| 23:54:19 | <dminuoso> | % :t sequence |
| 23:54:20 | <yahb> | dminuoso: (Traversable t, Monad m) => t (m a) -> m (t a) |
| 23:54:25 | <dminuoso> | % :t join |
| 23:54:26 | <yahb> | dminuoso: Monad m => m (m a) -> m a |
| 23:54:36 | <dminuoso> | % :t join . sequence |
| 23:54:36 | <yahb> | dminuoso: (Monad m, Traversable m) => m (m a) -> m a |
| 23:54:59 | → | sprout joins (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) |
| 23:55:07 | <dminuoso> | % :t join . fmap sequence |
| 23:55:08 | <yahb> | dminuoso: (Monad m, Traversable t) => m (t (m a)) -> m (t a) |
| 23:55:20 | <dminuoso> | Shiranai: Whether that does what you want it to do, Im not sure. |
| 23:55:29 | <shapr> | :t join |
| 23:55:30 | <lambdabot> | Monad m => m (m a) -> m a |
| 23:55:32 | <dminuoso> | So let me revoke my previous statement abuot "this is impossible" |
| 23:55:47 | <EvanR> | I can't wait to hear what Shiranai's operation is supposed to do xD |
| 23:56:27 | <EvanR> | so we bifurcate between coming up with a solution and clearing up misconceptions about monads |
| 23:56:49 | <EvanR> | or something else |
| 23:57:08 | <Shiranai> | sorry for disappointing you guys but I have no idea what that's supposed to do haha, I'm solving some exercises and that signature came up |
| 23:57:15 | <EvanR> | oof |
| 23:57:21 | shapr | is sad |
| 23:57:32 | <monochrom> | That can be a very XYZABC problem. |
| 23:58:16 | <Shiranai> | I was implementing monad for `data ListT m a = ConsT (m a) (ListT m a) | NilT` (I'm aware this is not the standard definition) |
| 23:59:26 | <Shiranai> | also thanks, dminuoso, that's probably what I needed |
| 23:59:56 | × | sprout quits (~quassel@2a02:a467:ccd6:1:511a:5eb2:c96:106b) (Ping timeout: 245 seconds) |
All times are in UTC on 2022-02-09.