Logs: freenode/#haskell
| 2021-03-31 02:17:08 | → | drakonis joins (~drakonis@unaffiliated/drakonis) |
| 2021-03-31 02:17:49 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-03-31 02:18:20 | × | Guest41032 quits (~laudiacay@67.176.215.84) (Ping timeout: 268 seconds) |
| 2021-03-31 02:20:40 | × | carlomagno quits (~cararell@148.87.23.6) (Remote host closed the connection) |
| 2021-03-31 02:20:46 | → | drbean_ joins (~drbean@TC210-63-209-55.static.apol.com.tw) |
| 2021-03-31 02:21:00 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-uawxrfrpxwexcklr) (Quit: Connection closed for inactivity) |
| 2021-03-31 02:22:38 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 268 seconds) |
| 2021-03-31 02:24:00 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-31 02:24:04 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 2021-03-31 02:27:02 | → | ezrakilty joins (~ezrakilty@97-113-35-199.tukw.qwest.net) |
| 2021-03-31 02:27:23 | × | average quits (uid473595@gateway/web/irccloud.com/x-mdzvkbciicshchec) (Quit: Connection closed for inactivity) |
| 2021-03-31 02:30:50 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 2021-03-31 02:33:21 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-31 02:33:53 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2021-03-31 02:34:33 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-31 02:38:04 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 252 seconds) |
| 2021-03-31 02:42:17 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Quit: WeeChat 3.0.1) |
| 2021-03-31 02:44:49 | × | ezrakilty quits (~ezrakilty@97-113-35-199.tukw.qwest.net) (Remote host closed the connection) |
| 2021-03-31 02:45:32 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-03-31 02:45:34 | → | shad0w_ joins (a0ca25aa@160.202.37.170) |
| 2021-03-31 02:50:07 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 258 seconds) |
| 2021-03-31 02:50:21 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 260 seconds) |
| 2021-03-31 02:51:22 | → | ddellacosta joins (~ddellacos@86.106.143.66) |
| 2021-03-31 02:55:28 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:14ea:f44:a077:bc09) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-31 02:56:02 | × | ddellacosta quits (~ddellacos@86.106.143.66) (Ping timeout: 252 seconds) |
| 2021-03-31 02:56:49 | → | lewky joins (~lewky@159.65.37.240) |
| 2021-03-31 02:57:00 | → | DTZUZU_ joins (~DTZUZO@207.81.119.43) |
| 2021-03-31 02:57:05 | → | RusAlex joins (~Chel@unaffiliated/rusalex) |
| 2021-03-31 02:58:59 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 246 seconds) |
| 2021-03-31 03:02:29 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-31 03:04:08 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 2021-03-31 03:16:46 | × | motherfsck quits (~motherfsc@unaffiliated/motherfsck) (Ping timeout: 240 seconds) |
| 2021-03-31 03:17:58 | × | drbean_ quits (~drbean@TC210-63-209-55.static.apol.com.tw) (Ping timeout: 240 seconds) |
| 2021-03-31 03:22:32 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-03-31 03:23:02 | → | motherfsck joins (~motherfsc@unaffiliated/motherfsck) |
| 2021-03-31 03:23:07 | → | matryoshka` joins (~matryoshk@2606:6080:1002:8:3285:30e:de43:8809) |
| 2021-03-31 03:24:06 | × | matryoshka quits (~matryoshk@2606:6080:1002:8:3285:30e:de43:8809) (Read error: Connection reset by peer) |
| 2021-03-31 03:25:21 | × | dpl quits (~dpl@77.121.78.163) (Ping timeout: 260 seconds) |
| 2021-03-31 03:31:03 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-03-31 03:32:09 | → | ddellaco_ joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-03-31 03:33:01 | → | poljar1 joins (~poljar@93-139-86-101.adsl.net.t-com.hr) |
| 2021-03-31 03:35:33 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 260 seconds) |
| 2021-03-31 03:36:02 | × | poljar quits (~poljar@93-143-162-187.adsl.net.t-com.hr) (Ping timeout: 268 seconds) |
| 2021-03-31 03:36:20 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 2021-03-31 03:36:24 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-03-31 03:36:26 | × | ddellaco_ quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 2021-03-31 03:36:38 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 2021-03-31 03:39:35 | × | matryoshka` quits (~matryoshk@2606:6080:1002:8:3285:30e:de43:8809) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-03-31 03:44:58 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-03-31 03:45:26 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Remote host closed the connection) |
| 2021-03-31 03:46:16 | × | _xor quits (~xor@74.215.46.133) (Quit: WeeChat 3.1) |
| 2021-03-31 03:56:50 | → | raym joins (~ray@115.187.32.14) |
| 2021-03-31 03:59:29 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-03-31 03:59:40 | → | _xor joins (~xor@74.215.46.133) |
| 2021-03-31 04:00:19 | → | Alleria joins (~textual@2603-7000-3040-0000-1143-d148-dab6-7a8a.res6.spectrum.com) |
| 2021-03-31 04:00:41 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 268 seconds) |
| 2021-03-31 04:00:42 | Alleria | is now known as Guest30185 |
| 2021-03-31 04:01:23 | → | borne joins (~fritjof@200116b864cfc800f7ed9fd86a2491f0.dip.versatel-1u1.de) |
| 2021-03-31 04:01:41 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Quit: Lost terminal) |
| 2021-03-31 04:01:55 | × | electricityZZZZ quits (~electrici@135-180-3-82.static.sonic.net) (Ping timeout: 268 seconds) |
| 2021-03-31 04:03:07 | → | Kaeipi joins (~Kaiepi@47.54.252.148) |
| 2021-03-31 04:03:09 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 2021-03-31 04:03:38 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-03-31 04:04:31 | × | Guest30185 quits (~textual@2603-7000-3040-0000-1143-d148-dab6-7a8a.res6.spectrum.com) (Ping timeout: 245 seconds) |
| 2021-03-31 04:07:01 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-31 04:08:14 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 2021-03-31 04:08:47 | → | Guest41032 joins (~laudiacay@67.176.215.84) |
| 2021-03-31 04:12:01 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-03-31 04:12:25 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 268 seconds) |
| 2021-03-31 04:13:07 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-31 04:13:53 | × | borne quits (~fritjof@200116b864cfc800f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 250 seconds) |
| 2021-03-31 04:15:00 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2021-03-31 04:15:33 | → | borne joins (~fritjof@200116b86411e500998fce1c43ef4e0a.dip.versatel-1u1.de) |
| 2021-03-31 04:16:26 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 2021-03-31 04:20:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 2021-03-31 04:20:49 | → | Nobita joins (ca0e7816@202.14.120.22) |
| 2021-03-31 04:21:19 | × | Nobita quits (ca0e7816@202.14.120.22) (Client Quit) |
| 2021-03-31 04:23:38 | × | deviantfero quits (~deviantfe@190.150.27.58) (Ping timeout: 260 seconds) |
| 2021-03-31 04:24:02 | <edwardk> | these linear logic proofs are making me go cross-eyed |
| 2021-03-31 04:24:58 | <edwardk> | https://github.com/ekmett/linear-logic/blob/main/src/Linear/Logic/Functor.hs#L1270 |
| 2021-03-31 04:27:38 | × | alx741 quits (~alx741@181.196.68.106) (Quit: alx741) |
| 2021-03-31 04:30:24 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-31 04:30:30 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:cdc8:88ee:4ef9:ae5c) |
| 2021-03-31 04:33:27 | → | JanBessa1 joins (~JanB@85-22-26-176.ip.dokom21.de) |
| 2021-03-31 04:33:37 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2021-03-31 04:35:27 | <glguy> | edwardk, how much of that is blindly following the types, and how much is creative? |
| 2021-03-31 04:35:51 | × | dbmikus quits (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) (Ping timeout: 268 seconds) |
| 2021-03-31 04:37:06 | × | JanBessai quits (~JanB@85-22-13-230.ip.dokom21.de) (Ping timeout: 260 seconds) |
| 2021-03-31 04:37:30 | <edwardk> | it actually gets difficult at times, but a lot os blind type following |
| 2021-03-31 04:37:38 | <edwardk> | a little tactic engine would knock these out fast |
| 2021-03-31 04:38:02 | <nshepperd2> | is this coq but in haskell |
| 2021-03-31 04:40:06 | <edwardk> | nshepperd2: in https://github.com/ekmett/linear-logic/blob/main/src/Linear/Logic/Internal.hs#L54 i define a 'full' intuitionistic linear logic suite using the limited linear haskell a %1 -> b arrow as half of my arrow, and by attaching involutively the notion of what evidence it takes to refute a given proof. |
| 2021-03-31 04:40:31 | <edwardk> | then once i have that, and build with and par, which are the missing connectives, its off to the races. |
| 2021-03-31 04:41:05 | <edwardk> | then i wanted a place to put all my boilerplate proofs, so i started adding bifunctors, monoidal category structure, etc. |
| 2021-03-31 04:41:30 | <edwardk> | but once i had that it was somewhat disappointing that the proofs couldn't flow back into the arguments for bimap, etc. |
| 2021-03-31 04:41:45 | <edwardk> | because they were external to the logic program itself. |
| 2021-03-31 04:41:53 | <edwardk> | but i was able to internalize them too |
| 2021-03-31 04:42:10 | × | evanjs quits (~evanjs@075-129-098-007.res.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-31 04:43:09 | <edwardk> | glguy: as for hard parts, i'd say it takes a good deal of creativity to figure out how to plumb apartness information around when you get more complicated proofs involving isos |
| 2021-03-31 04:43:25 | <edwardk> | using holes is critical to getting anything done |
All times are in UTC.