Newest at the top
| 2024-10-07 17:14:37 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 17:14:08 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-10-07 17:12:49 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 17:12:49 +0200 | Pixi` | Pixi |
| 2024-10-07 17:12:09 +0200 | mari-estel | (~mari-este@185.238.219.77) () |
| 2024-10-07 17:02:10 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 17:00:06 +0200 | Duste3 | (~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) (Remote host closed the connection) |
| 2024-10-07 16:59:47 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-10-07 16:58:23 +0200 | benjaminl | (~benjaminl@user/benjaminl) benjaminl |
| 2024-10-07 16:57:59 +0200 | benjaminl | (~benjaminl@user/benjaminl) (Ping timeout: 252 seconds) |
| 2024-10-07 16:50:29 +0200 | mari-estel | (~mari-este@185.238.219.77) |
| 2024-10-07 16:50:06 +0200 | Pixi | (~Pixi@user/pixi) (Ping timeout: 244 seconds) |
| 2024-10-07 16:48:33 +0200 | Pixi` | (~Pixi@user/pixi) Pixi |
| 2024-10-07 16:47:05 +0200 | <lortabac> | but depending on what you are trying to achieve you may not actually need this |
| 2024-10-07 16:46:34 +0200 | <lortabac> | maybe you can use the qualified type name as a Symbol with TemplateHaskell |
| 2024-10-07 16:44:23 +0200 | <lortabac> | fr33domlover: can I ask you what your goal is? |
| 2024-10-07 16:41:57 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-07 16:41:00 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 16:37:05 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-10-07 16:34:30 +0200 | spew | (~spew@201.141.99.170) spew |
| 2024-10-07 16:32:08 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 16:31:49 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 2024-10-07 16:31:02 +0200 | <haskellbridge> | <Bowuigi> The type family/type alias issue happens because they are supposed to be fully saturated (exceptions exist) as to avoid going to System F omega and further complicating GHC |
| 2024-10-07 16:29:51 +0200 | <haskellbridge> | <Bowuigi> Perhaps a bit too conservative there |
| 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) |