Newest at the top
| 2024-10-07 16:27:59 +0200 | <dolio> | Yeah. I don't think you can even manually instantiate without ImpredicativeTypes, though. |
| 2024-10-07 16:26:57 +0200 | <haskellbridge> | <Bowuigi> Also type inference (ala HM, inferring type applications and abstractions) in impredicative system F is undecidable IIRC, it makes sense that GHC is a bit conservative just in casd |
| 2024-10-07 16:26:21 +0200 | <dolio> | There's sort of a similar situation, where type families/aliases are reported to have some kind, but you can't use them everywhere things of that kind are expected. |
| 2024-10-07 16:25:19 +0200 | <haskellbridge> | <Bowuigi> Impredicativity just means "something that contains itself" so that checks out I guess |
| 2024-10-07 16:25:07 +0200 | ljdarj1 | ljdarj |
| 2024-10-07 16:25:06 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2024-10-07 16:24:56 +0200 | <dolio> | The impredicativity is that `forall a. ...` has kind Type despite quantifying over Type. However, by default, GHC does this weird thing where even though that quantified type supposedly has kind Type, you can't use it everywhere something of kind Type is expected. |
| 2024-10-07 16:23:05 +0200 | <dolio> | It's not really two different things. GHC just divides them up strangely. |
| 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 |