Newest at the top
| 2024-10-07 16:22:23 +0200 | <haskellbridge> | <Bowuigi> Duste3 /dolio Yeah there are two kinds of impredicativity. One is having an "impredicative universe" (which is the case with Type) and the other is being able to instance type variables to types with foralls |
| 2024-10-07 16:21:22 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 16:21:16 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 16:19:14 +0200 | diod | (~diod@142.188.102.4) () |
| 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) |