Logs on 2025-02-24 (liberachat/#haskell)
| 00:00:24 | × | malte quits (~malte@mal.tc) (Ping timeout: 272 seconds) |
| 00:01:41 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 00:02:42 | × | tnt2 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 00:07:35 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
| 00:08:34 | × | fp quits (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Remote host closed the connection) |
| 00:09:03 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 00:10:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:10:12 | → | fp joins (~Thunderbi@82-181-229-211.bb.dnainternet.fi) |
| 00:14:01 | → | malte joins (~malte@mal.tc) |
| 00:14:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 00:20:26 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 00:21:22 | × | euleritian quits (~euleritia@dynamic-176-000-004-036.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 00:21:41 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 00:23:36 | → | malte joins (~malte@mal.tc) |
| 00:25:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:25:52 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 00:31:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 00:34:25 | → | malte joins (~malte@mal.tc) |
| 00:37:19 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 00:38:00 | → | alfiee joins (~alfiee@user/alfiee) |
| 00:42:27 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 00:43:34 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:48:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 00:54:58 | × | fp quits (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Ping timeout: 252 seconds) |
| 00:56:39 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 00:57:28 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 00:57:28 | tnt2 | is now known as tnt1 |
| 00:58:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:00:22 | × | sprotte24 quits (~sprotte24@p200300d16f2727004d7c36967180880f.dip0.t-ipconnect.de) (Quit: Leaving) |
| 01:00:32 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 01:02:14 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 01:02:35 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 01:03:15 | → | malte joins (~malte@mal.tc) |
| 01:03:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:06:38 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 01:07:13 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 01:07:29 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 01:07:29 | tnt2 | is now known as tnt1 |
| 01:11:40 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 01:11:43 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 01:14:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:14:31 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 01:16:14 | × | tnt2 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 01:17:19 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 01:18:57 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 01:20:13 | → | malte joins (~malte@mal.tc) |
| 01:20:48 | × | acidjnk quits (~acidjnk@p200300d6e7283f56802bf7d29a6c8764.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 01:22:28 | × | alexherbo2 quits (~alexherbo@2a02-8440-3506-8fe9-64af-3769-8b6f-2aa7.rev.sfr.net) (Remote host closed the connection) |
| 01:23:01 | → | alexherbo2 joins (~alexherbo@2a02-8440-3506-8fe9-ac44-24f9-8cb8-0adb.rev.sfr.net) |
| 01:23:01 | × | MyNetAz quits (~MyNetAz@user/MyNetAz) (Remote host closed the connection) |
| 01:23:03 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 01:23:44 | → | alfiee joins (~alfiee@user/alfiee) |
| 01:25:24 | → | malte joins (~malte@mal.tc) |
| 01:26:33 | × | sp1ff` quits (~user@c-67-160-173-55.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 01:26:36 | × | alexherbo2 quits (~alexherbo@2a02-8440-3506-8fe9-ac44-24f9-8cb8-0adb.rev.sfr.net) (Remote host closed the connection) |
| 01:27:11 | → | todi1 joins (~todi@p57803331.dip0.t-ipconnect.de) |
| 01:27:44 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 01:28:22 | × | todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 01:29:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:30:01 | × | ft quits (~ft@mue-88-130-105-251.dsl.tropolys.de) (Ping timeout: 244 seconds) |
| 01:30:02 | → | MyNetAz joins (~MyNetAz@user/MyNetAz) |
| 01:32:01 | → | ft joins (~ft@i59F4F066.versanet.de) |
| 01:34:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:41:32 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 01:42:56 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 01:43:00 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 01:43:00 | tnt2 | is now known as tnt1 |
| 01:45:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:45:26 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 01:46:51 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 01:48:43 | → | malte joins (~malte@mal.tc) |
| 01:49:14 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 01:49:33 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 01:49:37 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 01:50:11 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 01:51:00 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 01:51:43 | → | malte joins (~malte@mal.tc) |
| 01:52:34 | → | prasad joins (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 01:54:21 | → | littlepig453 joins (~littlepig@user/littlepig453) |
| 01:57:55 | ← | littlepig453 parts (~littlepig@user/littlepig453) () |
| 02:00:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:00:51 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 02:03:32 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 02:06:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 02:06:53 | → | tavare joins (~tavare@user/tavare) |
| 02:08:50 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 02:09:28 | → | alfiee joins (~alfiee@user/alfiee) |
| 02:10:00 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 02:12:06 | × | Miroboru quits (~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 276 seconds) |
| 02:13:02 | → | Square joins (~Square@user/square) |
| 02:13:38 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 02:16:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:19:15 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 02:19:29 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 02:19:30 | tnt2 | is now known as tnt1 |
| 02:21:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:24:29 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 02:28:03 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 02:28:06 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 02:31:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:34:35 | × | Square quits (~Square@user/square) (Ping timeout: 265 seconds) |
| 02:36:24 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 02:36:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 02:38:03 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 02:40:19 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 02:40:49 | × | tnt2 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 02:46:07 | → | michalz joins (~michalz@185.246.207.218) |
| 02:49:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:52:31 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 02:52:33 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 02:53:05 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 02:53:06 | tnt2 | is now known as tnt1 |
| 02:53:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 02:55:12 | → | alfiee joins (~alfiee@user/alfiee) |
| 02:56:25 | lockywolf_ | is now known as lockywolf |
| 02:58:39 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 02:59:24 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 02:59:24 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 02:59:25 | tnt2 | is now known as tnt1 |
| 03:02:16 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 03:03:46 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 03:03:46 | tnt2 | is now known as tnt1 |
| 03:04:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:09:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 03:13:36 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 03:15:14 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 03:16:26 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 03:16:26 | → | comonad joins (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) |
| 03:17:58 | × | tnt2 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 03:20:17 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:21:33 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 03:23:06 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 03:23:06 | tnt2 | is now known as tnt1 |
| 03:24:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 03:28:14 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 03:30:11 | → | j1n37 joins (~j1n37@user/j1n37) |
| 03:32:27 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 03:33:25 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 03:34:06 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 03:34:06 | tnt2 | is now known as tnt1 |
| 03:35:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:37:22 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 03:38:40 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 03:38:40 | tnt2 | is now known as tnt1 |
| 03:40:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:40:22 | <cheater> | can someone kick tnt2/tnt1 |
| 03:40:36 | → | alfiee joins (~alfiee@user/alfiee) |
| 03:44:44 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 03:45:13 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 03:45:55 | → | ensyde joins (~ensyde@2601:5c6:c200:6dc0::a1d8) |
| 03:51:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:51:53 | → | sp1ff joins (~user@c-67-160-173-55.hsd1.wa.comcast.net) |
| 03:55:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 04:00:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:01:18 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 04:03:09 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 04:03:10 | tnt2 | is now known as tnt1 |
| 04:03:36 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 04:04:08 | → | rvalue joins (~rvalue@user/rvalue) |
| 04:06:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:10:52 | → | fp joins (~Thunderbi@82-181-229-211.bb.dnainternet.fi) |
| 04:13:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 04:13:44 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 04:14:04 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 04:14:04 | tnt2 | is now known as tnt1 |
| 04:14:35 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:19:43 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 04:20:21 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 04:20:21 | tnt2 | is now known as tnt1 |
| 04:24:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:24:42 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 04:25:04 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 04:25:16 | <Axman6> | @where ops |
| 04:25:16 | <lambdabot> | byorgey Cale conal copumpkin dcoutts dibblego dolio edwardk geekosaur glguy jmcarthur johnw mniip monochrom quicksilver shachaf shapr ski |
| 04:25:46 | <Axman6> | that's definitely an excessive amount of join/part noise. merijn was bad enough! =) |
| 04:25:48 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 04:26:20 | → | alfiee joins (~alfiee@user/alfiee) |
| 04:29:08 | × | ski quits (~ski@remote11.chalmers.se) (Ping timeout: 245 seconds) |
| 04:29:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 04:30:34 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 04:31:40 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 04:39:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:39:57 | × | k0zy quits (~user@user/k0zy) (Remote host closed the connection) |
| 04:40:37 | → | aforemny_ joins (~aforemny@2001:9e8:6cc6:4c00:6a7:4bec:d8bb:d20c) |
| 04:41:44 | × | aforemny quits (~aforemny@2001:9e8:6ce6:6d00:8593:bee7:8a90:9ac8) (Ping timeout: 260 seconds) |
| 04:44:17 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 04:55:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:59:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 05:00:36 | × | iteratee quits (~kyle@162.218.222.207) (Read error: Connection reset by peer) |
| 05:00:52 | → | iteratee joins (~kyle@162.218.222.207) |
| 05:07:53 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:10:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:12:24 | → | alfiee joins (~alfiee@user/alfiee) |
| 05:15:18 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 05:17:09 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 05:22:18 | × | fp quits (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Ping timeout: 244 seconds) |
| 05:24:38 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 05:26:00 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:30:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:31:33 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 248 seconds) |
| 05:41:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:47:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 05:52:26 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:56:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 05:58:28 | → | alfiee joins (~alfiee@user/alfiee) |
| 06:02:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 06:07:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:12:36 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 06:18:35 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 06:23:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:28:26 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 06:30:40 | × | mulk quits (~mulk@p5b2dc995.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 06:34:14 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 06:39:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:40:21 | × | saolsen quits (sid26430@id-26430.lymington.irccloud.com) (Ping timeout: 248 seconds) |
| 06:43:34 | → | saolsen joins (sid26430@id-26430.lymington.irccloud.com) |
| 06:43:52 | → | alfiee joins (~alfiee@user/alfiee) |
| 06:44:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 06:46:29 | → | alp joins (~alp@2001:861:8ca0:4940:5005:690c:e28e:7765) |
| 06:48:17 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 06:54:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:57:57 | × | Ranhir quits (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 06:59:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 07:03:55 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 07:09:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:13:12 | → | CiaoSen joins (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) |
| 07:14:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 07:19:57 | → | ski joins (~ski@remote11.chalmers.se) |
| 07:25:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:29:15 | → | alfiee joins (~alfiee@user/alfiee) |
| 07:32:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 07:33:28 | <energizer> | where can i find the implementation of `instance Monad List` ? |
| 07:33:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 07:37:43 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 07:43:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:46:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:47:50 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 07:51:02 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:52:24 | <kaol> | energizer: https://hackage.haskell.org/package/ghc-internal-9.1201.0/docs/src/GHC.Internal.Base.html#line-1751 |
| 07:53:39 | <kaol> | In as much as regular lists in Haskell use the [] notation. If you had some other List in mind then I don't know. |
| 07:54:21 | <energizer> | kaol: what does "xs >>= f = [y | x <- xs, y <- f x]" desugar to? |
| 07:56:16 | <Leary> | @undo xs >>= f = [y | x <- xs, y <- f x] |
| 07:56:16 | <lambdabot> | xs >>= f = concatMap (\ x -> concatMap (\ y -> [y]) (f x)) xs |
| 08:00:02 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 08:00:39 | → | mulk joins (~mulk@p5b112753.dip0.t-ipconnect.de) |
| 08:01:40 | → | caconym joins (~caconym@user/caconym) |
| 08:02:33 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 08:10:43 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 08:12:32 | × | ash3en quits (~Thunderbi@89.246.174.164) (Client Quit) |
| 08:14:39 | → | alfiee joins (~alfiee@user/alfiee) |
| 08:17:32 | <Leary> | energizer: There's a redundant `concatMap` in the `undo` output above, but either GHC's actual desugaring is better or optimisation tidies it up; the core amounts to: `xs >>= f = go xs where go = \case{ [] -> []; y:ys -> f y ++ go ys }`. |
| 08:17:55 | → | misterfish joins (~misterfis@84.53.85.146) |
| 08:18:59 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 08:20:43 | → | acidjnk joins (~acidjnk@p200300d6e7283f50b85661171ead7665.dip0.t-ipconnect.de) |
| 08:22:12 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 08:27:44 | × | ash3en quits (~Thunderbi@89.246.174.164) (Remote host closed the connection) |
| 08:32:35 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:38:10 | → | Miroboru joins (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 08:40:45 | → | harveypwca joins (~harveypwc@2601:246:d080:f6e0:34b5:bbb2:c6c:1ef6) |
| 08:46:51 | → | merijn joins (~merijn@77.242.116.146) |
| 08:49:37 | × | ft quits (~ft@i59F4F066.versanet.de) (Quit: leaving) |
| 08:53:07 | ← | f-a parts (ff2a@joined.irc.for-some.fun) () |
| 08:53:12 | <tomsmeding> | Athas: re multi-dimensional arrays: do you really think so? What people often struggle with is that if you have a function a -> b in Accelerate, you can't just `map` it to a `[]a -> []b`. Now this is strictly speaking not directly implied by having multi-dimensional arrays, but it is rather central to the model |
| 08:53:23 | <tomsmeding> | Good to hear that some people feel differently :p |
| 08:53:57 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 08:54:59 | × | Miroboru quits (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 08:56:11 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 08:59:09 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 268 seconds) |
| 09:00:23 | → | alfiee joins (~alfiee@user/alfiee) |
| 09:04:50 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 09:04:50 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 09:04:57 | <ski> | @src (>>=) [] |
| 09:04:57 | <lambdabot> | Source not found. Take a stress pill and think things over. |
| 09:05:01 | → | merijn joins (~merijn@77.242.116.146) |
| 09:05:01 | <ski> | @src [] (>>=) |
| 09:05:01 | <lambdabot> | xs >>= f = concatMap f xs |
| 09:05:05 | <ski> | @src [] return |
| 09:05:05 | <lambdabot> | return x = [x] |
| 09:05:20 | → | euleritian joins (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) |
| 09:10:13 | × | sa quits (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 248 seconds) |
| 09:11:55 | × | unlucy quits (sid572875@user/unlucy) (Ping timeout: 244 seconds) |
| 09:13:49 | → | sa joins (sid1055@id-1055.tinside.irccloud.com) |
| 09:14:27 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:15:41 | → | unlucy joins (sid572875@user/unlucy) |
| 09:16:48 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 09:18:46 | → | chele joins (~chele@user/chele) |
| 09:27:56 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 09:30:34 | → | merijn joins (~merijn@77.242.116.146) |
| 09:31:47 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 09:32:57 | <Athas> | tomsmeding: but on the other hand, you can efficiently and sanely express multi-dimensional things. |
| 09:35:32 | × | acidjnk quits (~acidjnk@p200300d6e7283f50b85661171ead7665.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 09:35:49 | <tomsmeding> | Athas: that's true |
| 09:36:25 | <tomsmeding> | perhaps difficulty with Accelerate's model is also engendered a bit by the typing of the embedded language |
| 09:36:44 | → | __monty__ joins (~toonn@user/toonn) |
| 09:37:00 | <tomsmeding> | that is to say, if Accelerate had a bespoke syntax with syntax for types that encouraged rank polymorphism, perhaps people would have less problems with it |
| 09:39:26 | → | acidjnk joins (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) |
| 09:40:29 | <Athas> | I got started on porting your GMM implementation to 'vector', but it is really tedious. |
| 09:40:39 | <Athas> | I may just end up with vectors-of-vectors, even though it's not very efficient. |
| 09:41:01 | <tomsmeding> | ah, that's how you got into this. :) |
| 09:41:25 | <tomsmeding> | you could always roll your own 2-dimensional array with manual divMod indexing |
| 09:42:11 | <Athas> | I suppose. I really don't want to be in the business of building abstractions, however. |
| 09:42:40 | → | zmt01 joins (~zmt00@user/zmt00) |
| 09:46:27 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 276 seconds) |
| 09:46:46 | → | alfiee joins (~alfiee@user/alfiee) |
| 09:48:33 | × | harveypwca quits (~harveypwc@2601:246:d080:f6e0:34b5:bbb2:c6c:1ef6) (Quit: Leaving) |
| 09:50:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 09:51:29 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 09:51:36 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.1) |
| 09:53:27 | → | fp joins (~Thunderbi@130.233.70.89) |
| 10:01:59 | → | merijn joins (~merijn@77.242.116.146) |
| 10:12:47 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 10:13:19 | → | rvalue joins (~rvalue@user/rvalue) |
| 10:16:44 | → | kuribas joins (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) |
| 10:22:32 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 10:32:31 | → | alfiee joins (~alfiee@user/alfiee) |
| 10:36:52 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 10:38:28 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 10:38:32 | × | ash3en quits (~Thunderbi@89.246.174.164) (Remote host closed the connection) |
| 10:42:50 | × | euleritian quits (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:43:57 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 10:44:18 | → | euouae joins (~euouae@user/euouae) |
| 10:44:40 | <euouae> | Hello I've been thinking about statements such as 'monads are just ... in the category of endofunctors' (fill in blank for me because I don't know it exactly) |
| 10:45:17 | <euouae> | From my studies on type theory, e.g. the lambda cube, I can't seem to figure out how type theory (theories) is formalized on category theory. I'm not sure if it is known or not. |
| 10:46:14 | <euouae> | I vaguely have heard of something about cartesian-closed categories, but I'm not sure if they capture all the salient points. What is the idea then? How are functors to be understood in type theory if there is no categorical formulation of it? Or am I missing something? |
| 10:48:57 | × | acidjnk quits (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 10:49:33 | <ncf> | i don't understand the question but see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory |
| 10:54:31 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 10:55:12 | → | euleritian joins (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) |
| 10:55:45 | <jackdk> | I wouldn't worry about the meme words (but for completeness, the `...` is "monoid objects", and you need to specify the tensor; see https://www.youtube.com/watch?v=cB8DapKQz-I ) . I don't know the details, but you can represent lambda calculus terms in CCCs; see Conal Eliott's excellent work on "compiling to categories" at e.g. https://www.youtube.com/watch?v=4WMfKhKKVN4 https://www.youtube.com/watch?v=zooYfk5-yPY |
| 10:56:12 | × | euleritian quits (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:56:29 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 10:56:40 | <euouae> | ncf: when that link says categories provide the semantics, does it mean that categories are models for type theories? |
| 10:57:37 | <euouae> | I mean *those certain* categories that are specified |
| 10:57:52 | → | fp1 joins (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) |
| 10:58:41 | <ncf> | yes |
| 10:59:33 | <euouae> | I see. What is meant by dependent type theory? This is another naive question. I know what a dependent type is vaguely, but I don't think there's a single "theory", that's why I'm asking |
| 10:59:42 | <euouae> | e.g. the lambda cube has several, not just CoC at the top |
| 11:00:01 | <ncf> | nlab usually means martin-löf type theory |
| 11:00:14 | <euouae> | and is that a single theory or multiple? |
| 11:00:19 | × | fp quits (~Thunderbi@130.233.70.89) (Ping timeout: 260 seconds) |
| 11:00:20 | fp1 | is now known as fp |
| 11:02:45 | <ncf> | multiple; there are several choices you can make and features you can add |
| 11:02:56 | <euouae> | Then how come they all have the same CCC models? |
| 11:03:02 | <euouae> | is it like a common core? |
| 11:05:36 | <ncf> | they don't |
| 11:06:21 | <ncf> | every model of MLTT is a locally cartesian closed category because that's the structure you need to interpret the basic features of a type theory; but the models may also have more structure to account for the other features |
| 11:07:43 | <euouae> | Does MLTT have sorts of order N? Or just 2? |
| 11:08:11 | <euouae> | I know for the lambda cube only two sorts are used, types and kinds, say |
| 11:08:27 | <euouae> | I don't quite grasp the significance of that. also last question I promise. thank you |
| 11:08:49 | <euouae> | jackdk: thanks for the links, I will check them out. I can at least say I've seen the diagram of the first video before |
| 11:09:51 | × | ethantwardy quits (user@user/ethantwardy) (Ping timeout: 246 seconds) |
| 11:10:45 | × | CiaoSen quits (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) (Ping timeout: 248 seconds) |
| 11:13:03 | <ncf> | euouae: i think that might depend on how you present the syntax and what you mean by "order". i don't think the answer is very significant |
| 11:13:34 | <euouae> | I'm doing personal "research" so there's no fixed order/set of papers/articles I'm reading |
| 11:13:51 | <ncf> | or do you mean universe levels? this is one of the choices you can make; you can have a MLTT with no universes, or one universe, or a countable hierarchy of universes, or crazier things |
| 11:13:57 | <euouae> | but e.g. in the HoTT book in the Appendix the type universes are presented as U_1, U_2, ... and I think those are types, kinds, higher kinds, etc |
| 11:14:08 | <ncf> | right the hott book uses a countable hierarchy |
| 11:14:18 | <euouae> | what is the significance of those? |
| 11:14:52 | <euouae> | It seems that both Haskell and Coq stop at 2, types and kinds, and it's good enough, especially in Coq you can formalize a ton of Math |
| 11:15:35 | <euouae> | Haskell having the deficiency that you can't directly play with kinds like you do with types, which is all I can say, I can't put it more succinctly, I need to study more |
| 11:15:36 | <ncf> | coq also has a countable hierarchy Type i |
| 11:15:59 | <ncf> | you need such a thing if you want every type to have a type, since Type : Type is inconsistent |
| 11:16:29 | <ncf> | type theory is best learned by forgetting about haskell |
| 11:16:46 | <ncf> | "kind" isn't really a thing separate from type; it is in haskell because it has type erasure |
| 11:18:35 | → | alfiee joins (~alfiee@user/alfiee) |
| 11:18:53 | → | random-jellyfish joins (~developer@user/random-jellyfish) |
| 11:19:43 | <euouae> | Wait, so Coq has N type universes? I thought the top of the lambda cube is CoC and Barendregt's paper says it only needs types and kinds |
| 11:19:52 | <euouae> | and I thought the calculus of constructions is what Coq uses |
| 11:20:14 | <ski> | euouae : "Categorical Logic and Type Theory" by Bart Jacobs in 1999 (<https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html>,TOC <https://www.gbv.de/dms/ilmenau/toc/119524279.PDF>) talks about using "fibrations" in category theory to express dependent type theory, categorically |
| 11:20:18 | <euouae> | type theory is dizzying. so many different theories |
| 11:21:19 | <euouae> | ski is that the right TOC? |
| 11:22:23 | <ski> | er .. no, sorry |
| 11:22:41 | <ski> | i was simultaneously looking up "Elementary Categories, Elementary Toposes" by Colin McLarty, which talks a bit about categorical logic, and internal language in a cartesian closed category |
| 11:23:07 | <euouae> | so when you're saying to experss dtt, do you mean that fibrations are used to formalize type theory in category theory? because that sounds different from having categories provide the semantics |
| 11:23:16 | <ncf> | i have found that the lambda cube is 1. what most people trying to learn type theory end up looking at because of wikipedia and 2. not a very useful thing to think about and not something type theorists ever talk about |
| 11:23:18 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 276 seconds) |
| 11:23:57 | <ski> | (but if you want to look more into toposes, which doesn't exactly deal with type theory, more plain logic from a categorical perspective, i'd suggest starting with "Conceptual Mathematics: a first introduction to categories" by William F. Lawvere,Stephen Schanuel, first) |
| 11:25:19 | <euouae> | More down to earth, ncf, how should I learn some type theory? |
| 11:25:42 | <euouae> | I am confident with deeper math, but I don't know what to look at |
| 11:25:48 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:26:23 | <euouae> | I came across the lambda cube from some reddit post, it stayed with me (marketing? lambda cube ... cool name, there's a picture of a cube) |
| 11:30:10 | <ncf> | tough question. i think the hott book is actually a decent introduction but not everyone might agree |
| 11:30:34 | <ncf> | these lecture notes are also very nicely written https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf |
| 11:34:25 | → | j1n37- joins (~j1n37@user/j1n37) |
| 11:34:49 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 11:37:13 | <euouae> | got it, I will look into those two then. thanks everyone! |
| 11:40:33 | <ncf> | euouae: to answer an earlier question, coq's type theory is *based* on CC but also extends it with many features. i think a better approximation is what people call "CICω", which is a pure type system with a hierarchy of ω sorts |
| 11:41:03 | <ncf> | (the I stands for Inductive) |
| 11:44:11 | → | jespada joins (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) |
| 11:46:10 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 11:46:12 | <euouae> | thank you! |
| 11:46:39 | × | euouae quits (~euouae@user/euouae) () |
| 11:47:18 | × | jespada quits (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Client Quit) |
| 11:49:19 | → | merijn joins (~merijn@77.242.116.146) |
| 11:50:49 | → | nwoob joins (~nikhilkau@user/nwoob) |
| 11:50:59 | ← | nwoob parts (~nikhilkau@user/nwoob) () |
| 11:51:43 | → | nwoob joins (~nikhilkau@user/nwoob) |
| 11:53:41 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Remote host closed the connection) |
| 11:57:45 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 12:01:02 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 12:04:14 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 12:04:18 | × | ash3en quits (~Thunderbi@89.246.174.164) (Client Quit) |
| 12:07:03 | → | alfiee joins (~alfiee@user/alfiee) |
| 12:07:09 | → | ethantwardy joins (user@user/ethantwardy) |
| 12:09:49 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 12:11:33 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 12:16:50 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 12:18:49 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 12:19:09 | → | jespada joins (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) |
| 12:19:28 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 12:23:08 | → | merijn joins (~merijn@77.242.116.146) |
| 12:37:52 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 12:39:13 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 12:41:36 | → | cheater_ joins (~Username@user/cheater) |
| 12:43:24 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 12:43:45 | × | cheater quits (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 12:43:51 | cheater_ | is now known as cheater |
| 12:44:20 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 12:51:07 | → | alexherbo2 joins (~alexherbo@2a02-8440-3503-a0c2-8daf-d920-c5db-5fe6.rev.sfr.net) |
| 12:53:08 | → | alfiee joins (~alfiee@user/alfiee) |
| 12:54:00 | × | fp quits (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) (Ping timeout: 252 seconds) |
| 12:56:28 | × | tv quits (~tv@user/tv) (Quit: derp) |
| 12:56:53 | → | tv joins (~tv@user/tv) |
| 12:57:29 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 12:59:59 | → | acidjnk joins (~acidjnk@p200300d6e7283f50c93f98c64cfbe971.dip0.t-ipconnect.de) |
| 13:00:57 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 13:01:15 | → | euleritian joins (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) |
| 13:04:33 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 13:04:52 | → | Square2 joins (~Square4@user/square) |
| 13:06:20 | → | CiaoSen joins (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) |
| 13:09:15 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 276 seconds) |
| 13:13:17 | → | Googulator joins (~Googulato@2a01:36d:106:c81:ad7c:ac56:196b:c9a2) |
| 13:14:10 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:17:01 | <spew> | ncf: those notes look really good, thank you for sharing |
| 13:28:25 | <ncf> | @tell euouae relevant discussion thread: https://mathstodon.xyz/@jadkoleilat/113553981368332306 |
| 13:28:25 | <lambdabot> | Consider it noted. |
| 13:39:12 | → | alfiee joins (~alfiee@user/alfiee) |
| 13:40:08 | → | ash3en joins (~Thunderbi@89.246.174.164) |
| 13:43:28 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 13:45:50 | × | pabs3 quits (~pabs3@user/pabs3) (Remote host closed the connection) |
| 13:46:52 | → | pabs3 joins (~pabs3@user/pabs3) |
| 13:49:52 | → | weary-traveler joins (~user@user/user363627) |
| 13:52:53 | × | nwoob quits (~nikhilkau@user/nwoob) (Ping timeout: 245 seconds) |
| 13:53:26 | <__monty__> | Isn't TAPL *the* introduction to type theory? |
| 13:55:52 | × | ash3en quits (~Thunderbi@89.246.174.164) (Ping timeout: 244 seconds) |
| 13:57:05 | → | zungi joins (~tory@user/andrewchawk) |
| 13:59:14 | <ncf> | looks more geared towards programmers |
| 13:59:22 | <leah2> | and implementors |
| 14:04:27 | → | fp joins (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) |
| 14:05:29 | × | acidjnk quits (~acidjnk@p200300d6e7283f50c93f98c64cfbe971.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 14:08:20 | → | fp1 joins (~Thunderbi@2001:708:20:1406::1370) |
| 14:09:00 | × | fp quits (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) (Ping timeout: 244 seconds) |
| 14:09:01 | fp1 | is now known as fp |
| 14:15:01 | × | hellwolf quits (~user@b1d5-60a7-bc53-7e05-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 252 seconds) |
| 14:20:52 | → | hellwolf joins (~user@ff62-a6a0-5031-3fa8-0f00-4d40-07d0-2001.sta.estpak.ee) |
| 14:24:56 | → | alfiee joins (~alfiee@user/alfiee) |
| 14:25:26 | → | acidjnk joins (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) |
| 14:29:19 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 14:30:14 | → | ft joins (~ft@p4fc2a610.dip0.t-ipconnect.de) |
| 14:34:24 | × | jespada quits (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 14:34:52 | → | jespada joins (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) |
| 14:38:06 | × | alp quits (~alp@2001:861:8ca0:4940:5005:690c:e28e:7765) (Ping timeout: 246 seconds) |
| 14:39:29 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 14:39:46 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 14:46:26 | → | YaShhhh joins (~YaShhhh@103.199.191.65) |
| 14:47:02 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 14:47:28 | × | CiaoSen quits (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) (Ping timeout: 245 seconds) |
| 14:47:56 | × | YaShhhh quits (~YaShhhh@103.199.191.65) (Client Quit) |
| 14:48:18 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 245 seconds) |
| 14:48:19 | tnt2 | is now known as tnt1 |
| 14:50:13 | × | ensyde quits (~ensyde@2601:5c6:c200:6dc0::a1d8) (Ping timeout: 252 seconds) |
| 14:53:45 | <ski> | __monty__ : more like intro to type systems |
| 14:55:35 | <ski> | i commonly point people first to "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~amoeller/mis/typeinf.p(s|df)>, though |
| 14:57:24 | → | bitterx joins (~bitterx@APN-122-12-44-gprs.simobil.net) |
| 14:58:21 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 15:00:48 | × | tnt1 quits (~Thunderbi@user/tnt1) (Quit: tnt1) |
| 15:11:00 | → | alfiee joins (~alfiee@user/alfiee) |
| 15:14:42 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 15:15:08 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 15:19:31 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 15:19:54 | × | Teacup quits (~teacup@user/teacup) () |
| 15:20:01 | → | rvalue joins (~rvalue@user/rvalue) |
| 15:20:19 | → | Teacup joins (~teacup@user/teacup) |
| 15:27:28 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 15:27:37 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Quit: leaving) |
| 15:27:54 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 15:28:24 | × | euleritian quits (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:28:42 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 15:36:32 | × | turlando quits (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 15:37:48 | → | turlando joins (~turlando@user/turlando) |
| 15:37:55 | <monochrom> | TAPL is type systems, not type theory. |
| 15:38:21 | <monochrom> | The name "type theory" comes from "set theory" and s/set/type/ |
| 15:39:10 | <ncf> | yeah |
| 15:43:17 | → | slack1256 joins (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) |
| 15:43:18 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 276 seconds) |
| 15:43:45 | <dolio> | FYI, CIC is no longer really a 'pure type system.' |
| 15:44:04 | <slack1256> | There is no effectful channel, so... What do you guys use for EarlyReturn? I know that Error (checked exceptions) can be used like that, but maybe there is a more ergonomic way? |
| 15:44:05 | <dolio> | The 'inductive' part takes it out of that realm. |
| 15:45:03 | <ncf> | oh yeah |
| 15:45:13 | <ncf> | should have said based on a pure type system |
| 15:48:30 | × | jespada quits (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 15:50:39 | → | nwoob joins (~nikhilkau@165.225.120.224) |
| 15:51:49 | × | fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 260 seconds) |
| 15:53:36 | <dolio> | I guess this is a bit ironic, but pure type systems kind of don't work very well for situations beyond the original lambda cube. |
| 15:54:18 | × | nwoob quits (~nikhilkau@165.225.120.224) (Read error: Connection reset by peer) |
| 15:54:40 | <dolio> | Like, if you want more universes, and to remain consistent, you need predicative sorts. But you can't really encode inductives with predicativity. |
| 15:56:23 | → | alfiee joins (~alfiee@user/alfiee) |
| 15:59:49 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 16:00:38 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 16:01:56 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 244 seconds) |
| 16:04:36 | → | Wygulmage joins (~Wygulmage@user/Wygulmage) |
| 16:08:09 | × | slack1256 quits (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) (Ping timeout: 260 seconds) |
| 16:08:18 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 16:08:49 | → | slack1256 joins (~slack1256@2803:c600:5111:952f:8534:d540:7202:b800) |
| 16:09:23 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 16:14:56 | → | merijn joins (~merijn@77.242.116.146) |
| 16:15:28 | → | kritzefitz joins (~kritzefit@debian/kritzefitz) |
| 16:18:25 | × | Digit quits (~user@user/digit) (Ping timeout: 248 seconds) |
| 16:18:49 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 16:20:50 | × | bitterx quits (~bitterx@APN-122-12-44-gprs.simobil.net) (Quit: bitterx) |
| 16:21:04 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 16:21:22 | <EvanR> | slack1256, Maybe's monad instance cancels the computation early with no result. Such and similar behavior can be built into your Big App monad if you have one. Or you can do it directly by opting to "return" Nothing for whatever branch of the computation |
| 16:22:35 | × | tromp quits (~textual@2a02:a210:cba:8500:e9b1:7587:9c27:25c9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:22:36 | <EvanR> | libraries based on an monadic DSL often have it built in, e.g. Parser monads return early as a matter of course (parse failure) |
| 16:26:38 | → | merijn joins (~merijn@77.242.116.146) |
| 16:28:05 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 16:33:30 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 16:35:48 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 16:38:04 | × | acidjnk quits (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 16:42:27 | → | alfiee joins (~alfiee@user/alfiee) |
| 16:44:18 | → | tromp joins (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) |
| 16:44:31 | → | alp joins (~alp@2001:861:8ca0:4940:4960:283e:5e01:3e7b) |
| 16:46:50 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 16:55:13 | → | acidjnk joins (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) |
| 16:58:18 | × | paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 268 seconds) |
| 16:58:53 | → | jespada joins (~jespada@r167-61-39-77.dialup.adsl.anteldata.net.uy) |
| 17:02:55 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:03:27 | × | alexherbo2 quits (~alexherbo@2a02-8440-3503-a0c2-8daf-d920-c5db-5fe6.rev.sfr.net) (Remote host closed the connection) |
| 17:08:44 | → | paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt) |
| 17:15:04 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 17:18:39 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 17:19:13 | → | euleritian joins (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) |
| 17:25:43 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 17:28:31 | → | alfiee joins (~alfiee@user/alfiee) |
| 17:32:37 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 17:33:41 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 17:33:56 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:34:30 | × | euleritian quits (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 17:35:32 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:38:24 | × | comonad quits (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) (Quit: WeeChat 4.5.2) |
| 17:39:49 | → | euleritian joins (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) |
| 17:39:52 | → | comonad joins (~comonad@pd9e07a19.dip0.t-ipconnect.de) |
| 17:44:02 | × | euleritian quits (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 17:50:09 | → | rherardi joins (~rherardi@user/rherardi) |
| 17:50:48 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 17:51:05 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:51:40 | → | Digit joins (~user@user/digit) |
| 17:52:39 | → | misterfish joins (~misterfis@84.53.85.146) |
| 17:55:56 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 17:57:48 | × | j1n37- quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 17:58:01 | → | Square joins (~Square@user/square) |
| 17:59:59 | × | tv quits (~tv@user/tv) (Quit: derp) |
| 18:00:14 | → | tv joins (~tv@user/tv) |
| 18:00:45 | <kuribas> | Big App monad = anti pattern |
| 18:01:19 | → | j1n37 joins (~j1n37@user/j1n37) |
| 18:03:18 | × | sa quits (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 18:03:19 | × | tritlo quits (sid58727@id-58727.hampstead.irccloud.com) (Ping timeout: 245 seconds) |
| 18:03:36 | → | tritlo joins (sid58727@id-58727.hampstead.irccloud.com) |
| 18:04:02 | × | Pent quits (sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 265 seconds) |
| 18:04:33 | × | tapas quits (sid467876@id-467876.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 18:04:34 | × | Square2 quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 18:05:00 | × | cbarrett quits (sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 265 seconds) |
| 18:05:23 | × | JSharp quits (sid4580@user/JSharp) (Ping timeout: 245 seconds) |
| 18:05:23 | × | gmc quits (sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 18:06:27 | × | mustafa quits (sid502723@rockylinux/releng/mustafa) (Ping timeout: 265 seconds) |
| 18:06:48 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:07:33 | → | sa joins (sid1055@id-1055.tinside.irccloud.com) |
| 18:07:43 | → | cbarrett joins (sid192934@id-192934.helmsley.irccloud.com) |
| 18:07:43 | × | tv quits (~tv@user/tv) (Quit: derp) |
| 18:07:47 | → | tapas joins (sid467876@id-467876.ilkley.irccloud.com) |
| 18:07:56 | → | tv joins (~tv@user/tv) |
| 18:07:59 | → | Pent joins (sid313808@id-313808.lymington.irccloud.com) |
| 18:08:08 | → | gmc joins (sid58314@id-58314.ilkley.irccloud.com) |
| 18:09:26 | → | mustafa joins (sid502723@rockylinux/releng/mustafa) |
| 18:11:32 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 18:11:37 | → | JSharp joins (sid4580@user/JSharp) |
| 18:13:39 | <haskellbridge> | <Bowuigi> dolio yeah Barendegt's PTSs don't have much power in terms of common theorem proving. Technically there's a way to regain that power but it requires fancy features, either the ones in CDLE/Cedille or that one encoding method I found on a random thesis and I can't find again |
| 18:14:15 | → | alfiee joins (~alfiee@user/alfiee) |
| 18:14:44 | × | rherardi quits (~rherardi@user/rherardi) (Ping timeout: 260 seconds) |
| 18:15:14 | <dolio> | Well, cedille solves the fact that you can't really encode inductive things at all, from the type theory end. |
| 18:15:55 | <mauke> | I should invent a language called Ç |
| 18:15:57 | <dolio> | But I don't think it'd solve the predicativity part. |
| 18:18:11 | <EvanR> | Ç plus plus (must be pronounced french) |
| 18:18:18 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 18:19:14 | <dolio> | The problem with predicativity is that encodings quantify over all the types that you're allowed to do recursion into, but then you're bigger than any of the things you can recurse into, and you can't recurse into anything bigger than what you picked. |
| 18:20:36 | <dolio> | So they don't even have the proper ability to do recursive stuff in general. |
| 18:22:36 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:24:27 | × | comonad quits (~comonad@pd9e07a19.dip0.t-ipconnect.de) (Quit: WeeChat 4.6.0-dev) |
| 18:24:46 | → | comonad joins (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) |
| 18:24:58 | <dolio> | E.G. a predicative version of System F can't do pentation. |
| 18:26:47 | <EvanR> | had to look this one up, pentation is repeated tetration |
| 18:26:58 | <dolio> | Yeah. |
| 18:27:20 | <EvanR> | system F can do tetration but not pentation, wtf |
| 18:27:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 18:27:35 | <EvanR> | does it had a hardcoded limit=4 somewhere |
| 18:30:22 | → | rherardi joins (~rherardi@user/rherardi) |
| 18:32:36 | ← | rherardi parts (~rherardi@user/rherardi) (Leaving...) |
| 18:35:00 | JuanDaugherty | is now known as ColinRobinson |
| 18:38:23 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:39:35 | → | euleritian joins (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) |
| 18:40:21 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:45:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 18:45:33 | <dolio> | No, System F can define any function provably total in second order arithmetic. But if you remove the impredicativity, and replace it with ω-many universes, you can only define tetration. |
| 18:46:44 | <dolio> | Or, anything in Grzegorczyk's class ε₄, which pentation isn't. |
| 18:47:43 | <EvanR> | 🤯 |
| 18:52:10 | <dolio> | The 'reason' is basically that exponentiation is the last hyper operation that can easily be defined by just instantiating numerals with the result type. You instantiate one to `r` and one to `r -> r` or something. So, with infinitely many predicative sorts, you only get one 'level' beyond exponentiation. |
| 18:52:58 | <dolio> | And you need to switch to using, like, a numeral, and a numeral on numerals. |
| 18:56:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:56:30 | <[exa]> | no. of places where I heard about grzegorczyk's hierarchy: happily increases |
| 18:59:08 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 19:00:39 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:01:06 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 19:02:44 | <dolio> | I guess a more detailed explanation is that since exponentiation involves instantiating one numeral to `r -> r`, when you want to do tetration, one of the numbers determines how many nestings of that instantiation you need to do, which isn't possible except by operating on numerals. |
| 19:03:05 | <dolio> | But operating on numerals requires a bigger numeral type in a predicative setting. |
| 19:03:40 | → | sprotte24 joins (~sprotte24@p200300d16f3063004006d4006bd9f81a.dip0.t-ipconnect.de) |
| 19:04:27 | <dolio> | And then you can't do pentation because that requires iterating tetration, which requires one of the numers to determine how many sizes you need, and there's no way to get an adaptive number of sizes unless you add a transfinite universe or something. |
| 19:04:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 19:05:40 | <dolio> | Which you can do. If you have a 'top' universe above all the finite numbered universes, you can use a numeral on the top universe to do pentation. |
| 19:11:41 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 19:12:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:14:14 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:14:39 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:15:27 | <EvanR> | and what are the consequences of the top universe |
| 19:17:10 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:17:37 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 19:18:28 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 19:20:05 | × | plitter quits (~plitter@user/plitter) (Ping timeout: 252 seconds) |
| 19:21:54 | → | plitter joins (~plitter@user/plitter) |
| 19:27:15 | <haskellbridge> | <Bowuigi> EvanR Well, it depends on the kind of top universe, if it is truly the top, it must have type in type or similar. If it isn't, then it belongs to an inaccessible universe. I think it would be sound in the second case (not on the first tho) |
| 19:28:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:28:10 | <haskellbridge> | <Bowuigi> Agda has a hierarchy of top universes, but you can't use level polymorphism on them |
| 19:28:18 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 19:33:23 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 19:33:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 19:36:05 | <EvanR> | Agda = U1, U2, U3, ... U_top1, U_top2, Utop3, ... |
| 19:38:59 | → | pavonia joins (~user@user/siracusa) |
| 19:40:04 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 260 seconds) |
| 19:42:00 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 19:43:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:46:03 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:47:09 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds) |
| 19:48:48 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:50:30 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:50:31 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 19:51:32 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:52:58 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 272 seconds) |
| 19:58:00 | <ncf> | impredicative encodings are just so weird |
| 19:58:24 | × | zungi quits (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 19:59:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:00:02 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 20:00:45 | → | caconym joins (~caconym@user/caconym) |
| 20:04:46 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:07:27 | → | euphores joins (~SASL_euph@user/euphores) |
| 20:08:47 | → | peterbecich1 joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 20:10:43 | × | kuribas quits (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) (Remote host closed the connection) |
| 20:11:05 | peterbecich1 | is now known as peterbecich |
| 20:12:10 | → | weary-traveler joins (~user@user/user363627) |
| 20:12:33 | × | michalz quits (~michalz@185.246.207.218) (Remote host closed the connection) |
| 20:13:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:18:42 | × | hgolden quits (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 20:19:33 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 20:20:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 20:21:17 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) |
| 20:24:13 | × | euleritian quits (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 20:24:35 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 20:25:39 | × | ThePenguin quits (~ThePengui@cust-95-80-24-166.csbnet.se) (Quit: Ping timeout (120 seconds)) |
| 20:26:29 | → | ThePenguin joins (~ThePengui@cust-95-80-24-166.csbnet.se) |
| 20:31:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:32:07 | → | alfiee joins (~alfiee@user/alfiee) |
| 20:35:29 | × | byte quits (~mu@user/byte) (Ping timeout: 260 seconds) |
| 20:36:17 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 20:36:22 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 20:37:41 | → | byte joins (~mu@user/byte) |
| 20:42:01 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 20:42:44 | → | gmg joins (~user@user/gehmehgeh) |
| 20:47:08 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:48:21 | → | zungi joins (~tory@user/andrewchawk) |
| 20:51:29 | → | hsw_ joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 20:51:47 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:52:32 | × | hsw quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 20:52:52 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 20:58:00 | × | jespada quits (~jespada@r167-61-39-77.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 21:02:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:04:43 | → | j1n37- joins (~j1n37@user/j1n37) |
| 21:05:35 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 21:07:53 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:13:27 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 21:14:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:14:44 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 21:18:51 | → | alfiee joins (~alfiee@user/alfiee) |
| 21:19:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 21:19:13 | → | Square2 joins (~Square4@user/square) |
| 21:19:32 | <haskellbridge> | <Bowuigi> They are, but Category Theory makes them make sense I guess |
| 21:20:22 | <haskellbridge> | <Bowuigi> Hinze's Generic Programming with Adjunctions illustrates this perspective quite well, with more advanced examples found in the HoTT blog |
| 21:21:50 | × | Square quits (~Square@user/square) (Ping timeout: 252 seconds) |
| 21:21:55 | <ncf> | category theory makes normal inductive types make even more sense |
| 21:22:51 | <ncf> | i know you can make sense of impredicative encodings via abstract nonsense like "if Set is impredicative then the category of sets is large-complete so the limit of the identity functor gives an initial algebra for every functor" but like... that's what i mean by weird |
| 21:23:39 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 21:25:41 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 21:27:45 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 21:30:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:34:45 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 21:35:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:37:59 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 21:38:46 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 21:40:33 | <EvanR> | what does "Set is impredicative" mean |
| 21:45:16 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 21:45:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:47:03 | <lyxia> | it means that types of the form "forall A : Set..." are not sets. Sets cannot contain elements that quantify over the universe of sets. |
| 21:47:22 | <ncf> | well it means the negation of that |
| 21:47:36 | <lyxia> | oh haha |
| 21:48:48 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 21:49:41 | <EvanR> | ok unnegate it please |
| 21:50:21 | × | Ekho quits (~Ekho@user/ekho) (Quit: CORE ERROR, SYSTEM HALTED.) |
| 21:50:26 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:51:15 | <tomsmeding> | Types of the form "forall A : Set..." are sets. Sets can contain elements that quantify over the universe of sets. |
| 21:52:09 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 21:54:19 | <ncf> | https://dl.acm.org/doi/pdf/10.1145/3209108.3209130 section 2 has a definition |
| 21:54:20 | <EvanR> | the elements of sets are sets? |
| 21:54:26 | <EvanR> | like in set theory? |
| 21:54:53 | <ncf> | huh |
| 21:55:01 | <ncf> | Set is just a universe here |
| 21:55:13 | <tomsmeding> | EvanR: the "quantify" is essential there |
| 21:55:20 | <EvanR> | "Sets can contain elements that quantify ..." |
| 21:55:39 | <EvanR> | So you have some sets, and now we're talking about elements |
| 21:55:45 | <ncf> | the elements/terms/inhabitants of a universe are types |
| 21:55:46 | <EvanR> | and the element is doing quantification somehow |
| 21:55:53 | <tomsmeding> | Int is a set. Maybe Int is a set. Is `forall a. Maybe a` a set? |
| 21:56:12 | <EvanR> | I don't know how to comprehend forall a . Maybe a |
| 21:56:43 | <EvanR> | a family of types ? |
| 21:56:44 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:57:06 | <EvanR> | but going back, you're saying the elements are actually stuff like Int |
| 21:57:06 | <ncf> | that's a type |
| 21:57:20 | <EvanR> | not stuff like 1, 3, 4, 7 |
| 21:57:46 | <EvanR> | but the word Sets earlier was plural |
| 21:57:54 | <EvanR> | so you're talking about universes of types |
| 21:57:59 | <EvanR> | is that right |
| 21:58:14 | <ncf> | yes, universes of types are the things that can be impredicative or not |
| 21:58:33 | <EvanR> | Int is a type, Maybe Int is a type |
| 21:58:49 | <EvanR> | it's not quantifying at all right so that's not applicable |
| 21:59:10 | <ncf> | yeah there's no size issues there |
| 21:59:10 | × | Wygulmage quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 21:59:28 | <EvanR> | forall a . Maybe a is syntactically a type, in haskell |
| 21:59:43 | <EvanR> | but what are the semantics |
| 22:00:10 | <ncf> | impredicativity can be understood syntactically |
| 22:00:16 | <EvanR> | ok |
| 22:00:23 | <EvanR> | I retract the question then |
| 22:00:53 | <ncf> | that type would be written Π (A : U) Maybe A in type theory, and the question is whether this is an element of U or U⁺, where U⁺ is the successor universe of U |
| 22:01:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:02:08 | <ncf> | in haskell this lives in U (as does every type) so haskell has an impredicative universe in this sense (in fact it has Type : Type which is even stronger (and inconsistent)) |
| 22:03:06 | <EvanR> | ok your last explanation made sense, the U vs U+ thing, with the capital pi, so what does "Set is impredicative / predicative" have to do with that |
| 22:03:37 | <EvanR> | originally i thought Set was a category |
| 22:03:40 | <ncf> | well both Set and U are what i'm calling the first universe |
| 22:04:04 | <EvanR> | Set = U |
| 22:04:12 | <ncf> | i called it Set at first because that's how Coq calls its impredicative universe iirc |
| 22:04:26 | <tomsmeding> | isn't that Prop? |
| 22:04:36 | <ncf> | its other one :) |
| 22:04:56 | → | alfiee joins (~alfiee@user/alfiee) |
| 22:04:58 | <ncf> | https://coq.inria.fr/doc/v8.15/refman/language/cic.html#the-calculus-of-inductive-constructions-with-impredicative-set |
| 22:06:24 | tomsmeding | doesn't actually know what I'm talking about here |
| 22:06:27 | <EvanR> | I see that Set is impredicative or predicative will bear on "what is in U anyway" |
| 22:06:34 | <EvanR> | (the first universe) |
| 22:06:45 | <EvanR> | beyond that I'm still not sure how xD |
| 22:07:23 | <EvanR> | something to do with pi types based on U |
| 22:07:41 | <EvanR> | but the syntax isn't forthcoming on which is which |
| 22:07:49 | <EvanR> | and syntax is all there is! |
| 22:07:53 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 22:08:30 | <ncf> | which is which what |
| 22:08:36 | <EvanR> | which universe U could be |
| 22:08:46 | <EvanR> | or where the whole type at hand lives |
| 22:08:49 | <EvanR> | if anywhere |
| 22:09:08 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 22:10:22 | → | Guest87 joins (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) |
| 22:10:36 | <EvanR> | is it like, in the course of defining a universe I first list self contained inhabitants and at the end, I say U is this thing consisting of all of the above. (a predicative presentation) |
| 22:10:50 | × | Guest87 quits (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) (Client Quit) |
| 22:10:54 | <EvanR> | or if I can't get to the end without mentioning the universe U that I'm trying to make, it is impredicative |
| 22:11:03 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 22:11:31 | <tomsmeding> | if I remember correctly, in the end, the difference is "is Π (A : U) Maybe A in U, or in U⁺?" If it's in U, then there is only one universe: all type formers just take stuff in U and the result lives in U. If it's _not_ in U, then Maybe Int will live in U0, but `Π (A : U0) Maybe A` will live in U1 because quantifying over something in U0 puts you in U0⁺ = U1 |
| 22:13:04 | <EvanR> | this second part would be easier to follow if you didn't switch from U to U0 suddenly |
| 22:13:15 | <EvanR> | which I guess is renaming of the same thing |
| 22:13:20 | <tomsmeding> | sorry |
| 22:13:25 | <tomsmeding> | I meant U for any Un |
| 22:13:31 | <EvanR> | shoot |
| 22:13:36 | <tomsmeding> | for example U0 |
| 22:13:39 | × | tromp quits (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:14:07 | → | Ekho joins (~Ekho@user/ekho) |
| 22:14:24 | <tomsmeding> | but if the answer to that question is "it's in U", then you might as well just destroy all Un with n >= 1, because you'll never need them, and then U = U0 because there's only one universe |
| 22:14:52 | <monochrom> | Bad habit from Coq I guess. You just write "Type" and it means "Type n" where n is inferred from context. So you write "Type : Type" and it is nothing paradoxical, it is inferred to be "Type n : Type n+1" |
| 22:15:58 | <EvanR> | is the precedence of Type _ really less than addition there |
| 22:16:34 | <monochrom> | :( |
| 22:16:41 | <monochrom> | "Type n : Type (n+1)" |
| 22:16:56 | <EvanR> | now I won't know |
| 22:16:59 | <EvanR> | lol |
| 22:17:28 | <EvanR> | do you need the parens in Coq |
| 22:18:01 | <monochrom> | Coq does not allow you to write "Type n" or "Type (n+1)". It only lets you write "Type" and it infers the level. |
| 22:19:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:19:26 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 22:19:38 | <ncf> | there seems to be syntax for specifying levels explicitly but i can't tell how it works https://coq.inria.fr/doc/V8.18.0/refman/language/core/sorts.html#sorts |
| 22:19:43 | <ncf> | average coq documentation experience |
| 22:19:47 | <monochrom> | But you would need the parens in Lean. :) |
| 22:22:54 | <monochrom> | I guess Coq's is like "Type @{...}" so it is parenthesized, by curry braces. |
| 22:23:20 | <EvanR> | parenthesized by braces, braced by brackets, and bracketed by parentheses |
| 22:23:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 22:25:51 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 22:35:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:37:46 | → | stm32nucleo joins (~stm32nucl@2a02:1210:545d:200:a978:119d:8aba:7f6e) |
| 22:40:01 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 22:49:07 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:49:10 | × | ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 22:50:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:52:00 | → | alfiee joins (~alfiee@user/alfiee) |
| 22:55:21 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 22:56:13 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 22:57:09 | × | stm32nucleo quits (~stm32nucl@2a02:1210:545d:200:a978:119d:8aba:7f6e) (Quit: Client closed) |
| 22:57:22 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:58:05 | → | olivial_ joins (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) |
| 23:00:34 | × | olivial quits (~benjaminl@user/benjaminl) (Ping timeout: 260 seconds) |
| 23:06:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:07:12 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:09:12 | → | malte joins (~malte@mal.tc) |
| 23:09:59 | × | AlexNoo quits (~AlexNoo@178.34.162.44) (Read error: Connection reset by peer) |
| 23:11:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 23:11:25 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 23:12:14 | → | AlexNoo joins (~AlexNoo@178.34.162.44) |
| 23:14:01 | → | gmg joins (~user@user/gehmehgeh) |
| 23:17:49 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 23:18:12 | × | zungi quits (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 23:20:17 | → | malte joins (~malte@mal.tc) |
| 23:20:23 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 23:21:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:23:20 | → | zungi joins (~tory@user/andrewchawk) |
| 23:26:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:29:47 | × | pabs3 quits (~pabs3@user/pabs3) (Remote host closed the connection) |
| 23:30:44 | → | pabs3 joins (~pabs3@user/pabs3) |
| 23:37:44 | → | alfiee joins (~alfiee@user/alfiee) |
| 23:37:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:42:13 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 23:42:39 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 23:44:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:50:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:55:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 23:57:47 | → | mange joins (~user@user/mange) |
All times are in UTC on 2025-02-24.