Logs: liberachat/#haskell
| 2021-05-25 21:18:48 | → | nshepperd2 joins (~nshepperd@li364-218.members.linode.com) |
| 2021-05-25 21:19:04 | <starlord> | dminuoso I'm designing my own language so it's probably just what I need. I'm having a hard time implementing "extensible records with scoped labels" correctly because I don't understand the apaper |
| 2021-05-25 21:19:13 | × | integral quits (sid296274@user/integral) (Ping timeout: 272 seconds) |
| 2021-05-25 21:19:13 | × | grfn quits (sid449115@brockwell.irccloud.com) (Ping timeout: 272 seconds) |
| 2021-05-25 21:19:20 | <dminuoso> | starlord: See https://en.wikipedia.org/wiki/Natural_deduction |
| 2021-05-25 21:19:24 | → | tomsmeding_ joins (~tomsmedin@2a03:b0c0:0:1010::767:3001) |
| 2021-05-25 21:19:28 | <dminuoso> | Ah, yes. Grab TaPL definitely then. |
| 2021-05-25 21:19:41 | → | Athas_ joins (athas@2a01:7c8:aaac:1cf:f685:221c:33ac:efb6) |
| 2021-05-25 21:19:45 | → | Philonous_ joins (~Philonous@user/philonous) |
| 2021-05-25 21:19:47 | → | maerwald_ joins (~maerwald@mail.hasufell.de) |
| 2021-05-25 21:19:49 | → | brown121407 joins (~smarton@121407.xyz) |
| 2021-05-25 21:20:05 | <boxscape> | tbf contexts and typing jugdments make typing rules slightly more confusing than vanilla natural deduction |
| 2021-05-25 21:20:06 | <starlord> | oh god, natural deduction, how I wish I had this 3 months ago :D thank you, now I'll get to reading |
| 2021-05-25 21:20:23 | → | grfn joins (sid449115@id-449115.brockwell.irccloud.com) |
| 2021-05-25 21:20:27 | → | integral joins (sid296274@user/integral) |
| 2021-05-25 21:20:30 | × | liskin quits (~liskin@ackle.nomi.cz) (Ping timeout: 272 seconds) |
| 2021-05-25 21:20:41 | × | piele quits (~piele@tbonesteak.creativeserver.net) (Read error: Connection reset by peer) |
| 2021-05-25 21:20:45 | × | polux quits (~polux@51.15.169.172) (Read error: Connection reset by peer) |
| 2021-05-25 21:20:45 | × | tomsmeding quits (~tomsmedin@tomsmeding.com) (Read error: Connection reset by peer) |
| 2021-05-25 21:20:45 | × | maerwald quits (~maerwald@user/maerwald) (Read error: Connection reset by peer) |
| 2021-05-25 21:20:47 | × | lambdabot quits (~lambdabot@haskell/bot/lambdabot) (Remote host closed the connection) |
| 2021-05-25 21:20:50 | → | liskin joins (~liskin@ackle.nomi.cz) |
| 2021-05-25 21:20:55 | × | smarton quits (~smarton@121407.xyz) (Read error: Connection reset by peer) |
| 2021-05-25 21:21:07 | × | pflanze quits (~pflanze@5-168-208-80-pool.fiber.fcom.ch) (Ping timeout: 272 seconds) |
| 2021-05-25 21:21:08 | × | anoe quits (~anoe@delanoe.org) (Ping timeout: 272 seconds) |
| 2021-05-25 21:21:08 | × | df quits (~ben@51.15.198.140) (Ping timeout: 272 seconds) |
| 2021-05-25 21:21:08 | × | statusfailed quits (~statusfai@statusfailed.com) (Ping timeout: 272 seconds) |
| 2021-05-25 21:21:08 | × | Hecate quits (~mariposa@user/hecate) (Ping timeout: 272 seconds) |
| 2021-05-25 21:21:15 | → | Hecate joins (~mariposa@163.172.211.189) |
| 2021-05-25 21:21:18 | × | Morrow quits (~Morrow@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 264 seconds) |
| 2021-05-25 21:21:20 | → | df joins (~ben@51.15.198.140) |
| 2021-05-25 21:21:21 | → | anoe joins (~anoe@delanoe.org) |
| 2021-05-25 21:21:21 | → | statusfailed joins (~statusfai@statusfailed.com) |
| 2021-05-25 21:21:21 | → | piele joins (~piele@tbonesteak.creativeserver.net) |
| 2021-05-25 21:21:23 | → | illegal joins (~v@anomalous.eu) |
| 2021-05-25 21:22:12 | → | lambdabot joins (~lambdabot@silicon.int-e.eu) |
| 2021-05-25 21:22:12 | × | lambdabot quits (~lambdabot@silicon.int-e.eu) (Changing host) |
| 2021-05-25 21:22:12 | → | lambdabot joins (~lambdabot@haskell/bot/lambdabot) |
| 2021-05-25 21:22:13 | × | immae quits (~immae@static.233.10.9.176.clients.your-server.de) (Read error: Connection reset by peer) |
| 2021-05-25 21:22:14 | → | xerox_ joins (~edi@user/edi) |
| 2021-05-25 21:22:17 | <minoru_shiraeesh> | geekosaur: yes, I tried building with the default resolver but got errors and then specified the older resolver |
| 2021-05-25 21:22:19 | × | Athas quits (athas@sigkill.dk) (Read error: Connection reset by peer) |
| 2021-05-25 21:22:21 | → | immae1 joins (~immae@2a01:4f8:141:53e7::) |
| 2021-05-25 21:22:24 | × | bcoppens quits (~bartcopp@user/bcoppens) (Ping timeout: 272 seconds) |
| 2021-05-25 21:22:30 | × | xerox quits (~edi@user/edi) (Remote host closed the connection) |
| 2021-05-25 21:22:32 | × | cjay quits (cjay@nerdbox.nerd2nerd.org) (Remote host closed the connection) |
| 2021-05-25 21:22:42 | → | bcoppens joins (~bartcopp@vpn2.bartcoppens.be) |
| 2021-05-25 21:22:43 | → | cjay joins (cjay@nerdbox.nerd2nerd.org) |
| 2021-05-25 21:22:57 | × | ham2 quits (~ham4@d8D8627D5.access.telenet.be) (Quit: Leaving) |
| 2021-05-25 21:23:40 | × | Philonous quits (~Philonous@user/philonous) (Ping timeout: 272 seconds) |
| 2021-05-25 21:24:03 | × | Hecate quits (~mariposa@163.172.211.189) (Client Quit) |
| 2021-05-25 21:24:09 | → | Hecate joins (~mariposa@163.172.211.189) |
| 2021-05-25 21:24:15 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 264 seconds) |
| 2021-05-25 21:24:17 | × | V quits (~v@anomalous.eu) (Ping timeout: 272 seconds) |
| 2021-05-25 21:24:47 | → | ham joins (~ham4@user/ham) |
| 2021-05-25 21:25:12 | × | Hecate quits (~mariposa@163.172.211.189) (Changing host) |
| 2021-05-25 21:25:12 | → | Hecate joins (~mariposa@user/hecate) |
| 2021-05-25 21:26:18 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 2021-05-25 21:27:09 | <dminuoso> | boxscape: Can you explain how typing judgements make typing rules slightly more confusing? |
| 2021-05-25 21:27:16 | × | maerwald_ quits (~maerwald@mail.hasufell.de) (Changing host) |
| 2021-05-25 21:27:16 | → | maerwald_ joins (~maerwald@user/maerwald) |
| 2021-05-25 21:27:41 | maerwald_ | is now known as maerwald |
| 2021-05-25 21:27:53 | <boxscape> | dminuoso it's not once your used to them, but at the beginning I think it's just one more thing to learn, and you have to grok the fixities of :, turnstile, etc |
| 2021-05-25 21:27:59 | <boxscape> | s/your/you're |
| 2021-05-25 21:28:43 | <boxscape> | s/fixities/precedences |
| 2021-05-25 21:29:12 | → | boxscape71 joins (~boxscape@user/boxscape) |
| 2021-05-25 21:30:08 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-05-25 21:30:55 | <monochrom> | IMO natural deduction's |- is different enough from typing rules's |- such that natural deduction is a bad way to start reading typing rules. |
| 2021-05-25 21:31:24 | <monochrom> | Approximately the only commonality is the horzontal line and the comma. |
| 2021-05-25 21:31:47 | <boxscape71> | I wasn't aware of |- in natural deduction |
| 2021-05-25 21:31:59 | <monochrom> | OK, and the implcit closed-world assumption. |
| 2021-05-25 21:32:50 | <boxscape71> | Oh actually I take that back |
| 2021-05-25 21:32:52 | × | immae1 quits (~immae@2a01:4f8:141:53e7::) (Quit: WeeChat 2.9) |
| 2021-05-25 21:32:55 | <monochrom> | :) |
| 2021-05-25 21:33:15 | × | boxscape quits (~boxscape@user/boxscape) (Ping timeout: 264 seconds) |
| 2021-05-25 21:33:19 | → | immae joins (~immae@2a01:4f8:141:53e7::) |
| 2021-05-25 21:34:37 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 244 seconds) |
| 2021-05-25 21:34:39 | boxscape71 | is now known as boxscape |
| 2021-05-25 21:34:41 | × | nan` quits (~nan`@rrcs-70-60-83-42.central.biz.rr.com) (Quit: Computer is sleeping. ZZZzzz…) |
| 2021-05-25 21:35:14 | → | nan` joins (~nan`@rrcs-70-60-83-42.central.biz.rr.com) |
| 2021-05-25 21:36:18 | × | haskman quits (~haskman@171.61.140.35) (Quit: Going to sleep. ZZZzzz…) |
| 2021-05-25 21:37:03 | → | favonia joins (~favonia@user/favonia) |
| 2021-05-25 21:37:20 | → | Bartosz joins (~textual@50.35.220.89) |
| 2021-05-25 21:37:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-25 21:37:34 | × | zeenk quits (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) (Quit: Konversation terminated!) |
| 2021-05-25 21:49:38 | × | michalz quits (~user@185.246.204.58) (Remote host closed the connection) |
| 2021-05-25 21:55:25 | → | aeoui joins (~aeoui@mobile-166-171-122-171.mycingular.net) |
| 2021-05-25 21:55:47 | × | aeoui quits (~aeoui@mobile-166-171-122-171.mycingular.net) (Read error: Connection reset by peer) |
| 2021-05-25 21:56:05 | → | aeoui joins (~aeoui@ip72-194-54-201.sb.sd.cox.net) |
| 2021-05-25 21:57:54 | × | epolanski quits (uid312403@id-312403.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-05-25 22:00:19 | → | Morrow joins (~Morrow@bzq-110-168-31-106.red.bezeqint.net) |
| 2021-05-25 22:00:22 | × | ddellacosta quits (~ddellacos@89.46.62.125) (Remote host closed the connection) |
| 2021-05-25 22:00:51 | → | ddellacosta joins (~ddellacos@89.46.62.125) |
| 2021-05-25 22:02:03 | → | ruomad joins (~ruomad@82-64-17-144.subs.proxad.net) |
| 2021-05-25 22:03:27 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 272 seconds) |
| 2021-05-25 22:05:34 | × | ddellacosta quits (~ddellacos@89.46.62.125) (Ping timeout: 264 seconds) |
| 2021-05-25 22:06:20 | × | Bartosz quits (~textual@50.35.220.89) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-25 22:06:22 | × | atwm quits (~andrew@19-193-28-81.ftth.cust.kwaoo.net) (Ping timeout: 265 seconds) |
| 2021-05-25 22:06:36 | polux7 | is now known as polux |
| 2021-05-25 22:11:01 | → | horex539 joins (~horex539@2a02:a03f:6aa5:a00:445e:c460:a1c:1c80) |
All times are in UTC.