Logs: freenode/#haskell
| 2021-04-04 16:38:49 | <tomsmeding> | *dependently-typed |
| 2021-04-04 16:39:06 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 260 seconds) |
| 2021-04-04 16:39:11 | <dmwit> | I don't think you can make it work with GHC's type-level naturals, because you can't recurse at the type level with them. |
| 2021-04-04 16:39:13 | <tomsmeding> | though you can partially fake it with a GADT |
| 2021-04-04 16:39:23 | <dmwit> | At least, not easily. You need some, like, unsafeCoerce and stuff. |
| 2021-04-04 16:39:28 | <tomsmeding> | really? |
| 2021-04-04 16:39:33 | <tomsmeding> | :( |
| 2021-04-04 16:39:33 | <dmwit> | yeah =( |
| 2021-04-04 16:40:07 | × | fendor quits (~fendor@178.165.129.178.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-04-04 16:40:08 | <dmwit> | I think it would be rad to have one extra class in some future GHC that was just a recursion principle for Nat |
| 2021-04-04 16:43:57 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 2021-04-04 16:44:04 | <monochrom> | Conclusion: Free monads are an expanded dynamic typing regime. (Note that SomeMany f is the free monad from functor f. >:) ) |
| 2021-04-04 16:46:11 | → | alx741 joins (~alx741@181.196.69.45) |
| 2021-04-04 16:47:12 | <monochrom> | But what does "many alg (Zero a)" do? |
| 2021-04-04 16:47:37 | <monochrom> | Err nevermind. |
| 2021-04-04 16:47:58 | × | thc202 quits (~thc202@unaffiliated/thc202) (Read error: Connection reset by peer) |
| 2021-04-04 16:48:08 | <dmwit> | You know, I think I could actually get on board with "free monads are an expanded dynamic typing regime". Sounds like excellent propaganda. |
| 2021-04-04 16:48:17 | <monochrom> | :) |
| 2021-04-04 16:48:42 | <dmwit> | Those two sentences are completely independent, and neither causes the other. |
| 2021-04-04 16:51:35 | → | carlomagno1 joins (~cararell@148.87.23.12) |
| 2021-04-04 16:51:45 | → | fendor joins (~fendor@178.165.129.178.wireless.dyn.drei.com) |
| 2021-04-04 16:52:30 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-04-04 16:53:22 | → | AkechiShiro joins (~AkechiShi@2a01:e0a:5f9:9681:1473:3dff:fe42:56a9) |
| 2021-04-04 16:54:34 | × | carlomagno quits (~cararell@148.87.23.10) (Ping timeout: 260 seconds) |
| 2021-04-04 16:56:02 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:69f6:cf35:c577:84e2) |
| 2021-04-04 16:58:21 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 2021-04-04 16:58:37 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-04-04 16:58:46 | × | alx741 quits (~alx741@181.196.69.45) (Quit: alx741) |
| 2021-04-04 16:58:55 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-04-04 16:59:32 | → | ambiso99211 joins (~ambiso@209.182.239.205) |
| 2021-04-04 16:59:43 | × | ambiso9921 quits (~ambiso@209.182.239.205) (Ping timeout: 252 seconds) |
| 2021-04-04 17:01:39 | × | AkechiShiro quits (~AkechiShi@2a01:e0a:5f9:9681:1473:3dff:fe42:56a9) (Quit: WeeChat 2.9) |
| 2021-04-04 17:02:06 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-04-04 17:04:07 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-04-04 17:05:49 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:69f6:cf35:c577:84e2) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-04 17:08:36 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 2021-04-04 17:09:45 | × | debugloop quits (~danieln@unaffiliated/debugloop) (Quit: WeeChat 3.0) |
| 2021-04-04 17:09:51 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-04-04 17:10:05 | → | debugloop joins (~danieln@unaffiliated/debugloop) |
| 2021-04-04 17:13:39 | → | AkechiShiro joins (~AkechiShi@2a01:e0a:5f9:9681:1473:3dff:fe42:56a9) |
| 2021-04-04 17:14:03 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-04 17:18:14 | × | elliott_ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Quit: WeeChat 3.1) |
| 2021-04-04 17:24:44 | × | ddere quits (uid110888@gateway/web/irccloud.com/x-zsaufvbzeddqdaps) (Quit: Connection closed for inactivity) |
| 2021-04-04 17:32:00 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2021-04-04 17:32:28 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 2021-04-04 17:36:53 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 17:39:42 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-04-04 17:40:32 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 268 seconds) |
| 2021-04-04 17:43:44 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 245 seconds) |
| 2021-04-04 17:45:23 | × | xff0x quits (~xff0x@2001:1a81:5223:f300:8ecc:fc17:b59f:86b8) (Ping timeout: 260 seconds) |
| 2021-04-04 17:45:42 | → | guest1123581321 joins (~jaroslawj@185.234.208.208.r.toneticgroup.pl) |
| 2021-04-04 17:46:02 | → | xff0x joins (~xff0x@2001:1a81:5223:f300:bd35:cc29:5dd:ed37) |
| 2021-04-04 17:48:55 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-qihmpjrjaahvhsww) |
| 2021-04-04 17:50:13 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-04-04 17:52:23 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 260 seconds) |
| 2021-04-04 17:53:10 | → | stree joins (~stree@68.36.8.116) |
| 2021-04-04 18:03:17 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-04-04 18:04:27 | → | esp32_prog joins (esp32_prog@gateway/vpn/mullvad/esp32prog/x-46565127) |
| 2021-04-04 18:04:31 | × | enoq quits (~textual@194-208-146-143.lampert.tv) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-04 18:05:07 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 2021-04-04 18:09:09 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 18:10:53 | × | Franciman quits (~francesco@host-87-20-23-243.retail.telecomitalia.it) (Quit: Leaving) |
| 2021-04-04 18:12:21 | × | kuribas quits (~user@ptr-25vy0i83sb71lqt997o.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2021-04-04 18:15:46 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 18:21:42 | × | theGrg quits (~theGrg@185.204.1.185) (Remote host closed the connection) |
| 2021-04-04 18:22:10 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2021-04-04 18:22:32 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 2021-04-04 18:22:47 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 18:23:31 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-tiatbdxsdtnvkusf) |
| 2021-04-04 18:23:35 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 18:23:59 | × | mkDoku quits (~TheMule@aftr-37-201-195-134.unity-media.net) (Ping timeout: 246 seconds) |
| 2021-04-04 18:28:03 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-leagdtamtaexonnr) (Quit: Connection closed for inactivity) |
| 2021-04-04 18:29:12 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 18:32:44 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 18:32:50 | → | DTZUZO joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-04-04 18:33:00 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 2021-04-04 18:33:35 | × | DTZUZO quits (~DTZUZO@205.ip-149-56-132.net) (Client Quit) |
| 2021-04-04 18:33:46 | → | DTZUZO joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-04-04 18:41:05 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 18:42:38 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 2021-04-04 18:46:52 | → | mkDoku joins (~TheMule@aftr-37-201-195-134.unity-media.net) |
| 2021-04-04 18:47:15 | × | dsrt^ quits (dsrt@ip98-184-89-2.mc.at.cox.net) () |
| 2021-04-04 18:49:26 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2021-04-04 18:51:01 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 18:54:48 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 2021-04-04 18:56:22 | → | __minoru__shirae joins (~shiraeesh@5.101.59.244) |
| 2021-04-04 18:57:00 | × | minoru_shiraeesh quits (~shiraeesh@109.166.57.249) (Ping timeout: 268 seconds) |
| 2021-04-04 18:59:14 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 19:00:31 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-04 19:03:56 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-04 19:06:19 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) |
| 2021-04-04 19:06:35 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2021-04-04 19:08:41 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-04-04 19:10:40 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 2021-04-04 19:12:00 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Client Quit) |
| 2021-04-04 19:13:17 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:d1df:45b8:caf8:f009) (Remote host closed the connection) |
| 2021-04-04 19:14:09 | × | malumore quits (~malumore@151.62.121.55) (Remote host closed the connection) |
| 2021-04-04 19:14:28 | → | malumore joins (~malumore@151.62.121.55) |
| 2021-04-04 19:15:08 | → | Guest68323 joins (~Guest6832@c-67-169-67-94.hsd1.ca.comcast.net) |
| 2021-04-04 19:15:11 | × | mikoto-chan quits (~anass@gateway/tor-sasl/mikoto-chan) (Remote host closed the connection) |
All times are in UTC.