Newest at the top
| 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 |
| 2024-10-22 17:00:22 +0200 | <tomsmeding> | Bowuigi: that sounds reasonable, but what was the "no" for? What you say doesn't sound like it contradicts what I said :p |
| 2024-10-22 16:59:19 +0200 | <haskellbridge> | <Bowuigi> In particular, now we can get dependent kinds (sort of) |
| 2024-10-22 16:59:02 +0200 | <haskellbridge> | <Bowuigi> tomsmeding no, NoTypeInType was supposed to fix the Type :: Type inconsistency, but since Haskell was already logically inconsistent, it was deprecated because it did more harm than good |
| 2024-10-22 16:58:07 +0200 | <tomsmeding> | and it does nothing |
| 2024-10-22 16:58:01 +0200 | <famubu> | TypeInType also gives a deprecation warning. |
| 2024-10-22 16:57:00 +0200 | <geekosaur> | ahh, consistency |
| 2024-10-22 16:56:56 +0200 | <geekosaur> | looks to me like it prints "Type" but you can't use it yourself |
| 2024-10-22 16:56:54 +0200 | <yahb2> | Maybe :: Type -> Type |
| 2024-10-22 16:56:54 +0200 | <tomsmeding> | % :k Maybe |
| 2024-10-22 16:56:49 +0200 | <yahb2> | <no output> |
| 2024-10-22 16:56:49 +0200 | <tomsmeding> | % :set -XNoStarIsType |
| 2024-10-22 16:56:26 +0200 | <tomsmeding> | Bowuigi: GHC defines -XTypeInType by default, and in fact -XNoTypeInType has been unsupported for ages; perhaps this is what you were thinking of? |
| 2024-10-22 16:55:35 +0200 | <yahb2> | Maybe :: * -> * |
| 2024-10-22 16:55:35 +0200 | <tomsmeding> | % :k Maybe |
| 2024-10-22 16:53:35 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-22 16:49:35 +0200 | <haskellbridge> | <Bowuigi> Like, in the REPL |
| 2024-10-22 16:49:18 +0200 | <haskellbridge> | <Bowuigi> Wait how does Type look when you do not have Data.Kind.Type nor StarIsType? |
| 2024-10-22 16:49:04 +0200 | <famubu> | Thanks! Needed to import Data.Kind after having GADTs. |
| 2024-10-22 16:48:28 +0200 | <haskellbridge> | <Bowuigi> Ah, that makes sense |
| 2024-10-22 16:46:57 +0200 | <geekosaur> | ghc doesn't automatically define it with NoStarIsType |
| 2024-10-22 16:46:36 +0200 | <geekosaur> | you still need to import it, I think it's in Data.Kind |
| 2024-10-22 16:46:09 +0200 | <haskellbridge> | <Bowuigi> I thought GADTs enabled NoStarIsType by default tho, might have confused it with DataKinds or something |
| 2024-10-22 16:45:13 +0200 | <haskellbridge> | <Bowuigi> famubu either change Type to * or use NoStarIsType (and maybe import the actual Type kind) |
| 2024-10-22 16:37:59 +0200 | <geekosaur> | private sublibs work in most versions of cabal, it's public ones that require recent ones |
| 2024-10-22 16:37:47 +0200 | <famubu> | Error is: Not in scope: type constructor or class ‘Type’ |
| 2024-10-22 16:37:35 +0200 | <famubu> | Is there an extension that needs to be enabled? |
| 2024-10-22 16:37:28 +0200 | <famubu> | I'm getting error at the `Type` part. |
| 2024-10-22 16:37:19 +0200 | <famubu> | Hi. When using GADTs extension, it is possible to have like `data NewType :: Ty -> Type where ...`, right? Where `Ty` is another type. |
| 2024-10-22 16:36:31 +0200 | famubu | (~julinuser@user/famubu) famubu |