Logs: liberachat/#haskell
| 2021-08-23 21:27:47 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 240 seconds) |
| 2021-08-23 21:28:53 | <batch12> | So I can do that, and that's what I would do at the value level. But why do I need to do that here? It's already a list of types holding any type of kind * (so a heterogeneous list) |
| 2021-08-23 21:29:14 | → | megaTherion joins (~therion@coruscant.unix.io) |
| 2021-08-23 21:29:44 | <batch12> | It feels like an existential type is solving an entirely different problem |
| 2021-08-23 21:30:05 | × | ubert quits (~Thunderbi@178.165.201.23.wireless.dyn.drei.com) (Ping timeout: 250 seconds) |
| 2021-08-23 21:31:28 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.2) |
| 2021-08-23 21:32:39 | <dminuoso> | mmm |
| 2021-08-23 21:33:02 | <dminuoso> | % type T = '[Show i => i] |
| 2021-08-23 21:33:02 | <yahb> | dminuoso: ; <interactive>:17:17: error: Not in scope: type variable `i'; <interactive>:17:22: error: Not in scope: type variable `i' |
| 2021-08-23 21:33:06 | <dminuoso> | % type T = '[forall i. Show i => i] |
| 2021-08-23 21:33:07 | <yahb> | dminuoso: ; <interactive>:18:1: error:; * Illegal polymorphic type: forall i. Show i => i; GHC doesn't yet support impredicative polymorphism; * In the type synonym declaration for `T' |
| 2021-08-23 21:33:16 | <dminuoso> | batch12: ^- here. impredicativity is the issue |
| 2021-08-23 21:33:41 | <dminuoso> | being in a type list doesnt help, as under the hood its all TypeInType |
| 2021-08-23 21:33:54 | <hseg> | btw, ghci has stopped listing loaded modules recently. anyone know what's up with that? |
| 2021-08-23 21:34:43 | <dminuoso> | hseg: http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/9.0.1-notes.html#ghci |
| 2021-08-23 21:34:56 | <sm> | a long awaited ux fix |
| 2021-08-23 21:35:29 | <tomsmeding> | hseg: :set prompt "%s> " |
| 2021-08-23 21:35:45 | <dminuoso> | batch12: With quick look (9.2?), you should be able to use that in the future. |
| 2021-08-23 21:35:52 | <dminuoso> | batch12: and mind you, an existential is just an encoding of the same fact. |
| 2021-08-23 21:35:54 | <hseg> | ok, fair, has annoyed me in the past |
| 2021-08-23 21:36:11 | <hseg> | but is there a way to list all loaded modules, then? |
| 2021-08-23 21:37:17 | <dminuoso> | % :show imports -- hseg |
| 2021-08-23 21:37:18 | <yahb> | dminuoso: syntax: :show [args | prog | editor | stop | imports | modules | bindings | linker | breaks | context | packages | paths | language | targets] |
| 2021-08-23 21:37:20 | <dminuoso> | % :show imports |
| 2021-08-23 21:37:21 | <yahb> | dminuoso: import Control.Applicative; import Control.Arrow; import Control.Concurrent; import Control.Concurrent.Chan; import Control.Concurrent.MVar; import Control.Concurrent.STM; import Control.Concurrent.STM.TChan; import Control.Concurrent.STM.TVar; import Control.Comonad.Store; import Control.Exception; import Control.Exception.Lens; import Control.Monad; import Control.Monad.Cont; import Control.Monad.Except; impo |
| 2021-08-23 21:37:32 | <hseg> | awesome, thanks |
| 2021-08-23 21:37:44 | <dminuoso> | hseg: Try using the GHC manual more! It's superb :) |
| 2021-08-23 21:37:57 | <dminuoso> | One of the few manuals that are really well maintained |
| 2021-08-23 21:38:03 | <batch12> | @dminuoso Thanks. Yeah, the variant with the constraint there leads to impredicative types. But this problem doesn't have anything to do with impredicativity. Given that you can write '[Nat] there, which is a kind of constraint already, I don't see why having a type class constraint would be any different? |
| 2021-08-23 21:38:03 | <lambdabot> | Unknown command, try @list |
| 2021-08-23 21:38:12 | <hseg> | usually do! didn't find this one though |
| 2021-08-23 21:38:28 | <dminuoso> | batch12: The problem has nothing to do with the constraint, it has to do with the quantification. |
| 2021-08-23 21:38:37 | <dminuoso> | Consider: |
| 2021-08-23 21:38:43 | <dminuoso> | [forall a. a] |
| 2021-08-23 21:38:43 | <batch12> | dminuoso: but the quantification always exists even with [Nat] |
| 2021-08-23 21:38:45 | × | elf_fortrez quits (~elf_fortr@adsl-72-50-4-39.prtc.net) (Quit: Client closed) |
| 2021-08-23 21:38:53 | <dminuoso> | No, Nat is not quantified. |
| 2021-08-23 21:39:18 | <batch12> | data Carrier (is :: [Nat]); is allowing for a type list that contains any type of kind Nat |
| 2021-08-23 21:39:27 | × | pbrisbin quits (~patrick@174-081-116-011.res.spectrum.com) (Ping timeout: 240 seconds) |
| 2021-08-23 21:39:37 | <dminuoso> | batch12: The key thing here is that given `type T = [forall a. a]`, with impredicativity you are allowed to instantiate `a` at T. |
| 2021-08-23 21:39:59 | → | roboguy__ joins (~roboguy_@2605:a601:afe7:9f00:20c9:56f0:4ff9:be7b) |
| 2021-08-23 21:40:08 | → | elf_fortrez joins (~elf_fortr@adsl-72-50-6-134.prtc.net) |
| 2021-08-23 21:40:13 | <dminuoso> | batch12: but with `data All where All :: a -> All`, [All] no longer has that self referential property |
| 2021-08-23 21:40:41 | <batch12> | That's at the type level, but this is a kind annotation instead |
| 2021-08-23 21:40:55 | <dminuoso> | With TypeInType there's no difference |
| 2021-08-23 21:41:03 | <dminuoso> | We no longer have kinds |
| 2021-08-23 21:41:34 | <dminuoso> | 23:39:18 batch12 | data Carrier (is :: [Nat]); is allowing for a type list that contains any type of kind Nat |
| 2021-08-23 21:41:41 | <dminuoso> | Yes, there is still no quantification on Nat. |
| 2021-08-23 21:41:52 | × | roboguy__ quits (~roboguy_@2605:a601:afe7:9f00:20c9:56f0:4ff9:be7b) (Client Quit) |
| 2021-08-23 21:42:56 | <dminuoso> | batch12: TypeInType is on the brink of deprecation I think, because under the hood its been TypeInType for a few years even! |
| 2021-08-23 21:43:05 | × | roboguy_ quits (~roboguy_@2605:a601:afe7:9f00:5b4:1bf2:3392:8995) (Ping timeout: 250 seconds) |
| 2021-08-23 21:43:16 | <batch12> | Right, it's deprecated for PolyKinds already |
| 2021-08-23 21:43:39 | <batch12> | But I don't see why quantification is needed here at all. There should be some other approach that avoids this issue |
| 2021-08-23 21:43:45 | <dminuoso> | you want a constraint |
| 2021-08-23 21:43:57 | <dminuoso> | Which type variable do you want a constraint on? |
| 2021-08-23 21:44:13 | <dminuoso> | Or do you want a nullary constraint like |
| 2021-08-23 21:44:17 | <elf_fortrez> | Turkey? |
| 2021-08-23 21:45:04 | <batch12> | dminuoso: The answer is probably to write a type family that takes the list and provides a Constraint which enforces that they're all members of this type class |
| 2021-08-23 21:45:15 | <dminuoso> | batch12: Ohh hold on I think I misunderstood what you're trying to do. |
| 2021-08-23 21:45:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-23 21:45:56 | <dminuoso> | batch12: Wouldn't that be a lifted GADT? |
| 2021-08-23 21:46:07 | <dminuoso> | Not sure whether that is even a thing |
| 2021-08-23 21:46:26 | <dminuoso> | % :set -XDataKinds |
| 2021-08-23 21:46:26 | <yahb> | dminuoso: |
| 2021-08-23 21:46:29 | <dminuoso> | % :set -XGADTs |
| 2021-08-23 21:46:29 | <yahb> | dminuoso: |
| 2021-08-23 21:46:45 | <elf_fortrez> | kind is child in germa |
| 2021-08-23 21:46:56 | <elf_fortrez> | German |
| 2021-08-23 21:46:57 | <dminuoso> | % data F where MkF :: Num a => a -> F |
| 2021-08-23 21:46:57 | <yahb> | dminuoso: |
| 2021-08-23 21:47:07 | <elf_fortrez> | Therefore Kinder |
| 2021-08-23 21:47:11 | <dminuoso> | % :k F |
| 2021-08-23 21:47:11 | <yahb> | dminuoso: * |
| 2021-08-23 21:47:17 | <dminuoso> | % :k MkF |
| 2021-08-23 21:47:17 | <yahb> | dminuoso: ; <interactive>:1:1: error:; * Data constructor `MkF' cannot be used here (it has an unpromotable context `Num a'); * In the type `MkF' |
| 2021-08-23 21:49:22 | <monochrom> | I feel left out that all #haskell questions are now type-level programming questions. |
| 2021-08-23 21:49:45 | <dminuoso> | % data G = forall a. Num a => MkG |
| 2021-08-23 21:49:45 | <yahb> | dminuoso: ; <interactive>:14:10: error:; * Could not deduce (Num a0); from the context: Num a; bound by the type of the constructor `MkG':; forall a. Num a => G; at <interactive>:14:10-31; The type variable `a0' is ambiguous; * In the ambiguity check for `MkG'; To defer the ambiguity check to use sites, enable AllowAmbiguousTypes; In the definition of |
| 2021-08-23 21:49:50 | <monochrom> | (To clarify, I haven't studied or practiced that.) |
| 2021-08-23 21:49:56 | <dminuoso> | Uh what? |
| 2021-08-23 21:50:01 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 250 seconds) |
| 2021-08-23 21:50:03 | <dminuoso> | % :q |
| 2021-08-23 21:50:03 | <yahb> | dminuoso: |
| 2021-08-23 21:50:05 | <dminuoso> | % data G = forall a. Num a => MkG |
| 2021-08-23 21:50:06 | <yahb> | dminuoso: ; <interactive>:1:10: error:; * Could not deduce (Num a0); from the context: Num a; bound by the type of the constructor `MkG':; forall a. Num a => G; at <interactive>:1:10-31; The type variable `a0' is ambiguous; * In the ambiguity check for `MkG'; To defer the ambiguity check to use sites, enable AllowAmbiguousTypes; In the definition of d |
| 2021-08-23 21:50:34 | <dminuoso> | Oh |
| 2021-08-23 21:50:36 | <dminuoso> | % data G = forall a. Num a => MkG a |
| 2021-08-23 21:50:37 | <yahb> | dminuoso: |
| 2021-08-23 21:50:40 | <dminuoso> | % :k MkG |
| 2021-08-23 21:50:40 | <yahb> | dminuoso: ; <interactive>:1:1: error:; * Data constructor `MkG' cannot be used here (it has an unpromotable context `Num a'); * In the type `MkG' |
| 2021-08-23 21:50:54 | <dminuoso> | % class Foo (i :: k) |
| 2021-08-23 21:50:54 | <yahb> | dminuoso: |
| 2021-08-23 21:50:58 | <dminuoso> | % data G = forall a. Foo a => MkG a |
| 2021-08-23 21:50:59 | <yahb> | dminuoso: |
| 2021-08-23 21:51:01 | <dminuoso> | % :k MkG |
| 2021-08-23 21:51:02 | <yahb> | dminuoso: ; <interactive>:1:1: error:; * Data constructor `MkG' cannot be used here (it has an unpromotable context `Foo a'); * In the type `MkG' |
| 2021-08-23 21:51:06 | <monochrom> | Or I should be happy that the reason there are no more value-level programming questions is because everyone is already an expert in Haskell value-level programming. :) |
| 2021-08-23 21:51:20 | <dminuoso> | batch12: No idea. But you'd need this. |
| 2021-08-23 21:51:37 | <dminuoso> | batch12: Or, you can just wait for quick look in GHC 9.2, flip on impredicativity and enjoy the rest. |
| 2021-08-23 21:51:52 | <hseg> | monochrom: what kind of questions are you missing? |
All times are in UTC.