Logs on 2023-11-29 (liberachat/#haskell)
| 00:00:00 | → | thegeekinside joins (~thegeekin@189.180.53.210) |
| 00:00:18 | <duncan> | Also, the Brick approach using combinators is quite powerful as a teaching mechanism because learning about combinators can be applied to other stuff like parsec |
| 00:09:35 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 00:10:21 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 00:12:08 | × | shapr quits (~user@2600:1700:c640:3100:147b:3662:c432:30f1) (Remote host closed the connection) |
| 00:12:23 | → | shapr joins (~user@2600:1700:c640:3100:c355:fe3e:4f9f:d5b6) |
| 00:13:40 | × | alp_ quits (~alp@2001:861:e3d6:8f80:1124:c998:cd66:bc03) (Ping timeout: 246 seconds) |
| 00:17:34 | → | mrmr15533 joins (~mrmr@user/mrmr) |
| 00:18:46 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Remote host closed the connection) |
| 00:19:10 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 00:22:47 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 00:23:34 | <EvanR> | gloss depends on glfw-b, and opengl that's it |
| 00:24:24 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 00:25:46 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 245 seconds) |
| 00:27:19 | × | Alleria quits (~JohnGalt@user/alleria) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 00:27:44 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 268 seconds) |
| 00:30:49 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 00:31:49 | <EvanR> | a new enough GLFW is probably in your distros package manager |
| 00:32:00 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 00:34:40 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 255 seconds) |
| 00:37:38 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 260 seconds) |
| 00:43:06 | → | Alleria joins (~JohnGalt@user/alleria) |
| 00:43:11 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 00:47:47 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 00:49:37 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 00:50:29 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Quit: Ping timeout (120 seconds)) |
| 00:50:40 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 00:51:16 | × | shailangsa quits (~shailangs@host109-152-9-157.range109-152.btcentralplus.com) (Read error: Connection reset by peer) |
| 00:51:29 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 00:51:29 | × | dumptruckman quits (~dumptruck@23-239-13-136.ip.linodeusercontent.com) (Remote host closed the connection) |
| 00:51:33 | × | tertek quits (~tertek@user/tertek) (Remote host closed the connection) |
| 00:51:39 | → | dumptruckman joins (~dumptruck@23-239-13-136.ip.linodeusercontent.com) |
| 00:51:54 | → | tertek joins (~tertek@user/tertek) |
| 00:53:53 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 00:54:12 | × | targetdisk quits (~daemonchi@45-33-4-162.ip.linodeusercontent.com) (Ping timeout: 256 seconds) |
| 00:56:30 | → | tzh_ joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 00:56:56 | × | dtman34 quits (~dtman34@c-76-156-89-180.hsd1.mn.comcast.net) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 00:57:05 | × | telser quits (~quassel@user/telser) (Quit: No Ping reply in 180 seconds.) |
| 00:57:17 | → | dtman34 joins (~dtman34@c-76-156-89-180.hsd1.mn.comcast.net) |
| 00:57:43 | <meejah> | EvanR: thanks |
| 00:57:55 | × | fun-safe-math quits (~fun-safe-@c-24-21-106-247.hsd1.or.comcast.net) (Quit: No Ping reply in 180 seconds.) |
| 00:58:10 | × | raym quits (~ray@user/raym) (Ping timeout: 256 seconds) |
| 00:58:44 | × | kaol quits (~kaol@94-237-42-30.nl-ams1.upcloud.host) (Ping timeout: 256 seconds) |
| 00:58:50 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 00:59:18 | <meejah> | ah, i have looked at gloss before. definitely like the "pitch" / paragraph on hackage :) (and so I want Graphics.Gloss.Interface.IO.Game is what you're saying ...) |
| 00:59:50 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 01:00:10 | <meejah> | ahh, BitmapSection sounds good too |
| 01:01:00 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 01:01:06 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 01:01:37 | → | fun-safe-math joins (~fun-safe-@c-24-21-106-247.hsd1.or.comcast.net) |
| 01:02:23 | → | telser joins (~quassel@user/telser) |
| 01:04:02 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (*.net *.split) |
| 01:04:02 | × | yahb2 quits (~yahb2@static.56.27.47.78.clients.your-server.de) (*.net *.split) |
| 01:04:02 | × | troydm quits (~troydm@user/troydm) (*.net *.split) |
| 01:04:02 | × | tremon quits (~tremon@83.80.159.219) (*.net *.split) |
| 01:04:02 | × | arahael quits (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (*.net *.split) |
| 01:04:03 | × | caef^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (*.net *.split) |
| 01:04:03 | × | ridcully quits (~ridcully@p57b52dae.dip0.t-ipconnect.de) (*.net *.split) |
| 01:04:03 | × | nek0 quits (~nek0@2a01:4f8:222:2b41::12) (*.net *.split) |
| 01:04:03 | × | John_Ivan quits (~John_Ivan@user/john-ivan/x-1515935) (*.net *.split) |
| 01:04:03 | × | benjaminl quits (~benjaminl@user/benjaminl) (*.net *.split) |
| 01:04:03 | × | teqwve quits (teqwve@2a01:4f8:c2c:e5b0::1) (*.net *.split) |
| 01:04:03 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) (*.net *.split) |
| 01:04:03 | × | inedia quits (~irc@23.153.248.82) (*.net *.split) |
| 01:04:03 | × | steew quits (~steew@user/steew) (*.net *.split) |
| 01:04:03 | × | turlando quits (~turlando@user/turlando) (*.net *.split) |
| 01:04:03 | × | bramhaag7 quits (~bramhaag@endeavour.server.bramh.me) (*.net *.split) |
| 01:04:03 | × | rncwnd quits (~quassel@2a01:4f8:221:27c6::1) (*.net *.split) |
| 01:04:04 | × | m1dnight quits (~christoph@78-22-4-67.access.telenet.be) (*.net *.split) |
| 01:04:04 | × | p3n quits (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (*.net *.split) |
| 01:04:04 | × | cawfee_ quits (~root@2406:3003:2077:2758::babe) (*.net *.split) |
| 01:04:04 | × | V quits (~v@ircpuzzles/2022/april/winner/V) (*.net *.split) |
| 01:04:04 | × | dyniec quits (~dyniec@dybiec.info) (*.net *.split) |
| 01:04:04 | × | arkeet quits (~arkeet@moriya.ca) (*.net *.split) |
| 01:04:04 | × | codedmart quits (codedmart@2600:3c01::f03c:92ff:fefe:8511) (*.net *.split) |
| 01:04:04 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (*.net *.split) |
| 01:04:04 | × | noctux1 quits (Hfi6K5vcqP@user/noctux) (*.net *.split) |
| 01:04:05 | × | dunj3 quits (~dunj3@kingdread.de) (*.net *.split) |
| 01:04:05 | × | defanor quits (~defanor@tart.uberspace.net) (*.net *.split) |
| 01:04:05 | × | dminuoso_ quits (~dminuoso@user/dminuoso) (*.net *.split) |
| 01:04:05 | × | Yumemi_ quits (~Yumemi@2001:bc8:47a0:1b14::1) (*.net *.split) |
| 01:04:05 | × | erisco quits (~erisco@d24-141-66-165.home.cgocable.net) (*.net *.split) |
| 01:04:05 | × | SoF quits (~skius@user/skius) (*.net *.split) |
| 01:04:05 | × | Xe quits (~cadey@perl/impostor/xe) (*.net *.split) |
| 01:04:05 | × | sudden quits (~cat@user/sudden) (*.net *.split) |
| 01:04:05 | × | nicole quits (ilbelkyr@libera/staff/ilbelkyr) (*.net *.split) |
| 01:04:05 | × | blackfield quits (~aenima@85.255.4.218) (*.net *.split) |
| 01:04:05 | × | cross quits (~cross@spitfire.i.gajendra.net) (*.net *.split) |
| 01:04:05 | × | eL_Bart0 quits (eL_Bart0@dietunichtguten.org) (*.net *.split) |
| 01:04:06 | × | jjhoo quits (~jahakala@user/jjhoo) (*.net *.split) |
| 01:04:06 | × | iteratee quits (~kyle@162.218.222.207) (*.net *.split) |
| 01:04:28 | × | Alleria quits (~JohnGalt@user/alleria) (*.net *.split) |
| 01:04:28 | × | end quits (~end@user/end/x-0094621) (*.net *.split) |
| 01:04:28 | × | remedan quits (~remedan@ip-94-112-0-18.bb.vodafone.cz) (*.net *.split) |
| 01:04:28 | × | potato44 quits (uid421314@id-421314.lymington.irccloud.com) (*.net *.split) |
| 01:04:28 | × | ubert quits (~Thunderbi@91.141.52.8.wireless.dyn.drei.com) (*.net *.split) |
| 01:04:29 | × | cods quits (~fred@tuxee.net) (*.net *.split) |
| 01:04:29 | × | dexter2 quits (dexter@2a01:7e00::f03c:91ff:fe86:59ec) (*.net *.split) |
| 01:04:29 | × | feetwind quits (~mike@user/feetwind) (*.net *.split) |
| 01:04:29 | × | incertia quits (~incertia@209.122.137.252) (*.net *.split) |
| 01:04:29 | × | swistak- quits (~swistak@185.21.216.141) (*.net *.split) |
| 01:04:29 | × | meinside quits (uid24933@id-24933.helmsley.irccloud.com) (*.net *.split) |
| 01:04:29 | × | nrr_______ quits (sid20938@id-20938.lymington.irccloud.com) (*.net *.split) |
| 01:04:29 | × | hamess_ quits (~hamess@user/hamess) (*.net *.split) |
| 01:04:29 | × | ft quits (~ft@p508db3bc.dip0.t-ipconnect.de) (*.net *.split) |
| 01:04:29 | × | nckx quits (~nckx@libera/staff/owl/nckx) (*.net *.split) |
| 01:04:29 | × | Pozyomka quits (~pyon@user/pyon) (*.net *.split) |
| 01:04:30 | × | connrs quits (~connrs@user/connrs) (*.net *.split) |
| 01:04:30 | × | kraftwerk28 quits (~kraftwerk@164.92.219.160) (*.net *.split) |
| 01:04:30 | × | xsarnik quits (xsarnik@lounge.fi.muni.cz) (*.net *.split) |
| 01:04:30 | × | pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-49-67-70-103-21.dsl.bell.ca) (*.net *.split) |
| 01:04:30 | × | davetapley quits (sid666@uxbridge.irccloud.com) (*.net *.split) |
| 01:04:30 | × | koala_man quits (~vidar@157.146.251.23.bc.googleusercontent.com) (*.net *.split) |
| 01:04:30 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (*.net *.split) |
| 01:04:30 | × | lbseale quits (~quassel@user/ep1ctetus) (*.net *.split) |
| 01:04:30 | × | ggVGc quits (~ggVGc@a.lowtech.earth) (*.net *.split) |
| 01:04:31 | × | NiKaN quits (sid385034@id-385034.helmsley.irccloud.com) (*.net *.split) |
| 01:04:31 | × | gaze_____ quits (sid387101@helmsley.irccloud.com) (*.net *.split) |
| 01:04:31 | × | conjunctive quits (sid433686@helmsley.irccloud.com) (*.net *.split) |
| 01:04:31 | × | tomku quits (~tomku@user/tomku) (*.net *.split) |
| 01:04:31 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (*.net *.split) |
| 01:04:31 | × | nisstyre quits (wes@user/nisstyre) (*.net *.split) |
| 01:04:31 | × | hamster quits (~ham@user/ham) (*.net *.split) |
| 01:04:31 | × | vgtw quits (~vgtw@user/vgtw) (*.net *.split) |
| 01:04:31 | × | Deide quits (d0130db69a@user/deide) (*.net *.split) |
| 01:04:31 | × | mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (*.net *.split) |
| 01:04:31 | × | g00gler quits (uid125351@id-125351.uxbridge.irccloud.com) (*.net *.split) |
| 01:04:31 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (*.net *.split) |
| 01:04:31 | × | AlexNoo quits (~AlexNoo@178.34.151.29) (*.net *.split) |
| 01:04:31 | × | komikat quits (~akshitkr@218.185.248.66) (*.net *.split) |
| 01:04:32 | × | shriekingnoise quits (~shrieking@186.137.175.87) (*.net *.split) |
| 01:04:32 | × | oo_miguel quits (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (*.net *.split) |
| 01:04:32 | × | xff0x quits (~xff0x@ai096045.d.east.v6connect.net) (*.net *.split) |
| 01:04:32 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (*.net *.split) |
| 01:04:32 | × | andjjj23_ quits (~irc@107.170.228.47) (*.net *.split) |
| 01:04:32 | × | bliminse quits (~bliminse@user/bliminse) (*.net *.split) |
| 01:04:32 | × | motherfsck quits (~motherfsc@user/motherfsck) (*.net *.split) |
| 01:04:32 | × | TheCatCollective quits (NyaaTheKit@user/calculuscat) (*.net *.split) |
| 01:04:33 | × | Logio quits (em@kapsi.fi) (*.net *.split) |
| 01:04:33 | × | tomboy64 quits (~tomboy64@user/tomboy64) (*.net *.split) |
| 01:04:33 | × | leeb quits (~leeb@tk2-243-31079.vs.sakura.ne.jp) (*.net *.split) |
| 01:04:33 | × | doyougnu quits (~doyougnu@45.46.170.68) (*.net *.split) |
| 01:04:33 | × | koz quits (~koz@121.99.240.58) (*.net *.split) |
| 01:04:33 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (*.net *.split) |
| 01:04:33 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (*.net *.split) |
| 01:04:33 | × | hc quits (~hc@mail.hce.li) (*.net *.split) |
| 01:04:34 | × | Arsen quits (arsen@gentoo/developer/managarm.dev.Arsen) (*.net *.split) |
| 01:04:34 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (*.net *.split) |
| 01:04:34 | × | hueso quits (~root@user/hueso) (*.net *.split) |
| 01:04:34 | × | benmachine quits (bm380@pip.srcf.societies.cam.ac.uk) (*.net *.split) |
| 01:04:34 | × | _________ quits (~nobody@user/noodly) (*.net *.split) |
| 01:04:34 | × | pie_ quits (~pie_bnc@user/pie/x-2818909) (*.net *.split) |
| 01:04:34 | × | tertek quits (~tertek@user/tertek) (*.net *.split) |
| 01:04:34 | × | dumptruckman quits (~dumptruck@23-239-13-136.ip.linodeusercontent.com) (*.net *.split) |
| 01:04:34 | × | Sgeo quits (~Sgeo@user/sgeo) (*.net *.split) |
| 01:04:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) (*.net *.split) |
| 01:04:35 | × | infinity0 quits (~infinity0@pwned.gg) (*.net *.split) |
| 01:04:35 | × | haasn` quits (~nand@haasn.dev) (*.net *.split) |
| 01:04:35 | × | TMA quits (tma@twin.jikos.cz) (*.net *.split) |
| 01:04:35 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (*.net *.split) |
| 01:04:35 | × | andreas303 quits (andreas303@is.drunk.and.ready-to.party) (*.net *.split) |
| 01:04:35 | × | srk quits (~sorki@user/srk) (*.net *.split) |
| 01:04:35 | × | [exa] quits (~exa@user/exa/x-3587197) (*.net *.split) |
| 01:04:35 | × | mulk quits (~mulk@p5b2dc93f.dip0.t-ipconnect.de) (*.net *.split) |
| 01:04:36 | × | chessai quits (sid225296@id-225296.lymington.irccloud.com) (*.net *.split) |
| 01:04:36 | × | astra quits (sid289983@user/amish) (*.net *.split) |
| 01:04:36 | × | bjs quits (sid190364@user/bjs) (*.net *.split) |
| 01:04:36 | × | shawwwn quits (sid6132@id-6132.helmsley.irccloud.com) (*.net *.split) |
| 01:04:36 | × | actioninja quits (~actioninj@user/actioninja) (*.net *.split) |
| 01:04:36 | × | son0p quits (~ff@181.136.122.143) (*.net *.split) |
| 01:04:36 | × | driib quits (~driib@vmi931078.contaboserver.net) (*.net *.split) |
| 01:04:36 | × | Buggys quits (Buggys@shelltalk.net) (*.net *.split) |
| 01:04:36 | × | mankyKitty quits (sid31287@id-31287.helmsley.irccloud.com) (*.net *.split) |
| 01:04:37 | × | riatre quits (~quassel@2001:310:6000:f::5198:1) (*.net *.split) |
| 01:04:37 | × | CAT_S quits (apic@brezn3.muc.ccc.de) (*.net *.split) |
| 01:04:37 | × | paddymahoney quits (~paddymaho@cpe883d24bcf597-cmbc4dfb741f80.cpe.net.cable.rogers.com) (*.net *.split) |
| 01:04:37 | × | duncan quits (~duncan@nat-server.ehlab.uk) (*.net *.split) |
| 01:04:38 | Lord_of_Life_ | is now known as Lord_of_Life |
| 01:05:57 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 01:06:13 | → | caef^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 01:06:33 | → | AlexNoo joins (~AlexNoo@178.34.151.29) |
| 01:06:33 | → | komikat joins (~akshitkr@218.185.248.66) |
| 01:06:33 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 01:06:33 | → | oo_miguel joins (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
| 01:06:33 | → | xff0x joins (~xff0x@ai096045.d.east.v6connect.net) |
| 01:06:33 | → | andjjj23_ joins (~irc@107.170.228.47) |
| 01:06:33 | → | bliminse joins (~bliminse@user/bliminse) |
| 01:06:33 | → | motherfsck joins (~motherfsc@user/motherfsck) |
| 01:06:33 | → | TheCatCollective joins (NyaaTheKit@user/calculuscat) |
| 01:06:33 | → | Logio joins (em@kapsi.fi) |
| 01:06:33 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 01:06:33 | → | leeb joins (~leeb@tk2-243-31079.vs.sakura.ne.jp) |
| 01:06:33 | → | doyougnu joins (~doyougnu@45.46.170.68) |
| 01:06:33 | → | koz joins (~koz@121.99.240.58) |
| 01:06:33 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 01:06:33 | → | tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 01:06:33 | → | hc joins (~hc@mail.hce.li) |
| 01:06:33 | → | Arsen joins (arsen@gentoo/developer/managarm.dev.Arsen) |
| 01:06:33 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 01:06:33 | → | hueso joins (~root@user/hueso) |
| 01:06:33 | → | benmachine joins (bm380@pip.srcf.societies.cam.ac.uk) |
| 01:06:33 | → | _________ joins (~nobody@user/noodly) |
| 01:06:33 | → | pie_ joins (~pie_bnc@user/pie/x-2818909) |
| 01:06:36 | → | targetdi1k joins (~daemonchi@45-33-4-162.ip.linodeusercontent.com) |
| 01:06:36 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 01:06:36 | → | teqwve joins (teqwve@2a01:4f8:c2c:e5b0::1) |
| 01:06:36 | → | yahb2 joins (~yahb2@static.56.27.47.78.clients.your-server.de) |
| 01:06:36 | → | troydm joins (~troydm@user/troydm) |
| 01:06:36 | → | arahael joins (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) |
| 01:06:36 | → | ridcully joins (~ridcully@p57b52dae.dip0.t-ipconnect.de) |
| 01:06:36 | → | nek0 joins (~nek0@2a01:4f8:222:2b41::12) |
| 01:06:36 | → | John_Ivan joins (~John_Ivan@user/john-ivan/x-1515935) |
| 01:06:36 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 01:06:36 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) |
| 01:06:36 | → | inedia joins (~irc@23.153.248.82) |
| 01:06:36 | → | steew joins (~steew@user/steew) |
| 01:06:36 | → | turlando joins (~turlando@user/turlando) |
| 01:06:36 | → | bramhaag7 joins (~bramhaag@endeavour.server.bramh.me) |
| 01:06:36 | → | rncwnd joins (~quassel@2a01:4f8:221:27c6::1) |
| 01:06:36 | → | m1dnight joins (~christoph@78-22-4-67.access.telenet.be) |
| 01:06:36 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 01:06:36 | → | cawfee_ joins (~root@2406:3003:2077:2758::babe) |
| 01:06:36 | → | V joins (~v@ircpuzzles/2022/april/winner/V) |
| 01:06:36 | → | dyniec joins (~dyniec@dybiec.info) |
| 01:06:36 | → | arkeet joins (~arkeet@moriya.ca) |
| 01:06:36 | → | codedmart joins (codedmart@2600:3c01::f03c:92ff:fefe:8511) |
| 01:06:36 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 01:06:36 | → | noctux1 joins (Hfi6K5vcqP@user/noctux) |
| 01:06:36 | → | dunj3 joins (~dunj3@kingdread.de) |
| 01:06:36 | → | defanor joins (~defanor@tart.uberspace.net) |
| 01:06:36 | → | dminuoso_ joins (~dminuoso@user/dminuoso) |
| 01:06:36 | → | Yumemi_ joins (~Yumemi@2001:bc8:47a0:1b14::1) |
| 01:06:36 | → | SoF joins (~skius@user/skius) |
| 01:06:36 | → | erisco joins (~erisco@d24-141-66-165.home.cgocable.net) |
| 01:06:36 | → | Xe joins (~cadey@perl/impostor/xe) |
| 01:06:36 | → | sudden joins (~cat@user/sudden) |
| 01:06:36 | → | nicole joins (ilbelkyr@libera/staff/ilbelkyr) |
| 01:06:36 | → | blackfield joins (~aenima@85.255.4.218) |
| 01:06:36 | → | cross joins (~cross@spitfire.i.gajendra.net) |
| 01:06:36 | → | jjhoo joins (~jahakala@user/jjhoo) |
| 01:06:36 | → | iteratee joins (~kyle@162.218.222.207) |
| 01:06:36 | molybdenum.libera.chat | sets mode +v yahb2 |
| 01:06:39 | × | Xe quits (~cadey@perl/impostor/xe) (Quit: WeeChat 4.1.0) |
| 01:06:39 | × | haskellbridge quits (~haskellbr@069-135-003-034.biz.spectrum.com) (Excess Flood) |
| 01:06:40 | × | pie_ quits (~pie_bnc@user/pie/x-2818909) (Max SendQ exceeded) |
| 01:06:40 | × | _________ quits (~nobody@user/noodly) (Max SendQ exceeded) |
| 01:06:40 | × | Arsen quits (arsen@gentoo/developer/managarm.dev.Arsen) (Max SendQ exceeded) |
| 01:06:44 | → | kaol_ joins (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 01:06:44 | → | tertek joins (~tertek@user/tertek) |
| 01:06:44 | → | dumptruckman joins (~dumptruck@23-239-13-136.ip.linodeusercontent.com) |
| 01:06:44 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 01:06:44 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) |
| 01:06:44 | → | infinity0 joins (~infinity0@pwned.gg) |
| 01:06:44 | → | 040AADFUL joins (~nand@haasn.dev) |
| 01:06:44 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 01:06:44 | → | TMA joins (tma@twin.jikos.cz) |
| 01:06:44 | → | andreas303 joins (andreas303@is.drunk.and.ready-to.party) |
| 01:06:44 | → | srk joins (~sorki@user/srk) |
| 01:06:44 | → | [exa] joins (~exa@user/exa/x-3587197) |
| 01:06:44 | → | mulk joins (~mulk@p5b2dc93f.dip0.t-ipconnect.de) |
| 01:06:44 | → | astra joins (sid289983@user/amish) |
| 01:06:44 | → | chessai joins (sid225296@id-225296.lymington.irccloud.com) |
| 01:06:44 | → | bjs joins (sid190364@user/bjs) |
| 01:06:44 | → | shawwwn joins (sid6132@id-6132.helmsley.irccloud.com) |
| 01:06:44 | → | actioninja joins (~actioninj@user/actioninja) |
| 01:06:44 | → | son0p joins (~ff@181.136.122.143) |
| 01:06:44 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 01:06:44 | → | Buggys joins (Buggys@shelltalk.net) |
| 01:06:44 | → | mankyKitty joins (sid31287@id-31287.helmsley.irccloud.com) |
| 01:06:44 | → | riatre joins (~quassel@2001:310:6000:f::5198:1) |
| 01:06:44 | → | CAT_S joins (apic@brezn3.muc.ccc.de) |
| 01:06:44 | → | paddymahoney joins (~paddymaho@cpe883d24bcf597-cmbc4dfb741f80.cpe.net.cable.rogers.com) |
| 01:06:44 | → | duncan joins (~duncan@nat-server.ehlab.uk) |
| 01:06:44 | → | pie__ joins (~pie_bnc@user/pie/x-2818909) |
| 01:06:50 | → | Arsen joins (arsen@gentoo/developer/managarm.dev.Arsen) |
| 01:06:53 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 01:06:54 | → | Xe joins (~cadey@perl/impostor/xe) |
| 01:07:04 | → | _________ joins (~nobody@user/noodly) |
| 01:07:17 | × | cross quits (~cross@spitfire.i.gajendra.net) (Max SendQ exceeded) |
| 01:07:29 | → | Alleria joins (~JohnGalt@user/alleria) |
| 01:07:29 | → | end joins (~end@user/end/x-0094621) |
| 01:07:29 | → | remedan joins (~remedan@ip-94-112-0-18.bb.vodafone.cz) |
| 01:07:29 | → | potato44 joins (uid421314@id-421314.lymington.irccloud.com) |
| 01:07:29 | → | ubert joins (~Thunderbi@91.141.52.8.wireless.dyn.drei.com) |
| 01:07:29 | → | cods joins (~fred@tuxee.net) |
| 01:07:29 | → | dexter2 joins (dexter@2a01:7e00::f03c:91ff:fe86:59ec) |
| 01:07:29 | → | feetwind joins (~mike@user/feetwind) |
| 01:07:29 | → | incertia joins (~incertia@209.122.137.252) |
| 01:07:29 | → | swistak- joins (~swistak@185.21.216.141) |
| 01:07:29 | → | meinside joins (uid24933@id-24933.helmsley.irccloud.com) |
| 01:07:29 | → | nrr_______ joins (sid20938@id-20938.lymington.irccloud.com) |
| 01:07:29 | → | hamess_ joins (~hamess@user/hamess) |
| 01:07:29 | → | ft joins (~ft@p508db3bc.dip0.t-ipconnect.de) |
| 01:07:29 | → | nckx joins (~nckx@libera/staff/owl/nckx) |
| 01:07:29 | → | Pozyomka joins (~pyon@user/pyon) |
| 01:07:29 | → | connrs joins (~connrs@user/connrs) |
| 01:07:29 | → | kraftwerk28 joins (~kraftwerk@164.92.219.160) |
| 01:07:29 | → | xsarnik joins (xsarnik@lounge.fi.muni.cz) |
| 01:07:29 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-49-67-70-103-21.dsl.bell.ca) |
| 01:07:29 | → | davetapley joins (sid666@uxbridge.irccloud.com) |
| 01:07:29 | → | koala_man joins (~vidar@157.146.251.23.bc.googleusercontent.com) |
| 01:07:29 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 01:07:29 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 01:07:29 | → | ggVGc joins (~ggVGc@a.lowtech.earth) |
| 01:07:29 | → | NiKaN joins (sid385034@id-385034.helmsley.irccloud.com) |
| 01:07:29 | → | gaze_____ joins (sid387101@helmsley.irccloud.com) |
| 01:07:29 | → | conjunctive joins (sid433686@helmsley.irccloud.com) |
| 01:07:29 | → | tomku joins (~tomku@user/tomku) |
| 01:07:29 | → | nisstyre joins (wes@user/nisstyre) |
| 01:07:29 | → | hamster joins (~ham@user/ham) |
| 01:07:29 | → | vgtw joins (~vgtw@user/vgtw) |
| 01:07:29 | → | Deide joins (d0130db69a@user/deide) |
| 01:07:29 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 01:07:29 | → | g00gler joins (uid125351@id-125351.uxbridge.irccloud.com) |
| 01:07:29 | → | Katarushisu1 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 01:07:30 | × | remedan quits (~remedan@ip-94-112-0-18.bb.vodafone.cz) (Max SendQ exceeded) |
| 01:07:31 | × | superbil quits (~superbil@1-34-176-171.hinet-ip.hinet.net) (*.net *.split) |
| 01:07:31 | × | Axman6 quits (~Axman6@user/axman6) (*.net *.split) |
| 01:07:44 | → | mikess joins (~sam@user/mikess) |
| 01:09:51 | → | Axman6 joins (~Axman6@user/axman6) |
| 01:09:51 | → | superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net) |
| 01:09:52 | × | NiKaN quits (sid385034@id-385034.helmsley.irccloud.com) (Ping timeout: 250 seconds) |
| 01:09:54 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:10:18 | → | raym joins (~ray@user/raym) |
| 01:11:44 | → | remedan joins (~remedan@ip-94-112-0-18.bb.vodafone.cz) |
| 01:12:53 | → | NiKaN joins (sid385034@id-385034.helmsley.irccloud.com) |
| 01:13:14 | → | cross joins (~cross@spitfire.i.gajendra.net) |
| 01:13:24 | → | rosco joins (~rosco@175.136.158.171) |
| 01:16:03 | → | eL_Bart0 joins (eL_Bart0@dietunichtguten.org) |
| 01:17:46 | → | notzmv joins (~zmv@user/notzmv) |
| 01:18:06 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 01:19:53 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 01:22:16 | → | emmanuelux_ joins (~emmanuelu@user/emmanuelux) |
| 01:24:11 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 01:24:14 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 256 seconds) |
| 01:25:23 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 01:26:07 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Remote host closed the connection) |
| 01:26:12 | → | haskellbridge joins (~haskellbr@069-135-003-034.biz.spectrum.com) |
| 01:26:12 | ChanServ | sets mode +v haskellbridge |
| 01:26:21 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 01:31:07 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 01:32:29 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 01:32:48 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 01:34:11 | → | shailangsa joins (~shailangs@host109-152-9-157.range109-152.btcentralplus.com) |
| 01:34:14 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 01:36:06 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 01:40:40 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 01:42:39 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 01:43:17 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 01:47:37 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 01:50:22 | → | trev joins (~trev@user/trev) |
| 01:53:50 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 01:54:16 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 256 seconds) |
| 01:56:24 | × | nonzen_ quits (~nonzen@user/nonzen) (Ping timeout: 252 seconds) |
| 01:56:40 | → | nonzen joins (~nonzen@user/nonzen) |
| 01:59:30 | → | ubert1 joins (~Thunderbi@178.165.189.208.wireless.dyn.drei.com) |
| 01:59:59 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 02:00:01 | × | ubert quits (~Thunderbi@91.141.52.8.wireless.dyn.drei.com) (Ping timeout: 256 seconds) |
| 02:00:01 | ubert1 | is now known as ubert |
| 02:03:59 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 256 seconds) |
| 02:05:56 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 02:08:44 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 02:10:39 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 02:11:29 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 02:14:03 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 02:14:12 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 02:17:23 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 02:22:48 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 02:23:10 | × | rosco quits (~rosco@175.136.158.171) (Ping timeout: 256 seconds) |
| 02:23:22 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 02:23:59 | → | rosco joins (~rosco@175.136.158.171) |
| 02:24:49 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 02:29:10 | × | matijja quits (~matijja@193.77.181.201) (Ping timeout: 260 seconds) |
| 02:29:11 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 02:29:19 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 255 seconds) |
| 02:30:00 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 02:30:58 | → | matijja joins (~matijja@193.77.181.201) |
| 02:32:01 | × | xff0x quits (~xff0x@ai096045.d.east.v6connect.net) (Ping timeout: 255 seconds) |
| 02:32:02 | → | Square2 joins (~Square4@user/square) |
| 02:35:13 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 02:35:46 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 02:36:36 | → | Guest3 joins (~Guest3@149.159.194.55) |
| 02:37:04 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 02:37:38 | <Guest3> | Why are partial functions bad? I am writing a IO action and trying to decide if I should just use error or if I should use Maybe and let the clients throw the error. |
| 02:38:01 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 02:38:01 | <Guest3> | Using Maybe would force all the clients to pattern match |
| 02:39:09 | <geekosaur> | I don't see that as a bad thing |
| 02:39:25 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 02:40:19 | <geekosaur> | if you use `error` and someone does want to catch it, they have to do it in `IO` *and* make sure it is actually executed in the `try` or `handle` so the exception doesn't leak through unevaluated and "go off" somewhere else |
| 02:41:11 | <Guest3> | It is an IO action, so I suppose they have to be in IO to catch it. |
| 02:41:39 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 02:41:52 | <geekosaur> | all exceptions must be caught in `IO` |
| 02:42:11 | <monochrom> | Have you considered defining your own exception to throw so it is easily distinguishable from the millions of other exceptions out there? |
| 02:42:13 | <Guest3> | Yes, but I meant, I am using `error` inside and IO action. |
| 02:42:20 | <[Leary]> | Guest3: Since you're in IO; remove `error` from your list of options and replace it with `throwIO`. |
| 02:42:33 | <[Leary]> | Partial functions are bad, exceptions aren't. |
| 02:42:58 | <Guest3> | Why are partial functions bad? And isn't `error` just throwing an exception? |
| 02:43:09 | <Guest3> | I suppose it just throws a generic exception |
| 02:43:28 | <geekosaur> | there is a difference between synchronous exceptions like thrown by `throwIO` and asynchronous exceptions like thrown by `error` |
| 02:43:32 | <Guest3> | Actually, this is a partial action (not a partial function) |
| 02:43:37 | <monochrom> | That is not how I classify good vs bad. |
| 02:43:51 | <Guest3> | error isn't asynchronous if i recall correctly |
| 02:44:11 | <monochrom> | Making my life harder is bad. After that, making other people's lives harder is bad. |
| 02:44:37 | × | matijja quits (~matijja@193.77.181.201) (Ping timeout: 255 seconds) |
| 02:44:54 | <monochrom> | 1% of the time partial functions make my and people's lives easier. 99% of the time harder. I don't ban partial functions. I ban making lives harder. |
| 02:45:01 | <geekosaur> | but partial functions are bad because they raise exceptions in pure code (not `IO`) and are thus especially difficult to catch because you may have to `deepseq` it inside a `catch`/`handle`/etc. to ensure the exception is actually thrown inside the handler |
| 02:45:42 | <geekosaur> | if it isn't fully evaluated inside the handler, it may leak out and detonate outside the handler |
| 02:46:13 | <Guest3> | ah, laziness |
| 02:46:15 | <monochrom> | Likewise, if I expect other people to catch what I throw, 99% of the time their lives are harder if I throw error which is hugely generic and bland, and then what, they have to parse my string to see it's from me? Why would I inflict this on them? |
| 02:46:49 | <monochrom> | Therefore, I define my own exception type and throw it. Then they have a much easier time checking that it's my custom exception. |
| 02:47:11 | <jackdk> | I have found that avoiding partial functions is much easier than I thought when I first started learning Haskell. Becoming fluent with Functor/Applicative/Monad helped a lot there. |
| 02:47:11 | <zzz> | can i use stm for ipc? |
| 02:47:20 | <Guest3> | monochrom, good point. In my case, I don't expect anyone to catch it. Only possibility is crashing. |
| 02:47:21 | <geekosaur> | and if there is associated data, you can make it part of the exception instead of forcing users to parse it out of the message |
| 02:47:27 | → | matijja joins (~matijja@193.77.181.201) |
| 02:47:35 | <Guest3> | correct |
| 02:48:07 | <Guest3> | zzz, by ipc do you mean across process boundaries? |
| 02:48:26 | <geekosaur> | zzz, only between threads, not processes |
| 02:49:54 | <zzz> | yes. i figured |
| 02:50:00 | <zzz> | thanks |
| 02:50:45 | <zzz> | i'm no t sure which form of ipc to use |
| 02:51:15 | <zzz> | i think i'm on the fence between sockets and named pipes |
| 02:51:29 | <geekosaur> | sockets, if you value your sanity |
| 02:51:48 | <monochrom> | Well, it says i"p"c not i"t"c. :D |
| 02:52:34 | <monochrom> | Is that because socket is bidirectional, pipes are unidirectional and then you need two of them? |
| 02:52:38 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 02:52:46 | <geekosaur> | partially |
| 02:53:12 | <monochrom> | I did inflict "make two pipes per child, there are n children" on my students in the exam. >:) |
| 02:53:33 | <geekosaur> | to use a named pipe reasonably you must open it `O_RDWR` and keep it open for as long as you are running, and have some way other than EOF to detect when another process closes it |
| 02:53:52 | <geekosaur> | if you use EOF and close it, the FIFO is subsequently dead and you have to remove and recreate it |
| 02:53:55 | <monochrom> | Ah right. That one is annoying yeah. |
| 02:54:41 | <zzz> | so sockets |
| 02:54:48 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 02:54:59 | <zzz> | which library is recommended? |
| 02:55:10 | <zzz> | for i"p"c |
| 02:56:32 | → | whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com) |
| 02:57:09 | <zzz> | Network.Socket ? |
| 02:57:42 | <geekosaur> | I don't think there currently exist higher level abstractions for AF_UNIX sockets |
| 02:58:02 | <geekosaur> | there's lots for TCP but not for other uses |
| 03:00:10 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 03:01:11 | <geekosaur> | (I'm pretty used to the lower level ones anyway, since I spent years programming in C) |
| 03:05:37 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Quit: Konversation terminated!) |
| 03:06:07 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 03:06:24 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 03:06:42 | <zzz> | i want high lever. it's a pretty simple use case and i'm just avoiding using a simple text file |
| 03:06:45 | × | td_ quits (~td@i5387092B.versanet.de) (Ping timeout: 256 seconds) |
| 03:06:52 | <zzz> | *level |
| 03:07:15 | <zzz> | i have no intention of exploring this subject deeply atm |
| 03:08:16 | <tabemann> | stupid question about partial functions - how does STM prevent partial functions from raising exceptions and them leaking out from atomically? |
| 03:08:21 | → | td_ joins (~td@i5387091D.versanet.de) |
| 03:09:30 | <tabemann> | i.e. allowing state that shouldn't be visible to become visible to the outside world |
| 03:09:57 | <tabemann> | apparently this issue is a big impediment to the implementation of STM in many programming languages |
| 03:10:00 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 03:10:01 | <zzz> | atomically discards any transaction in the event of an exception |
| 03:10:36 | <zzz> | either it performs all or none |
| 03:10:38 | <tabemann> | zzz: what I mean is because of laziness the exception could escape from the atomically |
| 03:11:04 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 03:11:19 | <zzz> | the entire transaction is rolled back as far as i know |
| 03:11:34 | <tabemann> | to prevent that you'd have to deepseq the value returned from atomically |
| 03:11:37 | <zzz> | but it's easy enough to test |
| 03:11:59 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 03:14:34 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) (Remote host closed the connection) |
| 03:14:48 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) |
| 03:15:26 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 03:17:25 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 03:20:36 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Read error: Connection reset by peer) |
| 03:22:23 | → | Katarushisu1 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 03:25:27 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 03:26:06 | <EvanR> | Guest3, partial functions are just fine as long as no one uses it on the missing parts of the domain! |
| 03:26:47 | <EvanR> | > map head (group "hello world") |
| 03:26:48 | <lambdabot> | "helo world" |
| 03:27:18 | <EvanR> | but this is a big if and isn't tracked by the type system |
| 03:28:07 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 240 seconds) |
| 03:28:33 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 03:28:51 | <jackdk> | In your instance, `group` should return `[NonEmpty a]`, right? But the general point stands |
| 03:29:12 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 03:29:18 | <EvanR> | (not that this applies to IO actions which aren't functions and no one would be surprised if they throwIO for some reason) |
| 03:29:56 | <EvanR> | yeah my example in fact has a way to be well typed, terrible example |
| 03:30:17 | × | edr quits (~edr@user/edr) (Quit: Leaving) |
| 03:30:17 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 03:30:21 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 03:31:48 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 03:32:05 | <probie> | EvanR: There's a pretty spooky way to track this in the type system |
| 03:32:12 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 03:35:21 | × | ddellacosta quits (~ddellacos@ool-44c73d16.dyn.optonline.net) (Ping timeout: 245 seconds) |
| 03:37:11 | <EvanR> | tabemann, if the transaction succeeds the transaction succeeds. Of course it could have set something up which when evaluate crashes whatever thread. Which is why you probably want to evaluate anything you put in an MVar |
| 03:37:32 | → | ddellacosta joins (~ddellacos@ool-44c73d16.dyn.optonline.net) |
| 03:37:32 | <EvanR> | or a TVar |
| 03:38:03 | <EvanR> | but I can see use cases where you don't want to fully evaluate it |
| 03:39:29 | → | Noob_Programmer joins (~Noob_Prog@2409:408d:683:c243:a574:68ee:74be:cb54) |
| 03:41:00 | <tabemann> | https://pastebin.com/zRm42Nvf |
| 03:41:22 | <tabemann> | this somehow doesn't raise an exception |
| 03:42:07 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds) |
| 03:42:37 | <tabemann> | because it ought to allow the divide-by-zero to escape the atomically |
| 03:42:51 | <tabemann> | because it is only forced by the "show" outside it |
| 03:43:33 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 03:43:41 | <EvanR> | uh, what does the basically putStrLn (show (1 `div` 0)) do if not crash |
| 03:43:49 | <EvanR> | should crash the thread right |
| 03:44:03 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 03:44:09 | <EvanR> | which is a silent affair by default |
| 03:46:13 | <tabemann> | I added a putStrLn $ show 256 to the loop to make it clear that the loop isn't crashing (because it outputs alternating 1's and 256's) |
| 03:46:34 | <tabemann> | while the main thread is outputting 'foo's |
| 03:46:50 | <EvanR> | % forkIO (print (1 `div` 0)) >> print "ok" >> threadDelay 100000 |
| 03:46:50 | <yahb2> | <interactive>:5:1: error: ; Variable not in scope: forkIO :: IO () -> IO a1 ; ; <interactive>:5:45: error: ; Variable not in scope: threadDelay :: t0 -> IO b |
| 03:48:05 | <Guest3> | it's not crashing because, bar is always 1 |
| 03:48:11 | <[Leary]> | tabemann: (writeTVar foo 0 >> writeTVar foo 1) = writeTVar foo 1 |
| 03:48:17 | × | Noob_Programmer quits (~Noob_Prog@2409:408d:683:c243:a574:68ee:74be:cb54) (Quit: Client closed) |
| 03:48:23 | <Guest3> | oh, wait never mid |
| 03:48:35 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 03:48:46 | <Guest3> | ah, no, i stand by it. bar is always 1 |
| 03:48:56 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 03:49:00 | <tabemann> | the key thing is that one thread is never seeing the case where foo is 0 in the other thread |
| 03:49:18 | <EvanR> | yeah, why would anyone see 0 |
| 03:49:24 | <tabemann> | i.e. something must be protecting it from seeing this intermediate state and not allowing it to escape |
| 03:49:25 | <Guest3> | yes, because it's a transaction |
| 03:49:31 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 255 seconds) |
| 03:49:35 | <EvanR> | hence the atomically |
| 03:49:56 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 03:50:00 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 03:50:14 | <EvanR> | what I thought you were going to try to do was put an exploding value in the TVar |
| 03:50:29 | <tabemann> | this whole exercise was raised by the question of other language's STM implementations, where all kinds of nastiness can occur from things like divide-by-zeros occurring within transactions |
| 03:50:50 | <EvanR> | if divide by zero happens during the transaction, then transaction fails |
| 03:51:12 | <EvanR> | otherwise it may succeed but set some other thread up to crash by e.g. storing a bomb somewhere |
| 03:51:24 | <tabemann> | the key thing I was trying to do is to allow the divide by zero to escape by the divide only being forced later on, outside the transaction |
| 03:51:59 | <monochrom> | This transaction includes only reading bar. |
| 03:52:26 | <Guest3> | tabemann, that's not a problem. |
| 03:53:01 | <monochrom> | Unless you say something like "atomically (if div 1 0 then read/write this else read/write that)" you will not have a division by 0 inside a transaction. |
| 03:53:04 | <tabemann> | to avoid this it must do something like ensure that all variables read before and after the transaction not only having not changed state, but also having never changed state - and changed back - in between |
| 03:53:48 | <EvanR> | stuff you write to a TVar or MVar or Chan etc isn't necessarily evaluated yet |
| 03:54:06 | <EvanR> | certainly a tricky thing which could bite you |
| 03:54:21 | <monochrom> | And pure too. pure doesn't evaluate either. |
| 03:55:09 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:55:09 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:55:10 | <Guest3> | tabemann, the exception happening later won't affect the transaction. The only side-effect you can do inside an STM transaction is modify TVars |
| 03:55:11 | <tabemann> | monochrom: which I was doing with return (which is pure, but I'm using an older version of Stack because I haven't played with Haskell in ages and did not feel like installing a new version right now) |
| 03:55:13 | <monochrom> | pure (div 1 0), writeTVar v (div 1 0) all do not including performing the division insde the transaction. |
| 03:55:27 | <Guest3> | And you can't modify TVars outside a transaction |
| 03:55:34 | <Guest3> | The type system takes care of this |
| 03:56:10 | <monochrom> | But like I said you can play with a transaction that needs conditional branching that depends on div 1 0. |
| 03:57:12 | <EvanR> | modifyTVar' tv (`div` 0) |
| 03:57:12 | <tabemann> | Guest3: of course |
| 03:57:23 | → | johnw joins (~johnw@69.62.242.138) |
| 03:57:38 | <EvanR> | this will take the liberty of evaluating the division by zero for you now |
| 03:57:38 | <monochrom> | None of this should be surprising. |
| 03:57:51 | <tabemann> | the thing is the point of this was to enable one thread to see another thread's intermediate state |
| 03:57:57 | <EvanR> | without the "prime" you would be writing a bomb to the TVar |
| 03:58:12 | <EvanR> | (if you don't rollback) |
| 03:58:17 | <tabemann> | i.e. make atomically non-atomic |
| 03:58:29 | <EvanR> | what language lets you see STM transactions intermediate state? That sounds broken |
| 03:58:40 | <monochrom> | And Haskell is not nicer or nastier than other languages in this regard because if you insert enough $!'s you can recover other languages' evaluation order. Try pure $! div 1 0. |
| 03:59:05 | <tabemann> | EvanR: that's why STM hasn't really caught on outside of Haskell and Clojure |
| 03:59:22 | <tabemann> | Haskell is uniquely well-suited to STM |
| 03:59:26 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Remote host closed the connection) |
| 03:59:26 | <monochrom> | All kinds of exceptions can still happen in STM too so what it does in response is already well-defined. |
| 03:59:28 | <EvanR> | because no one implements it correctly? |
| 03:59:32 | × | ddellacosta quits (~ddellacos@ool-44c73d16.dyn.optonline.net) (Quit: WeeChat 4.1.1) |
| 03:59:38 | <EvanR> | I figured clojure was correct |
| 04:00:09 | <tabemann> | EvanR: because most languages provide no mechanism to ensuring the correctness of STM |
| 04:00:20 | <tabemann> | it's up to the programmer to not fubar it |
| 04:00:26 | <EvanR> | well neither does haskell, STM is a GHC feature |
| 04:00:52 | <tabemann> | well yes, but Haskell enables constructing a type system that enforces STM |
| 04:00:53 | <monochrom> | I don't think you put the reason the right way. |
| 04:00:55 | <EvanR> | you can't program it with just forkIO |
| 04:01:16 | <[Leary]> | The real issue that stymies STM in other languages is impurity. Side effects in a transaction will be observed even if the transaction is cancelled. |
| 04:01:18 | <tabemann> | EvanR: exactly |
| 04:01:29 | <tabemann> | [Leary]: precisely |
| 04:01:53 | <monochrom> | I think the right way is this. By analogy to Haskell: Imagine inside atomically you can play with both TVar and IORef. That's what other languages allow, and that's why it becomes problematic. |
| 04:02:01 | <[Leary]> | However, execeptions themselves are not an issue, as the GHC implementation proves. |
| 04:02:25 | <tabemann> | so what I've discovered today is that atomically has some magic that prevents intermediate states from being read, to avoid constructing logic bombs that expose other threads' intemediate states |
| 04:02:51 | <EvanR> | I'm still not sure how the lazy division by zero would expose any intermediate states of anything |
| 04:03:06 | <EvanR> | if you divide by zero in the transaction it is canceled as expected |
| 04:03:16 | <[Leary]> | That's not deep magic, it's the core idea of using atomic transactions (however you implement them). |
| 04:03:17 | <monochrom> | Haskell's solution is to ban IORef inside STM, but still allow it in IO. Clojure's solution is to ban IORef altogether; all mutable vars are TVars. |
| 04:04:36 | <tabemann> | EvanR: laziness would still allow the divide by zero to escape; the magic must be to check all reads before and after to ensure that any updates, even if the actual values haven't changed before and after, abort the transaction |
| 04:06:11 | <EvanR> | your test of trying to read a zero from a TVar which is always left as 1 in the writing transaction just seems to test STM and not any exception case, your writing transaction never attempted to crash |
| 04:06:38 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 04:06:53 | <tabemann> | EvanR: I'm writing alternating 0's and 1's to the TVar |
| 04:07:09 | <tabemann> | in a transaction, such that from the outside PoV the TVar should always be 1 |
| 04:07:10 | <EvanR> | yes but the changes are not visible until after the comment |
| 04:07:31 | <EvanR> | I'm not sure how a division by zero in an unrelated thread would have any effect anyway |
| 04:07:48 | × | Guest3 quits (~Guest3@149.159.194.55) (Quit: Client closed) |
| 04:08:35 | <monochrom> | Sure. Any other transaction reading it will get 1. Albeit after much retries. |
| 04:08:52 | <monochrom> | What is the surprise again? |
| 04:09:13 | <EvanR> | you could have just tested the value for zero and printed an emoji if so |
| 04:09:18 | → | Guest3 joins (~Guest3@149.159.194.55) |
| 04:09:20 | × | rosco quits (~rosco@175.136.158.171) (Quit: leaving) |
| 04:09:43 | <tabemann> | I basically was trying to see whether a naive approach that just catches exceptions within the reading thread is being applied |
| 04:10:27 | <monochrom> | Huh but you wrote no catcher. |
| 04:11:01 | <EvanR> | they mean try to show the runtime system doing something really dumb |
| 04:11:05 | <tabemann> | monochrome: what I meant is whether atomically just relies on catching exceptions and aborting if any are raised |
| 04:11:07 | <monochrom> | Are you sure you didn't mix up "catch" with "throw". |
| 04:11:21 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 256 seconds) |
| 04:12:02 | <EvanR> | is there a language which does STM this way? |
| 04:12:37 | <tabemann> | probably most, as most languages aren't lazy |
| 04:12:38 | <EvanR> | catching exceptions in everyone elses thread |
| 04:12:53 | <EvanR> | rather than the thread doing the atomically |
| 04:13:04 | <tabemann> | I mean in the thread doing the atomically |
| 04:13:07 | × | Alleria quits (~JohnGalt@user/alleria) (Read error: Connection reset by peer) |
| 04:13:20 | <EvanR> | oh ok, well you didn't cause an error within the atomically |
| 04:14:25 | <tabemann> | I just confirmed that GHC has magic that prevents intermediate read values from escaping even if no writes are applied out to the target TVar |
| 04:14:44 | <tabemann> | probably in the form of something like an update clock or like |
| 04:15:18 | <EvanR> | no, it just doesn't commit any changes when transactions fail |
| 04:16:00 | <tabemann> | that's what I was trying to disprove |
| 04:16:19 | <tabemann> | that's what I mean by a "naive" approach |
| 04:16:33 | <EvanR> | the naive approach to STM is to just write to memory normally? xD |
| 04:16:49 | <EvanR> | and hope no other threads actually run |
| 04:17:23 | <tabemann> | no, a naive approach to STM is to just ensure that no writes conflict with one another, and no exceptions occur within atomically blocks |
| 04:17:48 | <monochrom> | Don't hope. Enforce. Run the threads with sequential time sharing. |
| 04:18:24 | <EvanR> | it's true that SQL servers come with modes that don't enforce transaction semantics, maybe this is why you're confused |
| 04:18:25 | <monochrom> | This is why a select/poll/event loop does not have to worry about this. >:) |
| 04:19:17 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 268 seconds) |
| 04:19:17 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 04:19:39 | <EvanR> | but transaction is supposed to mean any sequence of writes AND reads are consistent within the transaction, as well as only seeing the final state of previous commits |
| 04:20:02 | <tabemann> | EvanR: and that's what I've confirmed here |
| 04:20:03 | → | Alleria joins (~JohnGalt@user/alleria) |
| 04:20:19 | <tabemann> | monochrom: of course there's always Erlang's approach |
| 04:20:20 | <EvanR> | just to clarify, you say clojure is busted? |
| 04:20:45 | <EvanR> | or only busted when they do side effects |
| 04:20:50 | <tabemann> | EvanR: nah, not Clojure, just the millions of STM frameworks which I highly suspect are crap |
| 04:21:05 | <monochrom> | Clojure can't be busted. It lacks one of retry or orElse, I forgot which. |
| 04:21:24 | → | rosco joins (~rosco@175.136.158.171) |
| 04:21:33 | <tabemann> | because they have no means of preventing side effects from within transactions |
| 04:21:46 | <monochrom> | I.e., you can't make more mistakes if you simply omit important features! >:) |
| 04:22:23 | <EvanR> | technically haskell also lets you do non-transactional effects within the transaction |
| 04:22:37 | <tabemann> | EvanR: i.e. unsafePerformIO |
| 04:23:01 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 04:23:05 | <tabemann> | but unsafePerformIO means that you've decided to press the button anyways |
| 04:23:28 | <tabemann> | after that point all bets are off |
| 04:23:29 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 04:24:16 | <EvanR> | I thought that was actually disallowed in stm |
| 04:24:35 | <EvanR> | there's this thing unsafeIOToSTM |
| 04:25:06 | <monochrom> | Yeah you need also that. unsafePerformIO alone is not enough, you don't even have IO inside STM, formally. |
| 04:25:07 | <EvanR> | anyway it comes down to culture again |
| 04:25:10 | <tabemann> | that's when you launch a nuclear strike on your own position to kill all the zombies |
| 04:26:01 | <[Leary]> | atomically-in-atomically is disallowed by the RTS. I don't think it takes issue with just `unsafePerformIO`, though? |
| 04:26:09 | <EvanR> | oh ok |
| 04:26:30 | <EvanR> | it was either atomically inside unsafePerformIO or the other way around that was failing |
| 04:26:48 | <tabemann> | I thought it was atomically within unsafePerformIO that was verboten |
| 04:27:10 | <EvanR> | that direction makes less sense |
| 04:27:32 | <EvanR> | maybe it was transitive nesting of atomically |
| 04:29:34 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 260 seconds) |
| 04:31:02 | <[Leary]> | % atomically (pure $! unsafePerformIO (atomically (pure 0))) |
| 04:31:03 | <yahb2> | *** Exception: Control.Concurrent.STM.atomically was nested |
| 04:32:03 | × | rosco quits (~rosco@175.136.158.171) (Quit: Lost terminal) |
| 04:32:28 | <EvanR> | oh sure, yahb has STM but not forkIO and threadDelay |
| 04:32:37 | <EvanR> | and uPIO |
| 04:32:51 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 04:32:53 | <[Leary]> | I imported them in PM. |
| 04:40:20 | → | rosco joins (~rosco@175.136.158.171) |
| 04:43:36 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 04:44:39 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 04:50:43 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 255 seconds) |
| 04:53:22 | → | aforemny joins (~aforemny@i59F516F2.versanet.de) |
| 04:53:29 | × | aforemny_ quits (~aforemny@i59F516E0.versanet.de) (Ping timeout: 252 seconds) |
| 05:02:13 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 05:02:52 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 05:04:08 | × | Guest3 quits (~Guest3@149.159.194.55) (Ping timeout: 250 seconds) |
| 05:08:23 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 05:14:23 | × | Square2 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 05:19:51 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 05:25:53 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 05:27:57 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 05:33:54 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 05:45:55 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 05:51:11 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 245 seconds) |
| 06:03:20 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 06:07:26 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 06:07:51 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 06:08:25 | → | euleritian joins (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) |
| 06:09:13 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 256 seconds) |
| 06:13:20 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:13:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:17:14 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 06:17:14 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 06:17:14 | finn_elija | is now known as FinnElija |
| 06:18:10 | × | euleritian quits (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:18:28 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:19:49 | × | Alleria quits (~JohnGalt@user/alleria) (Read error: Connection reset by peer) |
| 06:20:20 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 06:22:18 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 06:25:16 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:25:57 | → | Alleria joins (~JohnGalt@user/alleria) |
| 06:26:07 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 06:26:26 | → | euleritian joins (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) |
| 06:26:34 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 255 seconds) |
| 06:28:31 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 06:34:20 | → | johnw joins (~johnw@69.62.242.138) |
| 06:34:38 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 260 seconds) |
| 06:35:28 | → | chomwitt joins (~chomwitt@2a02:587:7a10:2a00:1ac0:4dff:fedb:a3f1) |
| 06:37:39 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 06:38:26 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 06:39:01 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 06:46:29 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 06:48:27 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 256 seconds) |
| 06:52:47 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 06:53:19 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 06:53:19 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 06:53:47 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 06:59:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:00:40 | × | komikat quits (~akshitkr@218.185.248.66) (Ping timeout: 255 seconds) |
| 07:03:27 | → | acidjnk joins (~acidjnk@p200300d6e72b9352dcea2d781ea8e5a4.dip0.t-ipconnect.de) |
| 07:04:12 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 07:07:11 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 07:10:07 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 255 seconds) |
| 07:13:57 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 256 seconds) |
| 07:14:20 | → | harveypwca joins (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) |
| 07:15:24 | → | kenran joins (~user@user/kenran) |
| 07:17:01 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 07:19:52 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 4.1.1) |
| 07:21:57 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 07:22:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:23:23 | × | rosco quits (~rosco@175.136.158.171) (Read error: Connection reset by peer) |
| 07:24:22 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:25:34 | → | rosco joins (~rosco@175.136.158.171) |
| 07:25:39 | × | rosco quits (~rosco@175.136.158.171) (Client Quit) |
| 07:25:50 | → | rosco joins (~rosco@175.136.158.171) |
| 07:28:02 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:28:11 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 07:29:53 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 07:30:03 | × | pr0ton quits (~pr0ton@176.254.244.83) (Ping timeout: 261 seconds) |
| 07:30:24 | <srk> | dminuoso_: considered transitioning to dhall and dhall-to-nix? |
| 07:35:45 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 252 seconds) |
| 07:36:21 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 07:42:25 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 07:43:20 | → | Umeaboy joins (~Umeaboy@94-255-145-133.cust.bredband2.com) |
| 07:43:24 | <Umeaboy> | Hi! |
| 07:44:20 | <Umeaboy> | Why is there no support for glibc 2.36 in the cabal-install rpm? I see 2.33, 2.34 and 2.38. |
| 07:44:49 | <Umeaboy> | I ran rpm -qpR cabal-install-3.8.1.0-2.fc40.x86_64.rpm to check. |
| 07:45:19 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 07:45:19 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 07:45:19 | finn_elija | is now known as FinnElija |
| 07:47:32 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 07:47:55 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 255 seconds) |
| 07:52:35 | × | euleritian quits (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:53:04 | → | euleritian joins (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) |
| 07:53:07 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 07:53:21 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 252 seconds) |
| 07:53:22 | × | euleritian quits (~euleritia@dynamic-046-114-169-147.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:53:39 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:58:40 | → | Alatheia joins (~Alatheia@176.254.244.83) |
| 08:01:24 | → | gmg joins (~user@user/gehmehgeh) |
| 08:03:43 | → | cfricke joins (~cfricke@user/cfricke) |
| 08:05:12 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 08:07:01 | → | alp_ joins (~alp@2001:861:e3d6:8f80:ba78:18cf:70dd:23bc) |
| 08:11:06 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 256 seconds) |
| 08:11:16 | <sclv> | you will have to ask the debian or whatever maintainers. |
| 08:11:25 | <sclv> | ie its a distro question |
| 08:13:27 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 08:15:35 | → | kenran` joins (~user@user/kenran) |
| 08:16:12 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 08:17:23 | × | kenran quits (~user@user/kenran) (Ping timeout: 264 seconds) |
| 08:20:53 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 08:22:24 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 08:28:16 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 245 seconds) |
| 08:31:09 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 08:35:04 | → | Jackneill joins (~Jackneill@20014C4E1E0B5A0069081ECE081E635B.dsl.pool.telekom.hu) |
| 08:36:53 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:37:22 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 268 seconds) |
| 08:44:49 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 08:57:19 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 260 seconds) |
| 08:58:16 | × | tzh_ quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 08:58:51 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:59:55 | × | lbseale quits (~quassel@user/ep1ctetus) (Ping timeout: 256 seconds) |
| 09:02:04 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 09:02:09 | × | mikess quits (~sam@user/mikess) (Read error: Connection reset by peer) |
| 09:06:20 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) (Remote host closed the connection) |
| 09:06:30 | → | komikat joins (~akshitkr@218.185.248.66) |
| 09:09:35 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 09:11:02 | → | CiaoSen joins (~Jura@2a05:5800:28a:6100:2a3a:4dff:fe84:dbd5) |
| 09:15:35 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
| 09:24:31 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Remote host closed the connection) |
| 09:24:32 | × | jrm quits (~jrm@user/jrm) (Ping timeout: 268 seconds) |
| 09:24:44 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 09:24:59 | → | jrm joins (~jrm@user/jrm) |
| 09:26:09 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 09:26:27 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 09:27:02 | → | danza joins (~francesco@151.43.234.166) |
| 09:28:52 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:30:42 | × | harveypwca quits (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) (Quit: Leaving) |
| 09:31:01 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 09:31:58 | × | danza quits (~francesco@151.43.234.166) (Ping timeout: 255 seconds) |
| 09:41:48 | × | manwithluck quits (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 268 seconds) |
| 09:42:02 | → | manwithluck joins (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 09:43:54 | → | danse-nr3 joins (~danse@151.43.234.166) |
| 09:43:57 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) |
| 09:47:57 | × | alp_ quits (~alp@2001:861:e3d6:8f80:ba78:18cf:70dd:23bc) (Remote host closed the connection) |
| 09:48:14 | → | alp_ joins (~alp@2001:861:e3d6:8f80:455d:a197:398e:7c06) |
| 09:49:26 | <dminuoso_> | Servant question: Say Im making a typeclass class HasSummary api where toSummary :: Proxy api -> String; instance forall sym ty. KnownSymbol sym => HasSummary (Summary sym :> ty) where toSummary _ = symbolVal (Proxy :: Proxy sym) |
| 09:49:53 | <dminuoso_> | And I hold a generic endpoint record selector in my hand, Im a bit confused how to apply toSummary to that endpoint record selector. |
| 09:56:31 | × | rosco quits (~rosco@175.136.158.171) (Quit: Lost terminal) |
| 09:57:26 | × | manwithluck quits (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 245 seconds) |
| 09:58:38 | → | manwithluck joins (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 09:58:52 | × | CiaoSen quits (~Jura@2a05:5800:28a:6100:2a3a:4dff:fe84:dbd5) (Ping timeout: 246 seconds) |
| 09:59:00 | → | __monty__ joins (~toonn@user/toonn) |
| 10:00:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:01:29 | → | CiaoSen joins (~Jura@5.83.179.237) |
| 10:03:38 | × | danse-nr3 quits (~danse@151.43.234.166) (Read error: Connection reset by peer) |
| 10:03:57 | → | danse-nr3 joins (~danse@151.57.228.14) |
| 10:04:50 | <kuribas> | Welcome to the nastiness that is the Servant implementation. |
| 10:10:06 | → | chele joins (~chele@user/chele) |
| 10:11:10 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:12:35 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |
| 10:13:25 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 10:14:08 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:23:42 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds) |
| 10:34:28 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 10:34:32 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 10:36:04 | hamess_ | is now known as hamess |
| 10:38:14 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 10:38:20 | × | shapr quits (~user@2600:1700:c640:3100:c355:fe3e:4f9f:d5b6) (Remote host closed the connection) |
| 10:38:34 | → | shapr joins (~user@2600:1700:c640:3100:af48:8802:e8a5:3ea1) |
| 10:48:48 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 10:50:10 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 255 seconds) |
| 10:57:56 | × | Philonous quits (~Philonous@user/philonous) (Quit: ZNC - https://znc.in) |
| 10:58:21 | → | Philonous joins (~Philonous@user/philonous) |
| 10:58:44 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 11:04:45 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Ping timeout: 252 seconds) |
| 11:04:49 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 11:06:22 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 11:06:42 | × | shOkEy quits (~shOkEy@178-164-206-123.pool.digikabel.hu) (Ping timeout: 260 seconds) |
| 11:08:32 | → | shOkEy joins (~shOkEy@91-83-3-30.pool.digikabel.hu) |
| 11:12:24 | → | xff0x joins (~xff0x@2405:6580:b080:900:9a48:ce0:12d3:d0ae) |
| 11:14:09 | → | not_reserved joins (~not_reser@45.144.113.234) |
| 11:25:02 | <danse-nr3> | morning all. I think one needs dependent types to get type safety with matrices, do you have a solution you like in a non-dependent haskell library? |
| 11:27:15 | <danse-nr3> | i know it sounds like a contradiction, but i am not sure about the first statement and i am curious about other compromises |
| 11:30:55 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 11:31:45 | → | gmg joins (~user@user/gehmehgeh) |
| 11:35:32 | <lortabac> | dependent types are needed when you have terms whose type is determined at runtime |
| 11:35:57 | <lortabac> | so for example if the size of the matrix is known statically there is no need for dependent types |
| 11:37:00 | <danse-nr3> | i see, i have a wrong understanding of dependent types then. Any matrix typing you find elegant or nice to work with? |
| 11:38:25 | ← | arahael parts (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) () |
| 11:38:49 | <danse-nr3> | (i am surprised that lists with encoded length are not more common then, at least i never stumble upon them) |
| 11:39:01 | <lortabac> | if the size of the matrix is only known at runtime, then you need some way to reason generically over any size, and that's where dependent types become useful |
| 11:39:54 | <danse-nr3> | right, but usually the size is known in function signatures (add one to rows, transpose etcetera) |
| 11:40:15 | → | chele joins (~chele@user/chele) |
| 11:40:35 | <lortabac> | I've never worked with matrixes in Haskell, but I suppose there are libraries that do what you are looking for |
| 11:42:15 | → | rosco joins (~rosco@175.136.158.171) |
| 11:42:50 | <danse-nr3> | yes i think i saw some years ago, maybe repa or some custom types for some neural network lib, i don't recall now. I guess a type like `a n -> a (n+1)` cannot be written in vanilla haskell and it requires some extension? |
| 11:44:49 | × | CiaoSen quits (~Jura@5.83.179.237) (Ping timeout: 256 seconds) |
| 11:45:07 | <lortabac> | yes you need TypeFamilies, TypeOperators and maybe more |
| 11:45:17 | <danse-nr3> | cheers lortabac |
| 11:47:50 | <lortabac> | danse-nr3: imagine you want a function 'generateMatrix' that fills a matrix of size NxM with a given value |
| 11:48:15 | <lortabac> | generateMatrix :: Int -> Int -> Matrix n m |
| 11:48:21 | <danse-nr3> | is that where dependent types come in the picture? |
| 11:48:35 | <danse-nr3> | i guess one could have an `n` encoding for ints |
| 11:48:38 | <lortabac> | you need a way to tell the type system that the first Int should be 'n' and the second one should be 'm' |
| 11:48:48 | <lortabac> | but in Haskell you can't |
| 11:49:13 | → | akegalj joins (~akegalj@78-2-198-3.adsl.net.t-com.hr) |
| 11:49:30 | <danse-nr3> | that would be a very long haskell file though, probably unfeasible |
| 11:49:49 | <lortabac> | in a dependently-typed language it would be something like 'generateMatrix : (n : Nat) -> (m : Nat) -> Matrix n m |
| 11:50:06 | <danse-nr3> | yeah makes more sense like this |
| 11:52:11 | <lortabac> | where the type of the first argument is 'Nat' and 'n' is a name that refers to its value |
| 11:54:36 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 11:58:58 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 12:00:01 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 12:00:50 | <bwe> | think of hlint noting those spots in my code that make it probably very slow. is there a tool that does just that? instead of mapM use forM... or is there just a checklist of how to optimise my haskell code "instead ... use" |
| 12:00:58 | <lortabac> | oops the signature should be 'generateMatrix : (n : Nat) -> (m : Nat) -> a -> Matrix n m a' |
| 12:01:05 | <lortabac> | but you got the idea |
| 12:02:15 | <danse-nr3> | yes that syntax is clear |
| 12:02:39 | <bwe> | I know it's very basic but such a kind of list of rules of thumb would make all the difference for me. |
| 12:02:39 | <danse-nr3> | performance is more a matter of semantics bwe, i don't think linting goes that far |
| 12:04:05 | <bwe> | danse-nr3: so, if I'd ask you, which examples of instead … do … can you recall from your very experience? |
| 12:04:48 | <danse-nr3> | the different fold functions, i guess, but nothing to be automated, requires reasoning and understanding |
| 12:05:31 | <bwe> | danse-nr3: so along the lines of avoid iterating by putting everything into memory before giving it to the next function? |
| 12:06:34 | <danse-nr3> | well the considerations explained in wiki.haskell.org/Foldr_Foldl_Foldl' |
| 12:09:10 | <bwe> | so, great, I could find all those spots in my code and choose wisely. that implies mapM for example. Other than the intricacies of the different folds, what should I look at? |
| 12:10:48 | <bwe> | (also, how can I tell which function eventually calls a fold? is it possible to get that answer automated? I assume naïvely that this could be done because the execution does it anyways; but just a naïve approach) |
| 12:11:48 | → | kenran`` joins (~user@user/kenran) |
| 12:12:58 | × | danse-nr3 quits (~danse@151.57.228.14) (Remote host closed the connection) |
| 12:13:13 | × | Jackneill quits (~Jackneill@20014C4E1E0B5A0069081ECE081E635B.dsl.pool.telekom.hu) (Ping timeout: 276 seconds) |
| 12:13:16 | × | kenran` quits (~user@user/kenran) (Ping timeout: 245 seconds) |
| 12:13:22 | → | danse-nr3 joins (~danse@151.57.228.14) |
| 12:14:56 | → | tremon joins (~tremon@83.80.159.219) |
| 12:15:23 | → | kenran``` joins (~user@user/kenran) |
| 12:16:13 | <ski> | "you need a way to tell the type system that the first Int should be 'n' and the second one should be 'm'","but in Haskell you can't" -- you can do existentials |
| 12:17:31 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 12:17:59 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 12:17:59 | × | kenran`` quits (~user@user/kenran) (Ping timeout: 264 seconds) |
| 12:18:22 | × | danse-nr3 quits (~danse@151.57.228.14) (Ping timeout: 255 seconds) |
| 12:18:24 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 12:18:51 | → | gmg joins (~user@user/gehmehgeh) |
| 12:18:53 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 12:22:46 | kenran``` | is now known as kenran |
| 12:22:47 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
| 12:24:03 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 12:27:11 | <komikat> | b |
| 12:27:43 | <komikat> | been working with pytorch for sometime, is there any library to do deep learning with in #haskell |
| 12:28:30 | <komikat> | i've been meaning to write a dependency parser for natural languages and wanted to see if i could get that to work with a functional programming language |
| 12:37:42 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 12:42:27 | × | not_reserved quits (~not_reser@45.144.113.234) (Quit: Client closed) |
| 12:44:24 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 12:44:25 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 276 seconds) |
| 12:50:28 | × | remedan quits (~remedan@ip-94-112-0-18.bb.vodafone.cz) (Ping timeout: 256 seconds) |
| 12:51:20 | × | rosco quits (~rosco@175.136.158.171) (Quit: Lost terminal) |
| 12:52:51 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 12:52:57 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 12:53:01 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Quit: Konversation terminated!) |
| 12:55:44 | → | remedan joins (~remedan@ip-94-112-0-18.bb.vodafone.cz) |
| 12:56:27 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 13:02:36 | <bwe> | btw what is the go-to language if I'd seek something like Gofer or Hugs? |
| 13:02:57 | <bwe> | sort of Haskell for educational purposes |
| 13:08:53 | <haskellbridge> | 14<mauke> Isn't hugs just a Haskell interpreter? |
| 13:11:59 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 13:20:56 | → | edr joins (~edr@user/edr) |
| 13:26:24 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 13:30:31 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 13:33:20 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 13:34:07 | → | rosco joins (~rosco@175.136.158.171) |
| 13:34:30 | × | kimiamania46 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 13:34:50 | → | kimiamania46 joins (~65804703@user/kimiamania) |
| 13:38:07 | → | danse-nr3 joins (~danse@151.57.228.14) |
| 13:39:02 | → | CiaoSen joins (~Jura@2a05:5800:28a:6100:2a3a:4dff:fe84:dbd5) |
| 13:40:22 | × | kimiamania46 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 13:40:54 | × | danse-nr3 quits (~danse@151.57.228.14) (Remote host closed the connection) |
| 13:41:18 | → | danse-nr3 joins (~danse@151.57.228.14) |
| 13:42:47 | <danse-nr3> | how would you express that with existentials ski? |
| 13:43:07 | → | kimiamania46 joins (~65804703@user/kimiamania) |
| 13:43:40 | × | akegalj quits (~akegalj@78-2-198-3.adsl.net.t-com.hr) (Quit: leaving) |
| 13:47:59 | <danse-nr3> | not any popular one i am afraid komikat |
| 13:53:53 | × | kimiamania46 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 13:59:05 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 14:01:11 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 14:02:10 | → | kimiamania46 joins (~65804703@user/kimiamania) |
| 14:02:39 | × | Alleria quits (~JohnGalt@user/alleria) (Ping timeout: 268 seconds) |
| 14:03:50 | → | Alleria joins (~JohnGalt@user/alleria) |
| 14:04:58 | × | danse-nr3 quits (~danse@151.57.228.14) (Read error: Connection reset by peer) |
| 14:05:27 | → | danse-nr3 joins (~danse@151.35.247.219) |
| 14:07:59 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:16:01 | → | swamps joins (~swamps@static-a197.Irkutsk.golden.ru) |
| 14:16:57 | × | swamps quits (~swamps@static-a197.Irkutsk.golden.ru) (Client Quit) |
| 14:17:36 | → | swamps joins (~swamps@static-a197.Irkutsk.golden.ru) |
| 14:18:18 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 14:19:16 | × | rosco quits (~rosco@175.136.158.171) (Quit: Lost terminal) |
| 14:19:47 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 14:20:34 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 14:27:00 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 14:32:13 | × | danse-nr3 quits (~danse@151.35.247.219) (Ping timeout: 246 seconds) |
| 14:32:43 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 14:33:05 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 14:36:49 | → | danse-nr3 joins (~danse@151.35.247.219) |
| 14:39:48 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Quit: Konversation terminated!) |
| 14:43:56 | <komikat> | :( |
| 14:47:42 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 14:49:14 | <trev> | bwe: you could try idris |
| 14:49:58 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:50:07 | <danse-nr3> | komikat, you could try julia XD |
| 14:50:30 | <komikat> | does julia have types? |
| 14:50:48 | <komikat> | as in strong typing |
| 14:51:10 | <danse-nr3> | i think it does yes |
| 14:51:10 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 256 seconds) |
| 14:51:37 | <komikat> | interesting |
| 14:53:54 | → | seeg123456 joins (~seeg12345@64.176.64.83) |
| 14:55:01 | × | shapr quits (~user@2600:1700:c640:3100:af48:8802:e8a5:3ea1) (Remote host closed the connection) |
| 14:55:14 | → | shapr joins (~user@2600:1700:c640:3100:a007:14d5:426f:261d) |
| 14:58:57 | <komikat> | damn "Julia's type system is dynamic, but gains some of the advantages of static type systems by making it possible to indicate that certain values are of specific types" |
| 15:00:09 | <danse-nr3> | yeah, looking at it again, i am not sure the types satisfy your requirements docs.julialang.org/en/v1/manual/types. Also not sure that the language is that functionaly ... someone mentioned julia to me some time ago relating it to haskell, but i am not seeing the connection right now |
| 15:00:26 | <danse-nr3> | *functional |
| 15:02:16 | <danse-nr3> | i was also told that R is quite functional but i don't know it, and it is "dynamically typed" |
| 15:03:05 | <komikat> | ah yeah |
| 15:03:28 | <komikat> | it doesn't seem *purely* functional but at least it doesn't have objects xD like python |
| 15:10:38 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Remote host closed the connection) |
| 15:10:59 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 15:16:00 | → | ivelten joins (~ivelten@2804:82b8:8:ee01:fda6:516:611b:3176) |
| 15:22:01 | × | mrmr15533 quits (~mrmr@user/mrmr) (Ping timeout: 245 seconds) |
| 15:22:12 | → | mrmr155331 joins (~mrmr@user/mrmr) |
| 15:24:47 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:25:18 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:29:42 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 15:30:18 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:31:56 | <ski> | danse-nr3 : `generateMatrix :: Int -> Int -> a -> exists m n. Matrix n m a' |
| 15:32:56 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:33:02 | <ncf> | that doesn't really express that m and n come from the first two arguments |
| 15:33:25 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 276 seconds) |
| 15:33:35 | <ski> | (btw, note that this is weaker than `generateMatrix : (n : Nat) -> (m : Nat) -> a -> Matrix n m a'. basically same thing as `(exists a. P a) -> (exists a. Q a)' being weaker than `forall a. P a -> Q a'. so, it's weaker because it doesn't link the two size arguments, to the corresponding parameters to the return type) |
| 15:33:44 | → | ystael_ joins (~ystael@user/ystael) |
| 15:33:44 | <ski> | right |
| 15:33:59 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 15:34:21 | ystael_ | is now known as ystael |
| 15:34:47 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 15:35:14 | <ski> | it could still be used, to express that there will be *some* sizes for the resulting matrix. while `generateMatrix :: Int -> Int -> a -> Matrix n m' would be incorrect, as that's saying as the sizes of the resulting matrix will be whatever the caller wants them to be (unrelated to the two size arguments) |
| 15:35:54 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 15:35:57 | <danse-nr3> | interesting, thanks |
| 15:37:13 | <ski> | anyway, the `exists' is obviously pseudo-Haskell. you can encode it in two different ways in Haskell. (a) using `ExistentialQuantification' (imho a misnomer, `ExistentialConstructors' would be better); or (b) using CPS with `Rank2Types' |
| 15:38:21 | <danse-nr3> | i agree that sounds like a misnomer |
| 15:38:44 | <ski> | (a) would be `generateMatrix :: Int -> Int -> a -> SomeMatrix a' where `data SomeMatrix a = forall n m. WrapMatrix (Matrix n m a)' (or `data SomeMatrix :: * -> * where WrapMatrix :: Matrix n m a -> SomeMatrix a', using `GADTSyntax') |
| 15:39:27 | <ski> | (b) would be `withGeneratedMatrix :: Int -> Int -> a -> (forall n m. Matrix n m a -> o) -> o' |
| 15:40:36 | <danse-nr3> | meh, with `exists` it looked way more readable, but maybe this is not such a common use case |
| 15:40:44 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.0.5) |
| 15:41:14 | <ski> | yes. that's why i presented it with that pseudo-Haskell syntax first, becauses it's easier to reason about and think about it, in that form |
| 15:42:28 | <ski> | ((a) tends to be better, when you're going to store the result in data-structures. while (b) tends to be better when you're going to use the result directly after the call) |
| 15:43:16 | <ski> | perhaps in some future, we could get actual `exists' syntax .. |
| 15:43:30 | <lortabac> | ski: unless I misunderstood something, this doesn't solve the problem I was talking about |
| 15:43:38 | <ski> | (Mercury has real existential quantification, like that) |
| 15:43:47 | <danse-nr3> | yeah that would be nice |
| 15:43:55 | <danse-nr3> | no it is not the same lortabac but somehow close |
| 15:43:58 | <ski> | it does not solve the problem of connecting the size arguments to the type of the result, no |
| 15:44:07 | <lortabac> | I want the matrix to have size NxM where N and M are the values of the first 2 arguments |
| 15:44:12 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:44:15 | <ski> | well, you do get that |
| 15:44:21 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 15:44:27 | <ski> | it's just that you don't statically (in the types) know that that's what you get |
| 15:44:31 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:45:09 | <lortabac> | yes, my point was that with dependent types you can encode this piece of information in the types |
| 15:45:18 | <ski> | right |
| 15:45:50 | <lortabac> | (and also that if you don't have a similar use case you don't need full dependent types) |
| 15:46:11 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 245 seconds) |
| 15:46:46 | × | ivelten quits (~ivelten@2804:82b8:8:ee01:fda6:516:611b:3176) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 15:46:59 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:47:26 | <ski> | you could try something like `generateMatrix :: (KnownNat n,KnownNat m) => p m -> q n -> a -> Matrix n m a' |
| 15:48:58 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds) |
| 15:49:00 | → | vishnix joins (~vishwas@c-73-9-42-9.hsd1.il.comcast.net) |
| 15:49:16 | <ski> | (or, rolling your own singletons, `data Nat = Zero | Succ Nat; data IsNat :: Nat -> * where ZeroS :: IsNat Zero; SuccS :: IsNat n -> IsNat (Succ n)', then `generateMatrix :: IsNat n -> IsNat m -> a -> Matrix n m a') |
| 15:49:30 | × | vishnix quits (~vishwas@c-73-9-42-9.hsd1.il.comcast.net) (Client Quit) |
| 15:49:36 | <lortabac> | I don't think the solution with proxies would be usable if M and N are only known at runtime, for example fetched from a database |
| 15:49:38 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 15:49:40 | → | vishnix joins (~vishwas@c-73-9-42-9.hsd1.il.comcast.net) |
| 15:49:41 | → | ivelten joins (~ivelten@2804:82b8:8:ee01:fda6:516:611b:3176) |
| 15:53:06 | <ski> | (the `KnowNat' constraints would be carrying the run-time info. you could then use `natVal :: KnownNat n => proxy n -> Natural', or perhaps `natSing :: KnownNat n => SNat n') |
| 15:53:45 | <c_wraith> | You can use types that are only known at runtime |
| 15:53:47 | <ski> | (the operation that gets the `m' and `n' from the database would use existentials (in either encoding above) |
| 15:53:50 | <ski> | ) |
| 15:54:07 | <lortabac> | I don't think you can fully solve this problem without singletons |
| 15:54:26 | <lortabac> | with the other solutions somewhere you lose information in the types |
| 15:54:32 | <ski> | getDBNat :: ... -> IO (exists n. KnownNat n *> Const n ()) |
| 15:55:23 | <ski> | (with (b), that becomes `with DBNat :: ... -> (forall n. KnownNat n => IO o) -> IO o') |
| 15:57:41 | <lortabac> | if you use existentials, how do you pass the generated matrix to other functions and preserve the sizes in the types? |
| 15:57:56 | <c_wraith> | bizarrely enough, you just do |
| 15:58:32 | <lortabac> | I don't think that is possible without singletons |
| 15:58:41 | <c_wraith> | You have the KnownNat constraint available |
| 15:58:49 | <c_wraith> | you can always lower it to a value when needed |
| 15:59:14 | <c_wraith> | (as long as you are passing the constraint around) |
| 15:59:37 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 15:59:41 | <lortabac> | I'm not sure I follow |
| 15:59:58 | <lortabac> | (forall n. KnownNat n => IO o) the 'n' is lost here |
| 16:00:09 | <c_wraith> | No it's not. |
| 16:00:19 | <c_wraith> | it's right there in the type |
| 16:00:21 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 16:00:50 | <lortabac> | ok let's recapitulate |
| 16:01:17 | <c_wraith> | But you *do* need to use other extensions that allow you to use that formulation usefully |
| 16:01:26 | × | alp_ quits (~alp@2001:861:e3d6:8f80:455d:a197:398e:7c06) (Ping timeout: 256 seconds) |
| 16:01:49 | <c_wraith> | Otherwise you'd end up needing a type more like (forall n. KnownNat n => proxy n -> IO o) |
| 16:02:09 | <lortabac> | I want to fetch M and N from the database, create a (Matrix m n Int) and pass it to a function that expects a matrix, keeping the size information in the types |
| 16:02:31 | <lortabac> | all this without singletons |
| 16:03:32 | <c_wraith> | have you read through GHC.TypeLits? |
| 16:04:19 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 16:04:38 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:04:44 | <lortabac> | oh |
| 16:04:54 | <lortabac> | I wasn't aware that SNat is now in base |
| 16:05:02 | <c_wraith> | you don't even need it |
| 16:05:08 | <c_wraith> | you'd just call someNatVal twice |
| 16:05:16 | <c_wraith> | pattern match on the results, and go |
| 16:06:55 | <lortabac> | interesting |
| 16:07:48 | <c_wraith> | You do lose something over having literals in your types - you can't trivially generate new constraints like (0 < n) => ... |
| 16:08:12 | <c_wraith> | When all you have is KnownNat, that's the only constraint you get. |
| 16:08:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:13:08 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 16:13:43 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 16:14:40 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 16:16:02 | → | alp_ joins (~alp@2001:861:e3d6:8f80:882f:ff0d:da80:ca07) |
| 16:16:04 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:16:21 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:16:46 | kaol_ | is now known as kaol |
| 16:18:18 | <lortabac> | c_wraith: I'm trying to write a minimal example without success |
| 16:18:23 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 256 seconds) |
| 16:19:12 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 16:19:42 | <lortabac> | this naive version doesn't compile https://paste.tomsmeding.com/DRwgbFdT |
| 16:20:37 | <lortabac> | ah wait, I think I understand |
| 16:20:49 | <c_wraith> | Oh. That's because KnownNat n doesn't imply KnownNat (n-1) |
| 16:22:49 | <c_wraith> | Though you're also going to need ScopeTypeVariables to talk about n (the type) in the function body like that |
| 16:22:56 | <c_wraith> | *ScopedTypeVariables |
| 16:23:00 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:23:05 | <lortabac> | no, I'm lost |
| 16:23:09 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 16:23:09 | <ski> | the `Nat' `n' in the pattern in `n -> x :< generate (Proxy :: Proxy (n - 1)) x' is also unrelated to the `Nat' `n - 1' in the expressio there |
| 16:23:21 | <c_wraith> | yes, that's why you need ScopedTypeVariables |
| 16:23:24 | <ski> | yes |
| 16:23:26 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:23:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:23:52 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 16:23:59 | <ski> | you need to replace the pattern `pn' with `(pn :: p n)' |
| 16:24:40 | <ski> | or, i suppose, just add `forall p n a. ' to the signature |
| 16:24:59 | <lortabac> | I tried but it still doesn't compile |
| 16:25:22 | <lortabac> | Couldn't match type ‘n’ with ‘0’ |
| 16:25:55 | <lortabac> | anyway I have to go now, I'll try again tomorrow |
| 16:26:00 | <ski> | just matching on `n' will probably not be enough, yea |
| 16:26:07 | <lortabac> | you made me curious :) |
| 16:26:31 | <danse-nr3> | bye lortabac o/ |
| 16:26:52 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 16:27:12 | <c_wraith> | Honestly, that's like the single worst case for Nat, the way GHC works |
| 16:27:29 | <c_wraith> | (yes, I know lortabac is gone) |
| 16:27:44 | <ski> | i suspect they'll need to use `natSing', rather than `natVal', there |
| 16:28:45 | <c_wraith> | I don't think it matters. That definition of generate requires recursive generation of NatVal constraints |
| 16:29:04 | <c_wraith> | GHC makes that painful |
| 16:29:33 | <ski> | (s/NatVal/KnownNat/) |
| 16:29:34 | <ski> | yea |
| 16:29:37 | <c_wraith> | err, yes |
| 16:29:46 | → | harveypwca joins (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) |
| 16:30:15 | <c_wraith> | Amusingly, last time I looked through GHC typechecking plugins, I recall seeing one specifically intended for this purpose |
| 16:30:32 | <ski> | it says |
| 16:30:33 | → | bgamari_ joins (~bgamari@64.223.175.94) |
| 16:30:38 | → | phma_ joins (phma@2001:5b0:210d:4b88:3e7a:d751:236f:1da4) |
| 16:30:40 | <ski> | class KnownNat (n :: Nat) where |
| 16:30:44 | <ski> | GHC.TypeNats.natSing :: GHC.TypeNats.SNat n |
| 16:30:48 | <ski> | but i get nothing for `:i SNat' |
| 16:31:12 | <c_wraith> | are you on a GHC that uses base 4.19? |
| 16:31:24 | <ski> | hm, this was 8.8.4 |
| 16:31:37 | <c_wraith> | Oh, I guess 4.18 is sufficient |
| 16:32:20 | <ski> | if it had something like `data SNat :: Nat -> * where ZeroS :: SNat 0; SuccS :: KnownNat n => SNat n -> SNat (1 + n)', then matching on the `SNat n' would help |
| 16:32:20 | <c_wraith> | but 4.18 means GHC 9.6+ |
| 16:32:33 | × | bgamari quits (~bgamari@64.223.173.10) (Ping timeout: 256 seconds) |
| 16:33:10 | × | phma quits (~phma@host-67-44-208-32.hnremote.net) (Ping timeout: 256 seconds) |
| 16:34:03 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 16:35:39 | <c_wraith> | Hmm. This probably does get a lot easier if you use SNat, but you can probably get away with only doing that internally. |
| 16:36:26 | × | mrvdb- quits (~mrvdb@2001:19f0:5000:8582:5400:ff:fe07:3df5) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:36:28 | <c_wraith> | Oh, I see. You can also use sameNat |
| 16:36:57 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 16:36:58 | <ski> | hm, right |
| 16:37:17 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 16:37:48 | <c_wraith> | But yes, this stuff is painful. there's a reason I see it called "hasochism" |
| 16:38:59 | <danse-nr3> | well we were looking for ways to do the thing without the thing (dependent types), so no surprise if it results hacky |
| 16:40:44 | → | mrvdb joins (~mrvdb@185.92.221.186) |
| 16:40:50 | <danse-nr3> | although the lack of `exists` seems to have marked some significant increase in complexity... but maybe that is just my impression because i lost track of the problem afterwards |
| 16:41:02 | → | mikess joins (~sam@user/mikess) |
| 16:43:21 | <c_wraith> | It does add complexity, but it's purely mechanical complexity |
| 16:44:00 | <c_wraith> | the workarounds are known and don't require creativity |
| 16:45:11 | phma_ | is now known as phma |
| 17:01:47 | → | mmhat joins (~mmh@p200300f1c71a22b9ee086bfffe095315.dip0.t-ipconnect.de) |
| 17:02:27 | × | ivelten quits (~ivelten@2804:82b8:8:ee01:fda6:516:611b:3176) (Quit: Textual IRC Client: www.textualapp.com) |
| 17:04:26 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 17:07:00 | <c_wraith> | actually, it's worse than I thought. I don't see any way at all to relate n-1 as a value to n-1 as a type, no matter what you know about n as a type |
| 17:08:38 | × | Alleria quits (~JohnGalt@user/alleria) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 17:10:51 | <c_wraith> | So, like.. you're just going to have to unsafeCoerce, I guess! |
| 17:11:58 | × | danse-nr3 quits (~danse@151.35.247.219) (Ping timeout: 268 seconds) |
| 17:12:45 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:18:32 | → | danza joins (~francesco@151.35.247.219) |
| 17:20:02 | → | Alleria joins (~JohnGalt@user/alleria) |
| 17:20:40 | × | Alleria quits (~JohnGalt@user/alleria) (Client Quit) |
| 17:21:20 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:21:41 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:21:57 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 17:25:39 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 17:28:08 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 17:28:18 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 17:34:40 | × | sawilagar quits (~sawilagar@user/sawilagar) (Quit: Leaving) |
| 17:36:38 | → | Alleria joins (~JohnGalt@user/alleria) |
| 17:38:20 | → | dhil joins (~dhil@2001:8e0:2014:3100:8e3a:5299:914c:abf4) |
| 17:38:42 | × | CiaoSen quits (~Jura@2a05:5800:28a:6100:2a3a:4dff:fe84:dbd5) (Ping timeout: 260 seconds) |
| 17:39:58 | → | cstml joins (~cstml@user/cstml) |
| 17:40:09 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 17:41:28 | × | Alleria quits (~JohnGalt@user/alleria) (Ping timeout: 255 seconds) |
| 17:41:28 | × | komikat quits (~akshitkr@218.185.248.66) (Ping timeout: 255 seconds) |
| 17:41:57 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 17:46:55 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 17:49:58 | × | alp_ quits (~alp@2001:861:e3d6:8f80:882f:ff0d:da80:ca07) (Ping timeout: 246 seconds) |
| 17:53:30 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:54:42 | × | shapr quits (~user@2600:1700:c640:3100:a007:14d5:426f:261d) (Remote host closed the connection) |
| 17:54:56 | → | shapr joins (~user@2600:1700:c640:3100:f067:6b60:6d79:cd2d) |
| 17:55:46 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:5836:1305:ce95:7f7f) (Remote host closed the connection) |
| 17:56:01 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) |
| 18:02:34 | <c_wraith> | ski: (or anyone else) https://paste.tomsmeding.com/I2hpWpM9 Am I wrong? Can this be done without unsafeCoerce or a type checker plugin? |
| 18:03:55 | × | danza quits (~francesco@151.35.247.219) (Read error: Connection reset by peer) |
| 18:04:23 | → | qqq joins (~qqq@92.43.167.61) |
| 18:04:44 | <c_wraith> | well, ok. it can also be done by changing to an inductive Nat type instead of using a type literal. |
| 18:07:00 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:07:19 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:07:46 | <dolio> | Yeah, I think the reason you can't do it is because the instances for KnownNat aren't inductive. |
| 18:08:49 | <ski> | `KnownNat n => KnownNat (1 + n)' wouldn't help, would it ? |
| 18:09:31 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 245 seconds) |
| 18:09:32 | <dolio> | It would if the continuation had a KnownNat constraint. |
| 18:10:06 | <c_wraith> | which is a fine thing to add. |
| 18:11:13 | <c_wraith> | I'm honestly surprised the SNat stuff didn't have tools to do that |
| 18:11:39 | <c_wraith> | it seems like the right place to put them |
| 18:11:40 | <ski> | how would it help ? |
| 18:12:20 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:12:30 | <c_wraith> | something like SNatPlus :: SNat -> SNat -> SNat |
| 18:12:53 | × | harveypwca quits (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) (Quit: Leaving) |
| 18:13:01 | <dolio> | Because then it would instantiate to `forall n. KnownNat n => List (1 + n) a -> x`, which is used to build the continuation for the recursive call. |
| 18:13:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) (Remote host closed the connection) |
| 18:13:37 | <dolio> | Assuming the cons has length 1 + n. |
| 18:14:04 | <c_wraith> | err. SNat m -> SNat n -> SNat (m + n) |
| 18:14:48 | <c_wraith> | the partial functions would need a more clever type, but it could be done |
| 18:15:32 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) |
| 18:16:12 | <ski> | replicateExists k e (f :: forall n. KnownNat n => List n a -> o) = replicateExists (k - 1) e ((\ls -> f (e :< ls)) :: forall m. KnownNat m => List m a -> o) |
| 18:16:21 | <dolio> | Oh, but there's another problem. There's no connection between the supplied Integer argument and the type level natural. |
| 18:16:41 | <ski> | right, so `n = m + 1', and given `KnownNat m' we deduce `KnownNat n' |
| 18:17:24 | <c_wraith> | dolio: that doesn't actually matter if the KnownNat constraint is provided to the continuation, thanks to sameNat |
| 18:17:46 | <ski> | dolio : yea, that's what started this conversation branch, more or less |
| 18:18:01 | <dolio> | It matters in replicate, because e.g. `id` isn't a valid continuation. |
| 18:18:08 | <dolio> | It's a skolem escape. |
| 18:18:25 | <c_wraith> | you have to use sameNat and match it Just Refl |
| 18:18:27 | <ski> | right, you must use `n' locally |
| 18:18:48 | <c_wraith> | then you have proven the types are the same, and the skolem is safely trapped |
| 18:18:59 | <dolio> | You have to structure it differently, even if you have the inductive instances. |
| 18:19:36 | → | danza joins (~francesco@151.57.236.24) |
| 18:19:52 | <c_wraith> | I mean, you're correct that you can't use id |
| 18:20:12 | <ski> | (you could still use `WrapList :: KnownNat n => List n a -> SomeList a' as continuation) |
| 18:20:14 | <c_wraith> | but the tools you need are already there so long as the KnownNat constraint is there |
| 18:22:52 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 18:23:03 | → | euleritian joins (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) |
| 18:31:22 | → | cstml19 joins (~cstml@user/cstml) |
| 18:32:40 | × | cstml19 quits (~cstml@user/cstml) (Client Quit) |
| 18:33:28 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 18:35:20 | → | notzmv joins (~zmv@user/notzmv) |
| 18:39:21 | <c_wraith> | yeah... the missing part here is that the singletons in GHC.TypeLits are incomplete. You should have operations in the singletons that mirror the type-level operations provided. |
| 18:39:23 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:40:30 | <c_wraith> | but those are missing. as a result, the tools aren't available to reflect between types and values after applying type-level operations |
| 18:43:39 | × | Umeaboy quits (~Umeaboy@94-255-145-133.cust.bredband2.com) (Quit: Leaving) |
| 18:46:20 | → | AWizzArd joins (~code@user/awizzard) |
| 18:47:09 | × | thegeekinside quits (~thegeekin@189.180.53.210) (Remote host closed the connection) |
| 18:47:48 | <AWizzArd> | When using hspec and hedgehog in the same project (using Cabal 3+), hspec seems to be consuming all tests. I am running hedgehog tests in main but they won't start. Does this ring a bell for anyone? |
| 18:49:29 | × | danza quits (~francesco@151.57.236.24) (Ping timeout: 252 seconds) |
| 18:49:52 | <exarkun> | "Consuming"? |
| 18:49:54 | <c_wraith> | .... wait, maybe the tools are there. I need to come back to this later with a fresh pov |
| 18:51:45 | <c_wraith> | whoops. forget later, I got there now. the tools are indeed absent. |
| 18:52:27 | <AWizzArd> | exarkun: my main is essentially: main = do runHspecTess runHedgehogTests (with correct indentation of course). The HH tests never run. Even if they put them before the hspec tests. This is ignored. |
| 18:52:37 | <AWizzArd> | I can even remove runHspecTests and yet still only they run. Only if I put HH tests before and configure one of the hspec tests to fail the HH tests run. |
| 18:53:43 | <AWizzArd> | It seems to me a bit like some Cabal magic possibly. It discovers the hspec tests and runs them and then quits. |
| 18:54:32 | <geekosaur> | sounds more like something is not being rebuilt, especially if you can remove them and they stilll run |
| 18:54:55 | → | jorik808 joins (~jorik808@d51A48920.access.telenet.be) |
| 18:55:49 | × | euleritian quits (~euleritia@dynamic-046-114-032-227.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:56:09 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:57:10 | <AWizzArd> | geekosaur: yes, I deleted dist/ and new-dist/ but this didn’t change the outcome. Actually I had only one single hspec test. Now I have two. If I outcomment the hspec tests I still get this result: 1 of 1 test suites (1 of 1 test cases) passed. — it should say 2 tests passed |
| 19:00:35 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 19:03:27 | <AWizzArd> | I now found a log file that has been created. And the hedegehog tests do run, but they seem to log to that file and not to the screen! |
| 19:03:37 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 19:04:48 | <geekosaur> | are you using `cabal test`? if so then you want `--test-show-details=streaming` |
| 19:06:16 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:07:50 | × | cstml quits (~cstml@user/cstml) (Ping timeout: 260 seconds) |
| 19:08:09 | <AWizzArd> | geekosaur: aah, this displays the result on the screen! |
| 19:08:12 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 19:08:18 | → | cstml joins (~cstml@user/cstml) |
| 19:08:20 | <AWizzArd> | geekosaur: Excellent, thx! |
| 19:10:18 | <AWizzArd> | Is there also some kind of file watching capability built-in? Or would I be best advised to use some Linux tools for this? |
| 19:10:35 | <geekosaur> | I don't think there is |
| 19:10:43 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 19:11:03 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 19:12:34 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) (Remote host closed the connection) |
| 19:13:44 | <haskellbridge> | 06<sm> can recommend watchexec |
| 19:18:48 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 19:20:10 | → | qhong joins (~qhong@rescomp-21-400677.stanford.edu) |
| 19:20:22 | <AWizzArd> | haskellbridge: will have a look, thx |
| 19:26:23 | <ski> | s/haskellbridge/sm/ |
| 19:27:58 | ski | idly notes haskellbridge adds ZWSP, not some diacritic |
| 19:28:24 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 19:35:31 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) |
| 19:36:40 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 19:42:29 | × | cstml quits (~cstml@user/cstml) (Quit: WeeChat 3.7.1) |
| 19:45:01 | → | alp_ joins (~alp@2001:861:e3d6:8f80:4342:868e:5cc7:17fd) |
| 19:53:36 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) (Remote host closed the connection) |
| 19:55:53 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:58:42 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:59:03 | <tomsmeding> | ski: I saw some irc user elsewhere claim that that was "conventional" as a friently, i.e. non-notifying, mention |
| 19:59:38 | <tomsmeding> | not that I know how to type that character without going to https://tomsmeding.com/unicode |
| 20:00:10 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 20:00:22 | → | Pickchea joins (~private@user/pickchea) |
| 20:01:35 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 20:01:45 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 20:04:48 | <ski> | tomsmeding : yea. i'm just wondering to what extent it is an issue (compared to the complication it ensues) |
| 20:05:30 | <tomsmeding> | as in, that clients render it incorrectly or something? |
| 20:05:45 | <ski> | e.g. there is no nick "sm" in this channel, only on the other side of the bridge, so in this particular case that argument about non-notifying doesn't apply |
| 20:06:08 | <ski> | (and it does mean that if i search backlog for `<sm>', i won't find those abridged messages) |
| 20:07:02 | <ski> | tomsmeding : no, as in there's no issue with you getting noticed on the other side of the bridge, when saying something, if you're not actually also on the other side of the bridge (with the same nick) |
| 20:07:21 | <tomsmeding> | ski: ah, fair point |
| 20:08:07 | <tomsmeding> | though I believe there are indeed a few people who have a client on both sides of the bridge, at least occasionally |
| 20:08:19 | <ski> | (the ZWSP also renders as an extra unicode modification of the previous glyph, here .. making it looked like a dotted box above the character, which in turn makes it hard to make out the first character, so that i have to copy, and then delete the ZWSP in order to see which nick it's supposed to be) |
| 20:08:57 | <ski> | yes. but the bridge could, conceivably, only add ZWSP for messages from such nicks, and not to messages from all nicks |
| 20:08:59 | <tomsmeding> | ski: that sounds like a renderer problem :D https://ircbrowse.tomsmeding.com/browse/lchaskell?id=1153514#trid1153514 |
| 20:09:03 | <tomsmeding> | true |
| 20:09:06 | <ski> | yes |
| 20:10:59 | <ski> | tomsmeding : oh .. for some reason the log doesn't seem to handle the color code gracefully |
| 20:11:09 | <tomsmeding> | yeah I saw that too |
| 20:11:13 | <tomsmeding> | I'm less concerned about that |
| 20:11:32 | <tomsmeding> | I suspect it's just not interpreting the color code at all and just piping it to the browser, which shrugs and gives you this |
| 20:11:38 | <ski> | (if it just displayed the escape as `C', rather than silently ignoring it, that would be fine) |
| 20:12:08 | <tomsmeding> | yeah the escape byte is there literally in the html |
| 20:12:26 | <tomsmeding> | a \x03 byte |
| 20:12:40 | <EvanR> | > '\3' |
| 20:12:41 | <lambdabot> | '\ETX' |
| 20:12:47 | <tomsmeding> | end-of-text |
| 20:12:52 | <tomsmeding> | ¯\_(ツ)_/¯ |
| 20:13:00 | <ski> | (or `␃', yes) |
| 20:13:01 | <EvanR> | never seen that one before xD |
| 20:13:15 | <tomsmeding> | 03yes you have |
| 20:13:19 | <EvanR> | wtf |
| 20:13:46 | <tomsmeding> | https://modern.ircdocs.horse/formatting.html#color |
| 20:13:56 | ski | 11idly 07glances 13around |
| 20:14:18 | <tomsmeding> | EvanR: this is how haskellbridge does the coloured nicks :p |
| 20:15:03 | <EvanR> | when did all this happen |
| 20:15:09 | <ski> | since mIRC days |
| 20:15:21 | <EvanR> | I'm still recovering from ESC m |
| 20:15:21 | <ski> | it's not anything new |
| 20:15:38 | <ski> | (some of the other markup are new, though) |
| 20:15:46 | <tomsmeding> | bold |
| 20:15:59 | <EvanR> | how are you entering that |
| 20:16:03 | <tomsmeding> | italics are not always supported in terminals |
| 20:16:39 | <tomsmeding> | weechat has a hotkey, 'ctrl-c, c' produces a \x03 byte; but this depends on your client |
| 20:16:56 | <tomsmeding> | so to get bold I type ctrl-c, c, b, o, l, d, ctrl-c, o |
| 20:17:12 | <tomsmeding> | in irssi it's ctrl-c and ctrl-o iirc |
| 20:17:20 | <tomsmeding> | from a previous conversation about this :D |
| 20:17:48 | <[exa]> | oh irc colors are back, 1990 vibes |
| 20:17:48 | <EvanR> | bold |
| 20:18:09 | <EvanR> | I'm left out in the bold |
| 20:18:29 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:18:40 | <tomsmeding> | (don't see any control characters, if that was your intention) |
| 20:18:46 | <ski> | (i believe BboldB,_ underlined B,VinverseV are quite old, while ] italicized ],FblinkingF,^ strukthrough ^,QmonospacedQ are newer) |
| 20:19:00 | <tomsmeding> | how much effort took it to enter that |
| 20:19:04 | <ski> | yes |
| 20:19:09 | <tomsmeding> | right |
| 20:20:27 | <ski> | <https://modern.ircdocs.horse/formatting.html#characters>,<https://www.mirc.com/help/html/control_codes.html>,<https://www.mirc.com/colors.html>,<https://web.archive.org/web/20120211151852/http://ircle.com:80/colorfaq.shtml> |
| 20:20:40 | <dminuoso_> | Im getting an error `[...] This makes type inference for inner bindings fragile; either use MonoLocalBinds, or simplify it using the instance` |
| 20:20:43 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 20:20:47 | <ski> | (note that the last link talks about a different (incompatible) color coding scheme) |
| 20:21:10 | <dminuoso_> | Before it just says "The constraint C matches an instance declaration D" |
| 20:21:12 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 20:21:29 | <dminuoso_> | This is quite the terrible diagnostic, it really doesnt tell me whats going on or why its bad |
| 20:21:34 | <tomsmeding> | yeah, I knew which diagnostic that message fragment was from :p |
| 20:21:37 | <tomsmeding> | why it's bad I also don't know |
| 20:22:03 | <geekosaur> | I think it's described in the users guide under MonoLocalBinds |
| 20:22:30 | <ski> | tomsmeding : fwiw, most of the effort there was to not only turn on and off the markup formatting, but also to explicitly display which control codes were needed to do that |
| 20:22:47 | <tomsmeding> | ski: I recognised that, hence my response :p |
| 20:24:04 | ski | idly wonders what `C' and `D' would be, here |
| 20:24:23 | <dminuoso_> | • The constraint ‘GenericMode AsApi’ matches instance GenericMode AsApi -- Defined in ‘Servant.API.Generic’ |
| 20:24:29 | <geekosaur> | https://downloads.haskell.org/ghc/9.8.1/docs/users_guide/exts/let_generalisation.html |
| 20:24:39 | <tomsmeding> | ski: isn't C colour? |
| 20:24:56 | <ski> | yes (but i was speaking of dminuoso_'s issue there) |
| 20:25:01 | <tomsmeding> | ah |
| 20:25:36 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 268 seconds) |
| 20:25:55 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:f8e2:da48:b27b:3920) |
| 20:26:12 | <dminuoso_> | geekosaur: Yeah even with that user guide, I cant figure out whats going on here. |
| 20:26:46 | <dminuoso_> | It feels like "fragility" is something you might find in some exotic paper on the subject. |
| 20:27:06 | <dminuoso_> | I mean yes. the constraint "GenericMode AsApi" matches "instance GenericMode AsApi". |
| 20:27:21 | <dminuoso_> | And "Functor Maybe" matches "instance Functor Maybe" |
| 20:27:45 | <dminuoso_> | The way GHC presents this error, it suggests that constraints matching instances is a deep problem. |
| 20:27:51 | <dminuoso_> | As if this should never occur. |
| 20:27:52 | <ski> | the matrix bridge (in the earlier mode, before the change), would use monospace, i assume for fragments that were entered in some kind of quotes, but then wouldn't use it again to turn it off, but rather just use "turn off all color and markup" (being `O') .. with the result that i could see where the monospaced part started (since my client displayed it as `Q', not understanding that escape code), |
| 20:27:58 | <ski> | while, otoh, not being able to see where it ended (since `O' is recognized) |
| 20:28:21 | <tomsmeding> | I think it's mostly not about trivial constraints like 'Functor Maybe', but more about things like 'Semigroup (Maybe a)', which is apparently (?) more fragile (?) than 'Semigroup a' |
| 20:28:45 | <ski> | `FlexibleConstraints' ? |
| 20:28:54 | <geekosaur> | is either a GADT or a type family involved? I get the impression those are the fragile ones |
| 20:29:05 | <ski> | (er, s/Constraints/Contexts/) |
| 20:29:38 | <dminuoso_> | ski: Its on, yes. My main issue here is just that GHC isnt really communicating whats going on. |
| 20:29:51 | <ski> | yes |
| 20:30:07 | <dminuoso_> | It feels like the condition "constraint C matches instance D" is problematic under a very specific inference... thing. |
| 20:30:08 | <ski> | would be interesting to see a, perhaps minimal, example of this in action |
| 20:30:13 | <tomsmeding> | well, it's communicating that you shouldn't do this, but not why |
| 20:30:16 | <dminuoso_> | But GHC is completely silent on what the "very specific inference thing is" |
| 20:30:22 | <tomsmeding> | yep |
| 20:30:35 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 20:30:50 | <dminuoso_> | So Im carrying away "constraints should not match instances", which of course is in direct conflict with "No instance found" errors. |
| 20:31:01 | <dminuoso_> | GHC has a way of driving me crazy sometimes. |
| 20:31:11 | <tomsmeding> | constraints should not be _manually simplifiable using instances_ |
| 20:31:14 | <tomsmeding> | that's what the error is saying |
| 20:31:18 | <tomsmeding> | again, why, I don't know |
| 20:32:47 | <dminuoso_> | Okay as usual, a look inside GHC seems to help |
| 20:32:49 | <dminuoso_> | Note [Simplifiable given constraints] |
| 20:33:21 | <dminuoso_> | Note [Instance and Given overlap] too |
| 20:34:15 | <dminuoso_> | heh! that last note is referenced, but seems to have been lost/deleted. |
| 20:34:41 | <dminuoso_> | Some modules point to GHC.Tc.Solver.Dict, others point to TcInteract |
| 20:35:18 | <dminuoso_> | Ohh! No, it just uses {--} style comments, strange. |
| 20:56:45 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 256 seconds) |
| 20:57:55 | × | shapr quits (~user@2600:1700:c640:3100:f067:6b60:6d79:cd2d) (Remote host closed the connection) |
| 20:58:08 | → | shapr joins (~user@2600:1700:c640:3100:cd00:5363:89ce:baba) |
| 21:13:24 | × | mmhat quits (~mmh@p200300f1c71a22b9ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 21:13:46 | → | mmhat joins (~mmh@p200300f1c71a22daee086bfffe095315.dip0.t-ipconnect.de) |
| 21:17:43 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 21:28:47 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 21:38:01 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 21:40:51 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 21:43:36 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 21:48:08 | × | dhil quits (~dhil@2001:8e0:2014:3100:8e3a:5299:914c:abf4) (Ping timeout: 252 seconds) |
| 21:48:08 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 21:53:12 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 21:56:38 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 21:57:02 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 252 seconds) |
| 22:03:14 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Remote host closed the connection) |
| 22:06:22 | → | chexum_ joins (~quassel@gateway/tor-sasl/chexum) |
| 22:07:27 | × | alp_ quits (~alp@2001:861:e3d6:8f80:4342:868e:5cc7:17fd) (Ping timeout: 256 seconds) |
| 22:08:00 | → | talismanick joins (~user@2601:204:ef00:bb0::f34e) |
| 22:08:07 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 240 seconds) |
| 22:13:15 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 22:25:11 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 264 seconds) |
| 22:30:05 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 22:32:28 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 22:33:15 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 268 seconds) |
| 22:34:34 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:37:21 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 22:37:42 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:38:11 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
| 22:40:09 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 22:44:54 | → | mengu joins (~mengu@c83-254-18-254.bredband.tele2.se) |
| 22:48:46 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 22:55:22 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 22:56:04 | × | acidjnk quits (~acidjnk@p200300d6e72b9352dcea2d781ea8e5a4.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 22:56:55 | × | JeremyB99 quits (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) (Read error: Connection reset by peer) |
| 22:57:16 | → | JeremyB99 joins (~JeremyB99@2600:1702:21b0:a500:6581:2a34:dec3:8883) |
| 23:04:31 | × | mengu quits (~mengu@c83-254-18-254.bredband.tele2.se) (Quit: Client closed) |
| 23:04:43 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:07:11 | × | vishnix quits (~vishwas@c-73-9-42-9.hsd1.il.comcast.net) (Quit: leaving) |
| 23:09:57 | → | FinnBoat joins (~user@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) |
| 23:11:01 | × | mikess quits (~sam@user/mikess) (Quit: leaving) |
| 23:14:42 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 23:15:08 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:16:52 | × | mmhat quits (~mmh@p200300f1c71a22daee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 23:20:02 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 256 seconds) |
| 23:33:35 | → | mmhat joins (~mmh@p200300f1c723fb89ee086bfffe095315.dip0.t-ipconnect.de) |
| 23:37:52 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 23:38:02 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 260 seconds) |
| 23:38:58 | × | mmhat quits (~mmh@p200300f1c723fb89ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:43:37 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 23:43:45 | → | leungbk joins (~user@2603-8000-1201-2dd2-33ab-dcc3-8406-2f52.res6.spectrum.com) |
| 23:46:42 | → | pavonia joins (~user@user/siracusa) |
| 23:48:11 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 23:50:21 | × | hammond quits (proscan@user/hammond2) (Ping timeout: 245 seconds) |
| 23:50:38 | × | FinnBoat quits (~user@rul16-h01-176-151-21-224.dsl.sta.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 23:51:57 | → | pandry joins (~Pandry@93-41-34-64.ip79.fastwebnet.it) |
| 23:52:28 | → | mmhat joins (~mmh@p200300f1c7246193ee086bfffe095315.dip0.t-ipconnect.de) |
| 23:53:26 | × | talismanick quits (~user@2601:204:ef00:bb0::f34e) (Ping timeout: 260 seconds) |
| 23:54:17 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 23:56:59 | × | pandry quits (~Pandry@93-41-34-64.ip79.fastwebnet.it) (Ping timeout: 264 seconds) |
All times are in UTC on 2023-11-29.