| 2026-01-01 00:10:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 00:15:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 00:16:30 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-01-01 00:18:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 00:24:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 00:25:34 +0100 | <monochrom> | Do a pair of complementary things and do them well: Open a pastry bakery and a gym next to each other. (True story.) |
| 2026-01-01 00:32:23 +0100 | Pozyomka | (~pyon@user/pyon) pyon |
| 2026-01-01 00:40:38 +0100 | Pixi` | (~Pixi@user/pixi) Pixi |
| 2026-01-01 00:43:49 +0100 | Pixi | (~Pixi@user/pixi) (Ping timeout: 264 seconds) |
| 2026-01-01 00:44:11 +0100 | Everything | (~Everythin@46.96.10.169) (Quit: leaving) |
| 2026-01-01 00:52:38 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 00:55:55 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-01-01 00:57:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-01 01:03:55 +0100 | traxex | (traxex@user/traxex) (Ping timeout: 264 seconds) |
| 2026-01-01 01:05:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 01:06:47 +0100 | <janus> | [exa]: is it really just MPTC that would require type-level computation interleaved with previous typechecking? or is it about fundeps? |
| 2026-01-01 01:07:51 +0100 | <janus> | if i understand correctly, fundeps only make sense with MPTC, and since fundeps are so prevalent with mtl, i wonder whether that is why you said MPTC instead of saying fundeps. since for all practical typecheckers, they will need to support both |
| 2026-01-01 01:09:24 +0100 | <geekosaur> | my understanding is that MPTCs are really only usable with either fundeps or TFs |
| 2026-01-01 01:09:38 +0100 | <geekosaur> | inference isn't possible otherwise |
| 2026-01-01 01:10:04 +0100 | <janus> | right. so it's not strictly MPTC that require interleaving |
| 2026-01-01 01:10:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 01:10:36 +0100 | <janus> | i still can't imagine a program that would require something like that |
| 2026-01-01 01:13:17 +0100 | <janus> | maybe the easiest example should be something that uses mtl, and somehow has polymorphic types in both the 'input' and the 'output' type of a fundep. now, the surrounding program somehow determines one of these, and the typechecker should be able to run enough of 'regular' constraints to find out that there is this constraint on input and output |
| 2026-01-01 01:13:38 +0100 | <janus> | then, it should evaluate the fundep and that should give it enough info to find the 'principal' type |
| 2026-01-01 01:15:02 +0100 | <janus> | such a program, without interleaving, would have ambiguous types and compilation would fail. since it wouldn't be able to take the 'output' and propagate it to other constraints |
| 2026-01-01 01:19:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 01:23:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-01 01:30:16 +0100 | Tuplanolla1 | Tuplanolla |
| 2026-01-01 01:32:33 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-01-01 01:37:26 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 01:41:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-01 01:48:20 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-01 01:48:51 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-01 01:54:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 01:57:37 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 250 seconds) |
| 2026-01-01 02:00:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 02:02:55 +0100 | Square3 | (~Square@user/square) (Ping timeout: 240 seconds) |
| 2026-01-01 02:10:34 +0100 | omidmash8 | (~omidmash@user/omidmash) omidmash |
| 2026-01-01 02:13:07 +0100 | omidmash | (~omidmash@user/omidmash) (Ping timeout: 265 seconds) |
| 2026-01-01 02:13:07 +0100 | omidmash8 | omidmash |
| 2026-01-01 02:15:11 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 02:19:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 02:24:43 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-01 02:24:56 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-01-01 02:30:56 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 2026-01-01 02:37:59 +0100 | rainbyte_ | (~rainbyte@186.22.19.214) rainbyte |
| 2026-01-01 02:38:09 +0100 | rainbyte | (~rainbyte@186.22.19.214) (Ping timeout: 244 seconds) |
| 2026-01-01 02:43:41 +0100 | rainbyte | (~rainbyte@186.22.19.214) rainbyte |
| 2026-01-01 02:44:35 +0100 | rainbyte_ | (~rainbyte@186.22.19.214) (Ping timeout: 240 seconds) |
| 2026-01-01 02:50:44 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-01 02:53:30 +0100 | aman | (~aman@user/aman) aman |
| 2026-01-01 03:00:01 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 246 seconds) |
| 2026-01-01 03:00:26 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-01 03:00:55 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-01 03:01:36 +0100 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-01 03:02:11 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-01 03:04:13 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-01 03:06:39 +0100 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-01 03:10:37 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-01 03:43:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 03:48:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-01 03:54:55 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 2026-01-01 04:00:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 04:05:28 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 04:17:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 04:19:19 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) (Ping timeout: 244 seconds) |
| 2026-01-01 04:20:58 +0100 | synchromesh | (~john@115.69.186.131) synchromesh |
| 2026-01-01 04:21:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-01 04:22:00 +0100 | Digit | (~Digit@user/digit) (Ping timeout: 245 seconds) |
| 2026-01-01 04:22:07 +0100 | Digitteknohippie | (~Digit@user/digit) Digit |
| 2026-01-01 04:33:46 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 04:38:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 04:48:04 +0100 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2026-01-01 04:50:01 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) driib |
| 2026-01-01 04:51:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 04:56:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-01 04:56:29 +0100 | omidmash | (~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat) |
| 2026-01-01 05:01:03 +0100 | omidmash | (~omidmash@user/omidmash) omidmash |
| 2026-01-01 05:06:35 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds) |
| 2026-01-01 05:14:25 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-01 05:18:11 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) driib |
| 2026-01-01 05:37:31 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) (Ping timeout: 246 seconds) |
| 2026-01-01 05:41:51 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) driib |
| 2026-01-01 05:45:55 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds) |
| 2026-01-01 05:57:52 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) driib |
| 2026-01-01 06:01:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-01 06:01:55 +0100 | driib3180 | (~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds) |
| 2026-01-01 06:07:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-01 06:10:39 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-01 06:13:06 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-01 06:17:08 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2026-01-01 06:19:31 +0100 | elarks | (~elarks@user/yerrii) (Ping timeout: 246 seconds) |
| 2026-01-01 06:21:21 +0100 | <[exa]> | janus: yeah I believe the fundeps kinda trigger the computation issue there, but i have no actual proof in hand other than "yeah this is what you do with relations in set theory to turn them to functions" |
| 2026-01-01 06:49:58 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 246 seconds) |
| 2026-01-01 06:54:31 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 246 seconds) |
| 2026-01-01 07:03:50 +0100 | Vajb | (~Vajb@n70u4zvz328004ovt20-1.v6.elisa-mobile.fi) (Ping timeout: 256 seconds) |