| 2025-04-28 00:00:24 +0200 | j0lol | (~j0lol@132.145.17.236) (Ping timeout: 276 seconds) |
| 2025-04-28 00:00:57 +0200 | <davean> | I think the dependent version lets you use information a bit further away than Haskell does. |
| 2025-04-28 00:01:46 +0200 | <davean> | since it sorta drags providence along with it. |
| 2025-04-28 00:02:17 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-04-28 00:02:47 +0200 | <davean> | I have no idea if anyone has done serious work on dragging that information along though ... |
| 2025-04-28 00:04:20 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:05:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-04-28 00:07:43 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 00:22:00 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-28 00:22:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 00:25:20 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-04-28 00:34:46 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 00:35:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 00:44:31 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-28 00:47:07 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:49:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 00:50:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 00:59:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-28 01:02:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 01:03:14 +0200 | koz | (~koz@121.99.240.58) (Ping timeout: 244 seconds) |
| 2025-04-28 01:10:25 +0200 | <haskellbridge> | <loonycyborg> I still have no idea how can you have both pi types and type erasure in the same language. |
| 2025-04-28 01:12:49 +0200 | typedfern_ | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) typedfern |
| 2025-04-28 01:16:04 +0200 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
| 2025-04-28 01:16:37 +0200 | <EvanR> | if the code doesn't use the argument, be it a type or a value, then the body is effectively a constant |
| 2025-04-28 01:16:45 +0200 | j0lol | (~j0lol@132.145.17.236) j0lol |
| 2025-04-28 01:18:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 01:19:29 +0200 | <EvanR> | any call site would need to be adjusted to stop trying to call it like a function |
| 2025-04-28 01:19:41 +0200 | <EvanR> | just discard the argument |
| 2025-04-28 01:21:18 +0200 | <EvanR> | sigma type is a bit more mysterious to me, how do you know someone won't want to use the 2nd component |
| 2025-04-28 01:24:43 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) |
| 2025-04-28 01:25:24 +0200 | sprotte24 | (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-28 01:29:14 +0200 | <monochrom> | Do you accept: Encode Σx:A. B(x) as ∀r. Πx:A. B(x) -> r so it is just pi types all over again? :) |
| 2025-04-28 01:32:13 +0200 | <EvanR> | ... not sure |
| 2025-04-28 01:32:36 +0200 | <monochrom> | Err, ∀r. (Πx:A. B(x) -> r) -> r |
| 2025-04-28 01:34:14 +0200 | <EvanR> | ok yes |
| 2025-04-28 01:34:21 +0200 | <monochrom> | :) |
| 2025-04-28 01:35:01 +0200 | <haskellbridge> | <loonycyborg> Even if you technically make this work not sure it would be a good language design. Like most types that aren't passed around are erased but some have to remain which kinda feels inconsistent. |
| 2025-04-28 01:35:56 +0200 | <EvanR> | if that's in the machine code then it only bothers somebody trying to disassemnle it |
| 2025-04-28 01:36:02 +0200 | <monochrom> | Maybe the programmer doesn't use that encoding, but the compiler does the translation. |
| 2025-04-28 01:36:08 +0200 | <EvanR> | typing with pinkies is hard |
| 2025-04-28 01:36:36 +0200 | fantom | (~fantom@2.219.56.221) (Ping timeout: 244 seconds) |
| 2025-04-28 01:37:20 +0200 | <EvanR> | erasing types or proofs shouldn't change the "observable" behavior |
| 2025-04-28 01:38:16 +0200 | <haskellbridge> | <loonycyborg> still it requires operating on type level things that can't be erased |
| 2025-04-28 01:38:33 +0200 | <haskellbridge> | <loonycyborg> which probably will have different implementations at runtime and compile time |
| 2025-04-28 01:38:54 +0200 | <EvanR> | if it's purely at the type level then it wouldn't need to exist at runtime |
| 2025-04-28 01:39:22 +0200 | <EvanR> | because this isn't java |
| 2025-04-28 01:39:24 +0200 | mange | (~user@user/mange) mange |
| 2025-04-28 01:39:32 +0200 | <EvanR> | (but I heard java erases it's types also) |
| 2025-04-28 01:39:50 +0200 | <haskellbridge> | <loonycyborg> I'm not so sure because of types that could be specified entirely at runtime |
| 2025-04-28 01:40:30 +0200 | <EvanR> | well then that's not purely at the type level definitely |
| 2025-04-28 01:41:46 +0200 | <EvanR> | accept keyboard input and append to an ongoing list of Types that you can then ask for a listing of, because they have nice Show instances |
| 2025-04-28 01:41:55 +0200 | <EvanR> | isn't a type level thing |
| 2025-04-28 01:42:33 +0200 | <haskellbridge> | <loonycyborg> to me type erasure seems like technical decision asserting that "compile type == type level; runtime == term level" |
| 2025-04-28 01:43:01 +0200 | <EvanR> | well that's not true is it |
| 2025-04-28 01:43:19 +0200 | <EvanR> | because e.g. constant folding at compile time etc |
| 2025-04-28 01:43:48 +0200 | <haskellbridge> | <loonycyborg> so to get proper dependent types in a compiled language would have to drop type erasure, perhaps replacing it by something else |
| 2025-04-28 01:44:54 +0200 | <EvanR> | once you get to a phase where the types aren't doing anything, then keeping them around can only waste resources |
| 2025-04-28 01:46:03 +0200 | <haskellbridge> | <loonycyborg> But still there is the case of reading of arbitrary type from stdin :P |
| 2025-04-28 01:46:18 +0200 | <EvanR> | you can remove them like a compiler is expected to remove terms that aren't doing anything |
| 2025-04-28 01:46:26 +0200 | <haskellbridge> | <loonycyborg> if you explicitly don't support it then it's unlikely that it's a localized case |
| 2025-04-28 01:46:28 +0200 | <mange> | Idris 2 lets you be precise about which types you expect to be erased from the program, using multiplicities: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#erasure |
| 2025-04-28 01:46:41 +0200 | <haskellbridge> | <loonycyborg> like need to explicitly figure out what is supported and what isn't |
| 2025-04-28 01:47:01 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) (Ping timeout: 248 seconds) |
| 2025-04-28 01:47:33 +0200 | <EvanR> | I don't see how you would even erase a type that is generated at runtime |
| 2025-04-28 01:47:37 +0200 | <EvanR> | or why you would want to |
| 2025-04-28 01:50:39 +0200 | fantom | (~fantom@2.219.56.221) |
| 2025-04-28 01:51:13 +0200 | <haskellbridge> | <loonycyborg> What I'm really wondering about are things like: if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it? |
| 2025-04-28 01:51:33 +0200 | <haskellbridge> | <loonycyborg> And if we can then how it works :P |
| 2025-04-28 01:52:54 +0200 | <EvanR> | if this is mainstreet dependent types you wouldn't have a separate type level Nat |
| 2025-04-28 01:53:17 +0200 | <EvanR> | and compile time arithmetic at runtime sounds like a contradiction |
| 2025-04-28 01:54:02 +0200 | <EvanR> | the Nat used at type level can be the same Nat used at value level |
| 2025-04-28 01:54:13 +0200 | <EvanR> | not a DataKind |
| 2025-04-28 01:55:26 +0200 | <EvanR> | -- oh, compile time arithmetic at runtime, that would be JIT |
| 2025-04-28 01:56:53 +0200 | <mange> | I've also seen https://dl.acm.org/doi/10.1145/3341692, which is kind of about deferring type checking until runtime. It's not exactly what you're looking for, but it feels in the same ballpark. |
| 2025-04-28 01:59:07 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-28 01:59:21 +0200 | <haskellbridge> | <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P |
| 2025-04-28 02:01:21 +0200 | <EvanR> | the conflation between arithmetic on literal types is a haskell thing because it's weird type level hacks |
| 2025-04-28 02:01:35 +0200 | <EvanR> | you don't want to do this |
| 2025-04-28 02:01:47 +0200 | <EvanR> | outside haskell |
| 2025-04-28 02:04:17 +0200 | <haskellbridge> | <loonycyborg> Yes, but if it's made fully dependent typed then potentially could read any sort of types from stdin, even those that aren't haskell specific hacks |
| 2025-04-28 02:04:58 +0200 | jespada_ | (~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-28 02:05:30 +0200 | <EvanR> | you can read chars or Word8 from stdin I would believe that |
| 2025-04-28 02:06:15 +0200 | <haskellbridge> | <loonycyborg> So I'm thinking that going fully dependent typing would either result in some weird inconsistencies or push the language into becoming fully dynamic like python |
| 2025-04-28 02:06:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 02:06:41 +0200 | <haskellbridge> | <loonycyborg> * typed |
| 2025-04-28 02:06:48 +0200 | <EvanR> | python's dynamic types cause the program to crash if a type check fails |
| 2025-04-28 02:06:55 +0200 | <EvanR> | that wouldn't happen |
| 2025-04-28 02:07:16 +0200 | <EvanR> | the program itself can be well typed while still juggling types at runtime |
| 2025-04-28 02:07:26 +0200 | <EvanR> | (for whatever reason) |
| 2025-04-28 02:10:17 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-04-28 02:13:56 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 02:17:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 02:18:20 +0200 | <monochrom> | Yeah "type-level 0::Nat as opposed to term-level 0::Nat" is a GHC invention, proving that GHC does not have dependent typing. In dependent typing there is just one 0::Nat; you can use it anywhere you want, in a term or in a type, but it's the same 0::Nat used in both sites, not two different versions. |
| 2025-04-28 02:18:37 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-28 02:19:34 +0200 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2025-04-28 02:23:38 +0200 | <haskellbridge> | <loonycyborg> Practical case would be serialization: can you construct your data entirely based on something you de-serialize with dependent types? |
| 2025-04-28 02:24:06 +0200 | <haskellbridge> | <loonycyborg> Probably if your program operates on such types then it wouldn't be too optimized |
| 2025-04-28 02:24:22 +0200 | <haskellbridge> | <loonycyborg> because compiler doesn't know anything about actual data that will be read |
| 2025-04-28 02:24:26 +0200 | <haskellbridge> | <loonycyborg> unless it'sJIT |
| 2025-04-28 02:24:47 +0200 | <monochrom> | If you have n::Nat coming from user input, for example the user inputs n booleans and you store them in an index-safe vector, i.e., the vector type includes the length n, i.e., Vec n Bool, then generically speaking you now have a sigma type: v :: Σn::Nat. Vec n Bool. You can call that dynamic; it's a sigma, it's OOP now. |
| 2025-04-28 02:27:28 +0200 | <monochrom> | Or you can do an implicit church encoding like I described. You don't construct a pair for the sigma type, you pass n and v "separately" to a function foo :: (n::Nat) -> Vec n Bool -> IO (). |
| 2025-04-28 02:30:10 +0200 | <monochrom> | s/pass n and v/pass n and the vector/ |
| 2025-04-28 02:34:01 +0200 | <monochrom> | You are reminding me of that joke (or true story) about C++ back then. |
| 2025-04-28 02:34:57 +0200 | <monochrom> | Someone wrote a prime factorization algorithm in C++ that takes O(1) time. How: The factorization happened at compile time, the generated code just needs to print the answer. |
| 2025-04-28 02:35:31 +0200 | <geekosaur> | true story and done multiple times by multiple people |
| 2025-04-28 02:36:03 +0200 | <geekosaur> | (one of whom was a CS postgrad at C-MU who replicated it after hearing about the original) |
| 2025-04-28 02:36:55 +0200 | <monochrom> | If you require the number in question to be obtained during runtime-only from some user or entity, then the factorization must happen at run time. Do you call that unoptimized, just because the "O(1)-time static solution" exists? |
| 2025-04-28 02:37:59 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) |
| 2025-04-28 02:38:13 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) |
| 2025-04-28 02:40:38 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-28 02:41:31 +0200 | otto_s | (~user@p5de2f428.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-28 02:44:56 +0200 | <monochrom> | I guess I can cheat too. I can take it down to linear time. The program is a huge binary search tree that stores the answer for every input for a sufficiently large range. The exe will not fit in any storage in existence today, nay, any data centre, but we can talk hypothetically about how nice it would be. >:) |
| 2025-04-28 02:50:48 +0200 | otto_s | (~user@p4ff27ad7.dip0.t-ipconnect.de) |
| 2025-04-28 02:51:55 +0200 | <ames> | if you don't have typecase at runtime you can just erase all the types in addition to things that are otherwise marked erased. agda does this, pretty sure coq does too |
| 2025-04-28 02:54:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 02:55:26 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 272 seconds) |
| 2025-04-28 02:57:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 02:59:48 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-04-28 03:00:51 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 03:02:41 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-04-28 03:03:32 +0200 | <mauke> | #include "/dev/tty" // please type the correct code |
| 2025-04-28 03:05:52 +0200 | <int-e> | Ah yeah the good old 1988 IOCCC entry. |
| 2025-04-28 03:07:04 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-04-28 03:07:21 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-28 03:13:51 +0200 | OftenFaded9 | (~OftenFade@user/tisktisk) OftenFaded |
| 2025-04-28 03:14:54 +0200 | OftenFaded | (~OftenFade@user/tisktisk) (Ping timeout: 240 seconds) |
| 2025-04-28 03:15:19 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-28 03:15:30 +0200 | OftenFaded9 | (~OftenFade@user/tisktisk) (Client Quit) |
| 2025-04-28 03:18:07 +0200 | <monochrom> | Oh hahaha |
| 2025-04-28 03:21:14 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds) |
| 2025-04-28 03:22:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-28 03:28:53 +0200 | snoopy1 | (~Thunderbi@199.115.144.130) |
| 2025-04-28 03:33:06 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 03:33:24 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 03:33:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 03:34:35 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) (Remote host closed the connection) |
| 2025-04-28 03:37:01 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) hgolden |
| 2025-04-28 03:42:10 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-28 03:42:31 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 03:44:24 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-28 03:44:54 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 03:48:48 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:c531:a8cf:57a8:ee6f) (Quit: Leaving) |
| 2025-04-28 03:55:03 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) (Ping timeout: 276 seconds) |
| 2025-04-28 03:55:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-28 04:19:59 +0200 | Guest85 | (~Guest85@83.234.227.67) |
| 2025-04-28 04:20:37 +0200 | td_ | (~td@i5387092A.versanet.de) (Ping timeout: 248 seconds) |
| 2025-04-28 04:21:32 +0200 | Guest85 | (~Guest85@83.234.227.67) (Client Quit) |
| 2025-04-28 04:22:13 +0200 | td_ | (~td@i53870908.versanet.de) |
| 2025-04-28 04:29:46 +0200 | snoopy1 | (~Thunderbi@199.115.144.130) (Quit: snoopy1) |
| 2025-04-28 04:30:04 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-28 04:30:24 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 04:37:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-28 04:45:25 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-28 04:48:47 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 04:49:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 04:49:47 +0200 | Square | (~Square@user/square) (Ping timeout: 265 seconds) |
| 2025-04-28 04:50:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 04:50:18 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-28 04:51:08 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 04:56:45 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-28 05:01:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-28 05:03:40 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 05:03:56 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 05:12:21 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 05:12:38 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 05:30:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-28 05:31:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 05:32:37 +0200 | koz | (~koz@121.99.240.58) |
| 2025-04-28 05:35:16 +0200 | cbs | (df2953d28a@2a03:6000:1812:100::1451) cbs |
| 2025-04-28 05:36:08 +0200 | cbs | (df2953d28a@2a03:6000:1812:100::1451) () |
| 2025-04-28 05:38:38 +0200 | <haskellbridge> | <Bowuigi> loonycyborg if your pi type acts as a forall, you can erase it safely. There's more conditions but that's the most intuitive one |
| 2025-04-28 05:41:32 +0200 | <haskellbridge> | <Bowuigi> EvanR type erasure is part of standard optimization in any functional lang. Dependently typed langs get a "cut-down" version of it that requires complex algorithms to work properly (not sure if it's actually decidable). It's a problem on dependently typed langs, but a given on the rest |
| 2025-04-28 05:41:51 +0200 | <haskellbridge> | <Bowuigi> Also that's partly why dependent haskell takes so much effort |
| 2025-04-28 05:42:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 05:43:53 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-28 05:45:42 +0200 | <haskellbridge> | <Bowuigi> Another big reason was hinted at here too: Dependent types + unrestricted effects = magic. You can get something with a random type or with a type you read from stdin. Dependent types in Haskell aren't just about the proofs, it's about making a stupidly powerful language for everyone |
| 2025-04-28 05:50:57 +0200 | <haskellbridge> | <Bowuigi> Also, opening the door to dependent types means allowing the "I want to prove more and more" philosophy. First one adds the base constructs because deriving the eta laws for the rest of things is harder with just pi types (unless you use a novel trick from a random thesis I read and forgot about), then dependent ADTs, then slightly more complex equality, then HITs, then IRTs, then IITs, then cubical stuff, then... |
| 2025-04-28 05:51:02 +0200 | <haskellbridge> | ... extension types, then you take a Higher Observational detour aaaand you've reached current research and are stuck with a very complex system that's too hard to verify properly. |
| 2025-04-28 05:52:23 +0200 | <haskellbridge> | <Bowuigi> Suddenly to get a chance of using the newest features you need a PhD because progress is not quite there yet |
| 2025-04-28 05:52:25 +0200 | <ames> | seems very strange to assume that this is a common thing to do when there's exactly one language that's done that |
| 2025-04-28 05:54:01 +0200 | <ames> | also erasing types is very easy. code generators for languages that aren't Idris2 simply do not include a way to generate code for types |
| 2025-04-28 05:54:36 +0200 | <ames> | it's erasing the things that *aren't* types e.g. lengths of vectors that's complicated |
| 2025-04-28 05:54:58 +0200 | <haskellbridge> | <Bowuigi> I see |
| 2025-04-28 05:55:42 +0200 | <haskellbridge> | <Bowuigi> As for the "I want to prove more" thing, Agda is the prime example, but Coq and the Red* family (tho that's many languages, so not that big of an issue) are following suit. The rest are kinda on the same path, but moving more slowly |
| 2025-04-28 05:57:59 +0200 | <haskellbridge> | <Bowuigi> It isn't that big of a problem for theorem provers because well, they exist to prove theorems, but Haskell is not a theorem prover |
| 2025-04-28 05:58:05 +0200 | <ames> | coq does not have anything approaching a cubical mode and jon's proof assistants are basically proofs-of-concept |
| 2025-04-28 05:58:54 +0200 | <ames> | "make three to throw away" and all that |
| 2025-04-28 05:59:56 +0200 | <haskellbridge> | <Bowuigi> The previous steps (inductive-inductive and inductive-recursive stuff) were added / are in progress because of user demand in Coq AFAIU |
| 2025-04-28 06:00:37 +0200 | <ames> | "previous steps" - those are completely orthogonal features. |
| 2025-04-28 06:03:40 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Quit: Client closed) |
| 2025-04-28 06:05:30 +0200 | <haskellbridge> | <Bowuigi> Yeah that's the idea |
| 2025-04-28 06:06:13 +0200 | <haskellbridge> | <Bowuigi> Can't find the IIT/IRT stuff on the Coq issues but I remember some talk about supporting them exists lol |
| 2025-04-28 06:06:25 +0200 | <haskellbridge> | <Bowuigi> I should take more notes |
| 2025-04-28 06:10:18 +0200 | <ames> | but you're talking about these things as if there's a "universal dependently-typed language" that everyone's converging to. this is nonsense. idris people are not interested in "more complex equality" or "cubical stuff" and lean people are outright hostile towards these things |
| 2025-04-28 06:11:35 +0200 | <haskellbridge> | <Bowuigi> Ah, sorry, that's not what I meant. I mean that one should resist the temptation to add a lot of shiny new features, as with any software project |
| 2025-04-28 06:16:01 +0200 | <haskellbridge> | <Liamzee> huh, that's interesting, and probably extremely degenerate |
| 2025-04-28 06:16:16 +0200 | <haskellbridge> | <Liamzee> you know how emojis are actually part of the haskell operator namespace? |
| 2025-04-28 06:16:56 +0200 | <haskellbridge> | <Liamzee> if you want an operator version of go, emojis actually suffice since they have no collisions and are single characters. They also brighten up your day. :) |
| 2025-04-28 06:18:55 +0200 | <ames> | i think some emoji should be uppercase so we can use them as constructors |
| 2025-04-28 06:27:36 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2025-04-28 06:27:48 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-04-28 06:29:30 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-28 06:34:48 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 06:37:40 +0200 | polykernel | (~polykerne@user/polykernel) (Remote host closed the connection) |
| 2025-04-28 06:38:49 +0200 | polykernel | (~polykerne@user/polykernel) polykernel |
| 2025-04-28 06:40:04 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 06:40:39 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Quit: Client closed) |
| 2025-04-28 06:43:49 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-28 06:44:12 +0200 | michalz | (~michalz@185.246.207.218) |
| 2025-04-28 06:44:13 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 06:44:44 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Write error: Broken pipe) |
| 2025-04-28 06:47:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-28 06:47:58 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 06:49:38 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 06:51:32 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 06:52:52 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 06:56:03 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 06:58:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 06:58:37 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:00:51 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed) |
| 2025-04-28 07:01:40 +0200 | <EvanR> | or lowercase so we can use them as variables |
| 2025-04-28 07:02:54 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:03:57 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:07:05 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:09:38 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:14:08 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 07:17:15 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-04-28 07:26:44 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) |
| 2025-04-28 07:30:45 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:33:14 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:36:52 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-28 07:37:38 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 07:39:00 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:42:03 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:42:53 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-28 07:47:07 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:53:36 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 07:56:38 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 07:59:04 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 07:59:19 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 08:05:01 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-04-28 08:11:06 +0200 | jco | (~jco@78-70-217-44-no600.tbcn.telia.com) jco |
| 2025-04-28 08:12:32 +0200 | <jco> | Hey, anyone got any recommendations on libraries that can be used for writing (binary) file formats? I.e. something like the inverse of parsing...? |
| 2025-04-28 08:13:12 +0200 | <geekosaur> | @hackage binary |
| 2025-04-28 08:13:12 +0200 | <lambdabot> | https://hackage.haskell.org/package/binary |
| 2025-04-28 08:13:16 +0200 | <geekosaur> | @hackage cereal |
| 2025-04-28 08:13:16 +0200 | <lambdabot> | https://hackage.haskell.org/package/cereal |
| 2025-04-28 08:14:25 +0200 | <jco> | geekosaur: Thanks a lot. |
| 2025-04-28 08:15:01 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2025-04-28 08:18:13 +0200 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 276 seconds) |
| 2025-04-28 08:20:40 +0200 | <Axman6> | I kind of wish there were better options these days, I'm sure there must be. There was some really cool work that went into the cborg and serialise packages to make it fast but it's specific to CBOR |
| 2025-04-28 08:22:35 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-28 08:22:48 +0200 | chele | (~chele@user/chele) chele |
| 2025-04-28 08:24:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-28 08:24:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 08:27:18 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 08:29:55 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-04-28 08:34:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 08:44:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-28 08:48:18 +0200 | halloy3041 | (~halloy304@2001:569:76fd:b00:ada3:3d53:48e5:4f37) |
| 2025-04-28 08:50:29 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-28 08:51:39 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-04-28 08:55:41 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 08:55:47 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk |
| 2025-04-28 08:57:59 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-04-28 09:00:03 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-28 09:00:42 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-04-28 09:03:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 09:03:36 +0200 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) hackager |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <hellwolf> "less mainstream logics" |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <Bowuigi> Oh, mainstream here means popular, in a sense |
| 2025-04-28 09:03:36 +0200 | <haskellbridge> | <Bowuigi> As to which logics specifically, it actually depends on the features the type system has. Haven't read much on categorical logic yet but AFAIU you can use toposes to model dependently typed systems |
| 2025-04-28 09:03:36 +0200 | ChanServ | +v haskellbridge |
| 2025-04-28 09:03:45 +0200 | <haskellbridge> | <hellwolf> I actually don't have a clue what qualifies aslogic in the first place... I guess, something to do with formal way of describing"equality"? |
| 2025-04-28 09:03:47 +0200 | <haskellbridge> | <hellwolf> anyhow, not going to far, |
| 2025-04-28 09:03:49 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/crunkvuyNAgcnoaGKHVPavQw/HhaisemMfmk (5 lines) |
| 2025-04-28 09:03:50 +0200 | <haskellbridge> | <Bowuigi> If a proof is too trivial for you, it's probably also trivial on code. Some exceptions exist depending on what you consider trivial |
| 2025-04-28 09:03:52 +0200 | <haskellbridge> | <Bowuigi> Proofs about type systems are the proofs I read the most, I like how easy it is to do those in Twelf |
| 2025-04-28 09:03:54 +0200 | <haskellbridge> | <Bowuigi> Other logics can be embedded on top by using the actual implementation as a framework, but it's not a full replacement yeah |
| 2025-04-28 09:03:56 +0200 | <haskellbridge> | <Bowuigi> (Those are independent replies from 1 to 3, in order) |
| 2025-04-28 09:03:57 +0200 | <haskellbridge> | <hellwolf> understand. i am the consumer of type systems, i try to use it for something. by too trivial proofs, i meant judging from the value where it is used |
| 2025-04-28 09:03:59 +0200 | <haskellbridge> | <hellwolf> "less run time error" is probably the "KPI" |
| 2025-04-28 09:04:01 +0200 | <haskellbridge> | <hellwolf> interesting dependent types thread... |
| 2025-04-28 09:04:02 +0200 | <haskellbridge> | What's the healthy level of proofs that you would put in Haskell? |
| 2025-04-28 09:04:04 +0200 | <haskellbridge> | <Bowuigi> Up to and including the base constructs seems good enough I guess |
| 2025-04-28 09:04:05 +0200 | <haskellbridge> | <hellwolf> - propositional logic <-> static types (?) |
| 2025-04-28 09:04:07 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/UEPByodBGyiSVOqodXeCtYPh/LKR6AzyTcQ4 (3 lines) |
| 2025-04-28 09:04:08 +0200 | <haskellbridge> | <Bowuigi> Actually dependency in user-defined ADTs is good. With base constructs I mean pi and sigma types |
| 2025-04-28 09:04:10 +0200 | <haskellbridge> | <hellwolf> From logic's perspective, is dependent type to make the quantifiers more rigour vs. in Haskell usually you hand wave it or slap a quickcheck to it for the day? |
| 2025-04-28 09:04:12 +0200 | <haskellbridge> | <Bowuigi> Yeah that's the main idea, but formalizing/verifying stuff is optional, you can use a dependently typed lang without making use of any dependent types |
| 2025-04-28 09:04:14 +0200 | <haskellbridge> | <Bowuigi> Also dependent types don't correspond to propositional logic, but rather to less mainstream logics that have more power in some places but less in others |
| 2025-04-28 09:04:16 +0200 | <haskellbridge> | <hellwolf> what is that? |
| 2025-04-28 09:04:18 +0200 | <haskellbridge> | <Bowuigi> "Everyone's bad at code" and "I like having a good mental health" are probably why we still have PL research lol |
| 2025-04-28 09:04:21 +0200 | geekosaur | wonders how long those were queued |
| 2025-04-28 09:05:40 +0200 | <haskellbridge> | <hellwolf> Heh, yea, selling DT is hard because people are lazy and handwave the proofs a way by doing it on paper or simply yolo |
| 2025-04-28 09:07:29 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) akegalj |
| 2025-04-28 09:07:33 +0200 | <haskellbridge> | <geekosaur> oh, they weren't, you were just catching up while the bot was down (system upgrade) |
| 2025-04-28 09:07:34 +0200 | <haskellbridge> | <hellwolf> But rust also shows that some technique of better managing runtime system behaviour can be appreciated. Do you consider DT and LinearTypes are orthogonal to each other as researches? |
| 2025-04-28 09:07:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 09:09:07 +0200 | <haskellbridge> | <hellwolf> Also, I think length-indexed vector is the most practical everyday stuff DT should sell hard. Like selling ADT and pattern matching to mainstream languages. |
| 2025-04-28 09:11:51 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 09:17:29 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 245 seconds) |
| 2025-04-28 09:19:10 +0200 | <c_wraith> | length-indexed vectors are very easy to understand, but actually quite awkward to use. Like... filter can have a ton of different types, and it turns out all of them are a pain to work with. |
| 2025-04-28 09:21:42 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-28 09:21:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 09:22:08 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 09:22:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2025-04-28 09:22:43 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving) |
| 2025-04-28 09:23:05 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-28 09:23:12 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
| 2025-04-28 09:28:55 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 09:31:45 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-04-28 09:32:53 +0200 | akegalj | (~akegalj@144-188.dsl.iskon.hr) |
| 2025-04-28 09:33:05 +0200 | img | (~img@user/img) img |
| 2025-04-28 09:34:53 +0200 | prdak | (~Thunderbi@user/prdak) (Quit: prdak) |
| 2025-04-28 09:34:57 +0200 | <haskellbridge> | <hellwolf> https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html#g:5 |
| 2025-04-28 09:34:57 +0200 | <haskellbridge> | I am checking this... which one is painful? I am asking unironically. |
| 2025-04-28 09:35:12 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 09:36:47 +0200 | <haskellbridge> | <hellwolf> > dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n |
| 2025-04-28 09:36:47 +0200 | <haskellbridge> | beautiful interface :p |
| 2025-04-28 09:37:12 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2025-04-28 09:37:32 +0200 | <haskellbridge> | <hellwolf> but I can see the problem of filtering. |
| 2025-04-28 09:37:53 +0200 | xelxebar | (~xelxebar@wilsonb.com) (Ping timeout: 248 seconds) |
| 2025-04-28 09:39:32 +0200 | <haskellbridge> | <hellwolf> though, I could think " filter" differently, it is a fold that adding a boolean to the original vector |
| 2025-04-28 09:39:34 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/nUqJifIEojXapRsqcNyBxQyG/SZSeSOaoePA (3 lines) |
| 2025-04-28 09:39:50 +0200 | <haskellbridge> | <hellwolf> something like that, depending the use case |
| 2025-04-28 09:43:41 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 09:43:58 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 09:44:36 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 2025-04-28 09:45:33 +0200 | xelxebar | (~xelxebar@wilsonb.com) xelxebar |
| 2025-04-28 09:46:19 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-04-28 09:46:45 +0200 | <Leary> | Cute fact about that `dfoldr`: just like with regular `foldr` on lists, you can rearrange it to get the church encoding `Vec n a` ~ `forall f. (forall m. a -> f m -> f (S m)) -> f Z -> f n`. Rare to see these for GADTs. |
| 2025-04-28 09:52:53 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 252 seconds) |
| 2025-04-28 09:53:35 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-04-28 09:53:35 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-28 09:54:24 +0200 | <haskellbridge> | <hellwolf> amazing. |
| 2025-04-28 09:54:24 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/ZXmHzkdBFkCbuBgjCCIfldSk/hI24ncMuDu0 (3 lines) |
| 2025-04-28 09:59:15 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 09:59:30 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 10:06:46 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-28 10:16:13 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 10:29:58 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-28 10:39:26 +0200 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-04-28 10:43:14 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 10:44:31 +0200 | comerijn | (~merijn@77.242.116.146) merijn |
| 2025-04-28 10:44:47 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 10:47:28 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-04-28 10:50:23 +0200 | alexherbo2 | (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2 |
| 2025-04-28 10:54:05 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639) |
| 2025-04-28 11:00:01 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 248 seconds) |
| 2025-04-28 11:01:29 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-04-28 11:01:56 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 11:02:41 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 248 seconds) |
| 2025-04-28 11:02:42 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-04-28 11:03:02 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 11:03:43 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-04-28 11:05:12 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-04-28 11:05:22 +0200 | starburst | (~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9) |
| 2025-04-28 11:05:45 +0200 | <starburst> | hello h |
| 2025-04-28 11:07:20 +0200 | <starburst> | is anyone ther? (anyone ther.. anythr,,, (echoes)) |
| 2025-04-28 11:07:29 +0200 | Digit | (~user@user/digit) (Ping timeout: 245 seconds) |
| 2025-04-28 11:09:03 +0200 | <jco> | hi hi |
| 2025-04-28 11:10:17 +0200 | FragByte | (~christian@user/fragbyte) (Quit: Quit) |
| 2025-04-28 11:12:08 +0200 | <lxsameer> | b |
| 2025-04-28 11:12:13 +0200 | FragByte | (~christian@user/fragbyte) FragByte |
| 2025-04-28 11:13:54 +0200 | <starburst> | hii |
| 2025-04-28 11:14:09 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639) (Ping timeout: 245 seconds) |
| 2025-04-28 11:14:33 +0200 | starburst | (~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9) (Quit: Client closed) |
| 2025-04-28 11:16:12 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) (Read error: Connection reset by peer) |
| 2025-04-28 11:17:20 +0200 | <prdak> | hiiii |
| 2025-04-28 11:19:34 +0200 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) werneta |
| 2025-04-28 11:21:26 +0200 | <haskellbridge> | <hellwolf> h <> repeat 'i' |
| 2025-04-28 11:27:30 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2025-04-28 11:30:56 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-04-28 11:31:38 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-04-28 11:31:40 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-04-28 11:35:14 +0200 | hellwolf | (~user@df56-1a33-0fb6-67d2-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 268 seconds) |
| 2025-04-28 11:37:46 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk |
| 2025-04-28 11:38:03 +0200 | hellwolf | (~user@0f4e-6074-8c9d-a17c-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf |
| 2025-04-28 11:39:46 +0200 | alexherbo2 | (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection) |
| 2025-04-28 11:42:11 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-28 11:42:55 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 11:46:44 +0200 | prdak | (~Thunderbi@user/prdak) (Read error: Connection reset by peer) |
| 2025-04-28 11:48:21 +0200 | alexherbo2 | (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2 |
| 2025-04-28 11:54:34 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-28 11:55:27 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 12:05:37 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-28 12:05:37 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |