2026/01/01

2026-01-01 00:10:59 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 00:15:31 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 00:16:30 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2026-01-01 00:18:17 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 00:24:58 +0100merijn(~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 +0100Pozyomka(~pyon@user/pyon) pyon
2026-01-01 00:40:38 +0100Pixi`(~Pixi@user/pixi) Pixi
2026-01-01 00:43:49 +0100Pixi(~Pixi@user/pixi) (Ping timeout: 264 seconds)
2026-01-01 00:44:11 +0100Everything(~Everythin@46.96.10.169) (Quit: leaving)
2026-01-01 00:52:38 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 00:55:55 +0100L29Ah(~L29Ah@wikipedia/L29Ah) ()
2026-01-01 00:57:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 01:03:55 +0100traxex(traxex@user/traxex) (Ping timeout: 264 seconds)
2026-01-01 01:05:18 +0100merijn(~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 +0100merijn(~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 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 01:23:35 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 01:30:16 +0100Tuplanolla1Tuplanolla
2026-01-01 01:32:33 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2026-01-01 01:37:26 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 01:41:35 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 01:48:20 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2026-01-01 01:48:51 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2026-01-01 01:54:20 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 01:57:37 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 250 seconds)
2026-01-01 02:00:52 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 02:02:55 +0100Square3(~Square@user/square) (Ping timeout: 240 seconds)
2026-01-01 02:10:34 +0100omidmash8(~omidmash@user/omidmash) omidmash
2026-01-01 02:13:07 +0100omidmash(~omidmash@user/omidmash) (Ping timeout: 265 seconds)
2026-01-01 02:13:07 +0100omidmash8omidmash
2026-01-01 02:15:11 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 02:19:25 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 02:24:43 +0100divlamir(~divlamir@user/divlamir) (Read error: Connection reset by peer)
2026-01-01 02:24:56 +0100divlamir(~divlamir@user/divlamir) divlamir
2026-01-01 02:30:56 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 240 seconds)
2026-01-01 02:37:59 +0100rainbyte_(~rainbyte@186.22.19.214) rainbyte
2026-01-01 02:38:09 +0100rainbyte(~rainbyte@186.22.19.214) (Ping timeout: 244 seconds)
2026-01-01 02:43:41 +0100rainbyte(~rainbyte@186.22.19.214) rainbyte
2026-01-01 02:44:35 +0100rainbyte_(~rainbyte@186.22.19.214) (Ping timeout: 240 seconds)
2026-01-01 02:50:44 +0100Tuplanolla(~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.)
2026-01-01 02:53:30 +0100aman(~aman@user/aman) aman
2026-01-01 03:00:01 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 246 seconds)
2026-01-01 03:00:26 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2026-01-01 03:00:55 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2026-01-01 03:01:36 +0100jmcantrell(~weechat@user/jmcantrell) jmcantrell
2026-01-01 03:02:11 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
2026-01-01 03:04:13 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2026-01-01 03:06:39 +0100bitdex_(~bitdex@gateway/tor-sasl/bitdex) bitdex
2026-01-01 03:10:37 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
2026-01-01 03:43:37 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 03:48:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-01-01 03:54:55 +0100machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 264 seconds)
2026-01-01 04:00:59 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 04:05:28 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 04:17:09 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 04:19:19 +0100driib3180(~driib@vmi931078.contaboserver.net) (Ping timeout: 244 seconds)
2026-01-01 04:20:58 +0100synchromesh(~john@115.69.186.131) synchromesh
2026-01-01 04:21:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 04:22:00 +0100Digit(~Digit@user/digit) (Ping timeout: 245 seconds)
2026-01-01 04:22:07 +0100Digitteknohippie(~Digit@user/digit) Digit
2026-01-01 04:33:46 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 04:38:01 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 04:48:04 +0100bitdex_(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2026-01-01 04:50:01 +0100driib3180(~driib@vmi931078.contaboserver.net) driib
2026-01-01 04:51:40 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 04:56:13 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 04:56:29 +0100omidmash(~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat)
2026-01-01 05:01:03 +0100omidmash(~omidmash@user/omidmash) omidmash
2026-01-01 05:06:35 +0100driib3180(~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds)
2026-01-01 05:14:25 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2026-01-01 05:18:11 +0100driib3180(~driib@vmi931078.contaboserver.net) driib
2026-01-01 05:37:31 +0100driib3180(~driib@vmi931078.contaboserver.net) (Ping timeout: 246 seconds)
2026-01-01 05:41:51 +0100driib3180(~driib@vmi931078.contaboserver.net) driib
2026-01-01 05:45:55 +0100driib3180(~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds)
2026-01-01 05:57:52 +0100driib3180(~driib@vmi931078.contaboserver.net) driib
2026-01-01 06:01:14 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 06:01:55 +0100driib3180(~driib@vmi931078.contaboserver.net) (Ping timeout: 240 seconds)
2026-01-01 06:07:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 06:10:39 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
2026-01-01 06:13:06 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2026-01-01 06:17:08 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2026-01-01 06:19:31 +0100elarks(~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 +0100karenw(~karenw@user/karenw) (Ping timeout: 246 seconds)
2026-01-01 06:54:31 +0100jmcantrell(~weechat@user/jmcantrell) (Ping timeout: 246 seconds)
2026-01-01 07:03:50 +0100Vajb(~Vajb@n70u4zvz328004ovt20-1.v6.elisa-mobile.fi) (Ping timeout: 256 seconds)
2026-01-01 07:32:14 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 07:37:12 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-01-01 07:48:08 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 07:52:37 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 07:58:48 +0100mmohammadi9812(~mohammad@141.148.239.148) mmohammadi9812
2026-01-01 08:02:16 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 08:05:30 +0100mmohammadi9812(~mohammad@141.148.239.148) (Remote host closed the connection)
2026-01-01 08:06:58 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 08:11:12 +0100fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2026-01-01 08:16:59 +0100fgarcia(~lei@user/fgarcia) fgarcia
2026-01-01 08:18:13 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 08:22:35 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 08:28:29 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: ZNC 1.9.1+deb2+b3 - https://znc.in)
2026-01-01 08:30:21 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2026-01-01 08:34:01 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 08:38:28 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 08:52:26 +0100machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod
2026-01-01 08:52:46 +0100debayan(~debayan@user/debayan) debayan
2026-01-01 08:53:40 +0100debayan(~debayan@user/debayan) (Client Quit)
2026-01-01 08:59:26 +0100gabiruh(~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in)
2026-01-01 08:59:42 +0100gabiruh(~gabiruh@vps19177.publiccloud.com.br) gabiruh
2026-01-01 09:03:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 09:07:52 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 09:18:18 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 09:23:43 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-01-01 09:29:55 +0100machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 246 seconds)
2026-01-01 09:36:23 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 09:36:58 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2026-01-01 09:42:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 10:01:40 +0100Inline(~User@cgn-195-14-221-74.nc.de) (Remote host closed the connection)
2026-01-01 10:04:17 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 10:09:06 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2026-01-01 10:28:56 +0100aetepe(~aetepe@212.125.9.97) aetepe
2026-01-01 10:32:30 +0100Inline(~User@cgn-195-14-221-74.nc.de) Inline
2026-01-01 10:40:08 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2026-01-01 10:43:59 +0100wickedjargon(~user@64.114.24.74) wickedjargon
2026-01-01 10:59:10 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 246 seconds)
2026-01-01 10:59:53 +0100Square3(~Square@user/square) Square
2026-01-01 11:00:26 +0100wickedjargon(~user@64.114.24.74) (Remote host closed the connection)
2026-01-01 11:02:00 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) robobub
2026-01-01 11:04:12 +0100wickedjargon(~user@64.114.24.74) wickedjargon
2026-01-01 11:05:18 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 11:09:44 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2026-01-01 11:10:01 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 11:15:35 +0100wickedjargon(~user@64.114.24.74) (Remote host closed the connection)
2026-01-01 11:16:29 +0100zlqrvx(~zlqrvx@user/zlqrvx) zlqrvx
2026-01-01 11:17:36 +0100wickedjargon(~user@64.114.24.74) wickedjargon
2026-01-01 11:23:02 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 11:27:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 11:27:58 +0100DigitteknohippieDigit
2026-01-01 11:39:54 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 11:41:58 +0100zlqrvx(~zlqrvx@user/zlqrvx) (Quit: connection reset by purr)
2026-01-01 11:42:10 +0100zlqrvx(~zlqrvx@user/zlqrvx) zlqrvx
2026-01-01 11:44:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 11:45:16 +0100Tuplanolla(~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) Tuplanolla
2026-01-01 11:56:08 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 11:58:00 +0100wickedjargon(~user@64.114.24.74) (Remote host closed the connection)
2026-01-01 11:58:55 +0100jreicher(~user@user/jreicher) (Ping timeout: 240 seconds)
2026-01-01 12:00:09 +0100jreicher(~user@user/jreicher) jreicher
2026-01-01 12:00:15 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-01 12:04:47 +0100itaipu(~itaipu@168.121.98.37) itaipu
2026-01-01 12:06:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 12:10:55 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-01 12:17:07 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 264 seconds)
2026-01-01 12:20:01 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 246 seconds)
2026-01-01 12:20:37 +0100housemate(~housemate@202.7.247.155) (Quit: I am over the moon, although it is day time so I am probably on the other side of the world, and upside down which would make me the right way up.)
2026-01-01 12:23:43 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2026-01-01 12:25:24 +0100housemate(~housemate@202.7.247.155) housemate
2026-01-01 12:38:09 +0100itaipu(~itaipu@168.121.98.37) (Read error: Connection reset by peer)
2026-01-01 12:55:57 +0100itaipu(~itaipu@168.121.98.37) itaipu
2026-01-01 12:56:38 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-01 13:09:29 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2026-01-01 13:10:41 +0100arthurvlearthy
2026-01-01 13:22:42 +0100marinelli(~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli)
2026-01-01 13:22:43 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds)
2026-01-01 13:32:15 +0100Jackneill(~Jackneill@178-164-245-16.pool.digikabel.hu) (Ping timeout: 244 seconds)
2026-01-01 13:32:49 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 246 seconds)
2026-01-01 13:34:23 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn