Logs: liberachat/#haskell
| 2021-05-31 12:40:17 | <maerwald> | yes |
| 2021-05-31 12:40:19 | <schuelermine> | hm |
| 2021-05-31 12:40:27 | <maerwald> | ecosystem effects aren't considered in that proposal at all |
| 2021-05-31 12:40:32 | → | brandonh joins (~brandonh@151.38.202.252) |
| 2021-05-31 12:40:43 | <the-coot[m]> | maerwald: Agda can be compiled to Haskell; the problem is that in some way you loose control over the low level code (Haskell in this case). |
| 2021-05-31 12:40:48 | <merijn> | schuelermine: I *like* dependent typs, I just don't like the as ad hoc, backwards incompatible change bolted onto a language not designed for it |
| 2021-05-31 12:41:14 | <beaky> | i think agda has a ghc backend too that lets you compile agda as executables or libraries and use between haskell modules |
| 2021-05-31 12:41:31 | <maerwald> | so, why don't we explore that, instead of mudding up Haskell |
| 2021-05-31 12:41:48 | <merijn> | schuelermine: The appeal of, say, Idris and Agda is that there is only one syntax for type and value level that's identical |
| 2021-05-31 12:41:55 | × | igghibu quits (~igghibu@37.120.201.126) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-05-31 12:42:05 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-05-31 12:42:14 | <schuelermine> | I actually feel bolting it in ad hoc could help make it more discoverable |
| 2021-05-31 12:42:17 | → | ksqsf joins (~textual@67.209.186.120.16clouds.com) |
| 2021-05-31 12:42:19 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 2021-05-31 12:42:19 | × | ksqsf quits (~textual@67.209.186.120.16clouds.com) (Client Quit) |
| 2021-05-31 12:42:30 | <schuelermine> | excuse me |
| 2021-05-31 12:42:32 | <merijn> | Haskell pretty explicitly has *different* type and value level syntax, and mixing them now is confusion where some things are correct, some aren't and some mean something different from what you expect |
| 2021-05-31 12:42:43 | <schuelermine> | yeah |
| 2021-05-31 12:43:04 | <merijn> | schuelermine: Have you looked at something like Idris before? Type level programming in Idris is *much* easier to learn/understand than Hasochism, imo |
| 2021-05-31 12:43:17 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 268 seconds) |
| 2021-05-31 12:43:25 | <schuelermine> | Is Idris better than Agda? |
| 2021-05-31 12:44:37 | <schuelermine> | actually no wait |
| 2021-05-31 12:44:37 | <schuelermine> | Does Idris have the same provable productiveness or termination restriction as Agda? |
| 2021-05-31 12:45:12 | <beaky> | yes idris is more designed to be 'pacman complete' as edwin brady would say while also haveing the nice depdnendent types like agda (although it uses a different theory i think) |
| 2021-05-31 12:45:24 | <schuelermine> | I have to leave, my battery is dead |
| 2021-05-31 12:45:29 | <schuelermine> | Thanks |
| 2021-05-31 12:45:45 | <tomsmeding> | rip battery |
| 2021-05-31 12:45:52 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 2021-05-31 12:47:18 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 2021-05-31 12:50:06 | × | schuelermine quits (~schuelerm@2a02:3032:403:c9bf:a3eb:b0ef:ce:fa31) (Ping timeout: 264 seconds) |
| 2021-05-31 12:50:41 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 12:51:17 | → | koishi_ joins (~koishi_@67.209.186.120.16clouds.com) |
| 2021-05-31 12:51:42 | × | Guest31 quits (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-05-31 12:52:42 | × | koishi_ quits (~koishi_@67.209.186.120.16clouds.com) (Remote host closed the connection) |
| 2021-05-31 12:53:19 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) (Quit: WeeChat 2.8) |
| 2021-05-31 12:53:54 | → | koishi_ joins (~koishi_@185.209.85.134) |
| 2021-05-31 12:54:24 | → | eightball joins (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) |
| 2021-05-31 12:58:08 | × | argento quits (~argent0@168.227.96.53) (Ping timeout: 252 seconds) |
| 2021-05-31 12:58:42 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
| 2021-05-31 13:01:15 | → | alx741 joins (~alx741@186.178.108.160) |
| 2021-05-31 13:01:19 | → | sondre joins (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) |
| 2021-05-31 13:01:32 | → | Guest43oreosplas joins (~Guest43or@ip5b40c0d8.dynamic.kabel-deutschland.de) |
| 2021-05-31 13:01:40 | × | Guest43oreosplas quits (~Guest43or@ip5b40c0d8.dynamic.kabel-deutschland.de) (Client Quit) |
| 2021-05-31 13:01:58 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2021-05-31 13:02:05 | × | eightball quits (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) (Quit: Leaving) |
| 2021-05-31 13:02:22 | → | eightball joins (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) |
| 2021-05-31 13:03:22 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2021-05-31 13:04:04 | → | gentauro joins (~gentauro@user/gentauro) |
| 2021-05-31 13:04:53 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 2021-05-31 13:05:53 | × | sondre quits (~sondrelun@eduroam-193-157-245-37.wlan.uio.no) (Ping timeout: 272 seconds) |
| 2021-05-31 13:06:45 | × | koishi_ quits (~koishi_@185.209.85.134) (Quit: /ragequit) |
| 2021-05-31 13:07:25 | × | eightball quits (~eight@162-226-201-119.lightspeed.tukrga.sbcglobal.net) (Quit: Leaving) |
| 2021-05-31 13:09:44 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Read error: Connection reset by peer) |
| 2021-05-31 13:09:47 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 268 seconds) |
| 2021-05-31 13:09:47 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 2021-05-31 13:15:14 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-31 13:23:16 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 13:23:22 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 268 seconds) |
| 2021-05-31 13:23:43 | → | argento joins (~argent0@168.227.96.53) |
| 2021-05-31 13:28:44 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 2021-05-31 13:30:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-31 13:31:16 | → | shryke joins (~shryke@91.103.43.254) |
| 2021-05-31 13:33:53 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 13:34:35 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 265 seconds) |
| 2021-05-31 13:35:14 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-05-31 13:37:47 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 13:39:30 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 244 seconds) |
| 2021-05-31 13:42:08 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 252 seconds) |
| 2021-05-31 13:42:08 | × | pe200012 quits (~pe200012@218.107.17.245) (Ping timeout: 252 seconds) |
| 2021-05-31 13:42:27 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-05-31 13:43:14 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 252 seconds) |
| 2021-05-31 13:43:18 | <tdammers> | arahael: I think you missed me by mere minutes, but I usually leave my server idling, so you can just ping me and I'll read later, most of the time. Anyway, glad you like ginger. |
| 2021-05-31 13:43:18 | → | pe200012 joins (~pe200012@218.107.17.245) |
| 2021-05-31 13:44:09 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-31 13:45:51 | <kuribas> | I think idris is more for practical programming, less for proving stuff. |
| 2021-05-31 13:46:25 | <kuribas> | At least, I tried to prove stuff in idris, and I found it not very convenient. |
| 2021-05-31 13:46:34 | <tdammers> | well yeah, that's its mission, isn't it - bring dependent types to a practical programming language. or, if you prefer, bring practical programming to a dependently typed language. |
| 2021-05-31 13:47:04 | <kuribas> | A disadvantage is that you give up on HM type inference. |
| 2021-05-31 13:47:44 | <tdammers> | Haskell doesn't do HM either |
| 2021-05-31 13:48:54 | → | lbseale joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 2021-05-31 13:51:04 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 13:51:36 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-05-31 13:51:44 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-05-31 13:51:48 | cheater1__ | is now known as cheater |
| 2021-05-31 13:54:23 | → | chaosite joins (~chaosite@user/chaosite) |
| 2021-05-31 13:55:22 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-05-31 13:55:25 | × | kiwi_33 quits (~00000000@selfhost1.threedot14.com) (Ping timeout: 268 seconds) |
| 2021-05-31 13:56:02 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 268 seconds) |
| 2021-05-31 13:59:07 | × | chaosite quits (~chaosite@user/chaosite) (Ping timeout: 268 seconds) |
| 2021-05-31 14:00:21 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds) |
| 2021-05-31 14:04:39 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 14:06:02 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) |
| 2021-05-31 14:08:19 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-05-31 14:09:17 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 14:11:17 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-05-31 14:11:42 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-05-31 14:12:45 | × | connrs quits (~connrs@s1.connrs.uk) (Changing host) |
| 2021-05-31 14:12:45 | → | connrs joins (~connrs@user/connrs) |
| 2021-05-31 14:13:48 | → | atwm joins (~andrew@178.197.235.239) |
| 2021-05-31 14:14:12 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
All times are in UTC.