Newest at the top
| 2024-10-07 16:17:30 +0200 | <EvanR> | what a mess |
| 2024-10-07 16:16:18 +0200 | <dolio> | (Despite that not being the thing that ImpredicativeTypes enables.) |
| 2024-10-07 16:15:48 +0200 | <fr33domlover> | o/ Given some type `a`, is there a way to get a unique `(s :: Symbol)` that represents type `a`? Kind of like a type-level Show/Unique |
| 2024-10-07 16:15:44 +0200 | <dolio> | GHC is impredicative in the type theory sense once you allow data types that have `forall` in the types of fields. |
| 2024-10-07 16:14:13 +0200 | synchromesh | (~john@2406:5a00:241a:5600:1537:bb1c:ebe9:2fdf) synchromesh |
| 2024-10-07 16:13:49 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-10-07 16:13:18 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-10-07 16:13:11 +0200 | <haskellbridge> | <Bowuigi> Haskell already was inconsistent because you have access to general recursion and to undefined (bottom) |
| 2024-10-07 16:12:46 +0200 | synchromesh | (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) (Read error: Connection reset by peer) |
| 2024-10-07 16:12:45 +0200 | <dolio> | (And not being New Foundations, I suppose.) |
| 2024-10-07 16:12:25 +0200 | <dolio> | Like having a set of all sets. |
| 2024-10-07 16:12:03 +0200 | <dolio> | Type :: Type is more than impredicative. It's is outright inconsistent. |
| 2024-10-07 16:11:31 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 264 seconds) |
| 2024-10-07 16:10:38 +0200 | <Duste3> | Since Type :: Type then Haskell would be considered Impredicative? (and so its inconsistent as a theorem prover) |
| 2024-10-07 16:07:33 +0200 | Leonard26 | (~Leonard26@49.236.8.9) (Quit: Client closed) |
| 2024-10-07 16:05:56 +0200 | mari-estel | (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) (Ping timeout: 265 seconds) |
| 2024-10-07 16:00:52 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 2024-10-07 15:57:54 +0200 | <EvanR> | so by definition they seem to be different |
| 2024-10-07 15:57:45 +0200 | <EvanR> | the question seemed to be if "Kinds" as a conversational category of things "is the same thing" as "Type 1" which is a type, and has type Type 2 |
| 2024-10-07 15:55:43 +0200 | <EvanR> | there's no Type 1 |
| 2024-10-07 15:55:31 +0200 | <EvanR> | Type :: Type |
| 2024-10-07 15:55:29 +0200 | <EvanR> | but also |
| 2024-10-07 15:55:22 +0200 | <EvanR> | Char :: Type |
| 2024-10-07 15:54:52 +0200 | mari-estel | (~mari-este@2a02:3032:304:651c:216:3eff:fe65:4eef) |
| 2024-10-07 15:52:34 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 15:40:57 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-07 15:40:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 15:40:11 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2 |
| 2024-10-07 15:39:52 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection) |
| 2024-10-07 15:37:34 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-10-07 15:29:59 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:29:37 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 15:29:33 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 2024-10-07 15:27:20 +0200 | <Duste3> | Ok thanks |
| 2024-10-07 15:22:52 +0200 | <tomsmeding> | (it's also inconsistent as a theorem prover for a bunch of other reasons) |
| 2024-10-07 15:22:30 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-10-07 15:22:05 +0200 | <tomsmeding> | but do note that Haskell is inconsistent when viewed as a theorem prover, because Type \in Type (where Type is the kind of types that can hold values, sometimes written *) |
| 2024-10-07 15:21:54 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) NinjaTrappeur |
| 2024-10-07 15:20:47 +0200 | <tomsmeding> | not sure about the precise numbering of the universe levels, but it indeed corresponds to one universe level higher than types |
| 2024-10-07 15:20:26 +0200 | <tomsmeding> | Duste3: values have types, and types have kinds |
| 2024-10-07 15:20:19 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.4.2) |
| 2024-10-07 15:18:21 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:16:42 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:16:36 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 15:14:49 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 15:13:03 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 15:09:11 +0200 | Typedfern | (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) |
| 2024-10-07 15:08:30 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 2024-10-07 15:07:29 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 15:06:57 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |