Newest at the top
2024-10-22 17:47:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-10-22 17:46:49 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 260 seconds) |
2024-10-22 17:46:34 +0200 | kaskal | (~kaskal@213-225-13-57.nat.highway.a1.net) kaskal |
2024-10-22 17:46:27 +0200 | <geekosaur> | interesting. not even an extension? (I think Chrome has an extension for fancy encoding defaults including per-site defaults) |
2024-10-22 17:45:34 +0200 | <mauke> | geekosaur: apparently firefox defaults to latin-1 in the absence of any encoding information and there is no way to change that default |
2024-10-22 17:44:44 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2024-10-22 17:43:11 +0200 | <dolio> | Yeah, that version uses a data type, which makes it easier. |
2024-10-22 17:42:55 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2024-10-22 17:42:40 +0200 | euleritian | (~euleritia@dynamic-176-006-135-055.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2024-10-22 17:41:44 +0200 | Square2 | (~Square4@user/square) Square |
2024-10-22 17:41:29 +0200 | kaskal | (~kaskal@213-225-13-57.nat.highway.a1.net) (Quit: ZNC - https://znc.in) |
2024-10-22 17:39:20 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 272 seconds) |
2024-10-22 17:38:28 +0200 | <geekosaur> | lol |
2024-10-22 17:38:27 +0200 | euleritian | (~euleritia@dynamic-176-006-135-055.176.6.pool.telefonica.de) |
2024-10-22 17:37:56 +0200 | <mauke> | haha, the "repair text encoding" menu entry fixes the display in firefox, but then it immediately asks me if I want to translate the page from Greek to English |
2024-10-22 17:37:29 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
2024-10-22 17:37:28 +0200 | ash3en1 | ash3en |
2024-10-22 17:37:27 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
2024-10-22 17:36:15 +0200 | ash3en1 | (~Thunderbi@146.70.124.222) ash3en |
2024-10-22 17:34:30 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-10-22 17:33:51 +0200 | <geekosaur> | I'm a bit busy today but I'll file a bug upstream if there isn't one already (serving pastebins is new; it used to hand that off to Synapse but that was disabled recently) |
2024-10-22 17:32:45 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2024-10-22 17:32:41 +0200 | <geekosaur> | hm, it renders okay here. browser settings? |
2024-10-22 17:29:15 +0200 | twistedparity | (~twistedpa@mobile-access-2e8454-108.dhcp.inet.fi) |
2024-10-22 17:19:34 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
2024-10-22 17:18:44 +0200 | <haskellbridge> | <Bowuigi> That is how type theory felt at first lmao |
2024-10-22 17:17:52 +0200 | <mauke> | it's served with no encoding |
2024-10-22 17:17:45 +0200 | <mauke> | https://kf8nh.com/_heisenbridge/media/kf8nh.com/JmsRildBqQawmqczaGKzvBaA/0Vl4TQmPlUs RIP unicode |
2024-10-22 17:15:48 +0200 | CiaoSen | (~Jura@2a05:5800:20b:3a00:ca4b:d6ff:fec1:99da) (Ping timeout: 245 seconds) |
2024-10-22 17:13:15 +0200 | <haskellbridge> | <Bowuigi> Yeah definitely, TypeInType is better for this use case |
2024-10-22 17:12:30 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/JmsRildBqQawmqczaGKzvBaA/0Vl4TQmPlUs (27 lines) |
2024-10-22 17:12:30 +0200 | <haskellbridge> | <Bowuigi> {-# OPTIONS --type-in-type #-} |
2024-10-22 17:12:27 +0200 | <dolio> | Anyhow, it doesn't really matter, because that would be the most difficult way to write a fixpoint operator in Haskell. |
2024-10-22 17:09:03 +0200 | <haskellbridge> | <Bowuigi> https://ionathan.ch/2021/11/24/inconsistencies.html this explains many inconsistencies better than I can rn, Girard-Russell is the first one |
2024-10-22 17:07:05 +0200 | <dolio> | It's not super easy to come up with the right terms just from Type : Type. Less easy than in set theory. It's somehwat easier if you allow other features than just functions, I think. |
2024-10-22 17:06:07 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
2024-10-22 17:05:41 +0200 | <geekosaur> | oh okay, shows what I know 😛 |
2024-10-22 17:05:03 +0200 | <haskellbridge> | <Bowuigi> No wait the Russell paradox doesn't need a Cubical Type Theory |
2024-10-22 17:04:56 +0200 | <tomsmeding> | ¯\_(ツ)_/¯ |
2024-10-22 17:04:55 +0200 | <dolio> | No, cubical agda is something else. |
2024-10-22 17:04:25 +0200 | <geekosaur> | (Cubical Agda, which IIRC allows it access to the whole lambda cube) |
2024-10-22 17:04:18 +0200 | Guest19 | (~Guest19@lewi-30-b2-v4wan-168203-cust232.vm4.cable.virginm.net) (Client Quit) |
2024-10-22 17:04:08 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
2024-10-22 17:04:02 +0200 | <geekosaur> | tomsmeding, correct. even in Agda you need to do extra work to observe it |
2024-10-22 17:03:57 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2024-10-22 17:03:31 +0200 | <geekosaur> | NoTypeInType was removed because it was becoming too hard to support it while moving forward on Dependent Haskell |
2024-10-22 17:03:26 +0200 | <tomsmeding> | oh isn't it? I tried to reproduce it in haskell a while back but I couldn't do it, sounds like that is expected |
2024-10-22 17:02:59 +0200 | <geekosaur> | Bouwigi, NoTypeInType is how ghc used to work. but ghc went the quasi-dependent-types direction, thus TypeInType. (The inconsistency isn't observable in Haskell, but I've seen an Agda proof case for it.) |
2024-10-22 17:00:55 +0200 | Guest19 | (~Guest19@lewi-30-b2-v4wan-168203-cust232.vm4.cable.virginm.net) |
2024-10-22 17:00:36 +0200 | <tomsmeding> | oh that it was the thing you were thinking of I guess |