Logs: freenode/#haskell
| 2020-10-23 19:26:09 | <dminuoso> | % :set -XDataKinds |
| 2020-10-23 19:26:09 | <yahb> | dminuoso: |
| 2020-10-23 19:26:13 | <dminuoso> | % data Foo = Foo Foo |
| 2020-10-23 19:26:14 | <yahb> | dminuoso: |
| 2020-10-23 19:26:18 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-23 19:26:18 | <dminuoso> | % data Foo = Foo 'Foo |
| 2020-10-23 19:26:19 | <yahb> | dminuoso: ; <interactive>:140:16: error:; * Data constructor `Foo' cannot be used here (it is defined and used in the same recursive group); * In the type 'Foo; In the definition of data constructor `Foo'; In the data declaration for `Foo' |
| 2020-10-23 19:26:34 | <blip> | Yeah, that's understandable, the compiler would loop |
| 2020-10-23 19:26:36 | <davean> | I mean you can't generate an infinite type either |
| 2020-10-23 19:27:01 | <dminuoso> | blip: Hold on, in the above, is the B supposed to have a tick or not? |
| 2020-10-23 19:27:03 | <blip> | But if I promote another constructor it's not infinite |
| 2020-10-23 19:27:07 | <blip> | yep |
| 2020-10-23 19:27:12 | <blip> | they are omittable |
| 2020-10-23 19:27:14 | <dminuoso> | blip: But that's the same example. |
| 2020-10-23 19:27:25 | <dminuoso> | Im just aksing because it could be ambgiuous without more context |
| 2020-10-23 19:27:35 | <dminuoso> | Oh, my example was poor |
| 2020-10-23 19:27:46 | <dminuoso> | % data Foo = F 'F |
| 2020-10-23 19:27:46 | <yahb> | dminuoso: ; <interactive>:141:14: error:; * Data constructor `F' cannot be used here (it is defined and used in the same recursive group); * In the type 'F; In the definition of data constructor `F'; In the data declaration for `Foo' |
| 2020-10-23 19:28:09 | <blip> | data Foo = F | X (Proxy F') |
| 2020-10-23 19:28:12 | <blip> | darn |
| 2020-10-23 19:28:16 | <dminuoso> | Note the choice of the word "group" |
| 2020-10-23 19:28:21 | <blip> | data Foo = F | X (Proxy 'F) |
| 2020-10-23 19:28:44 | <blip> | yes, I know that it doesn't work. The question is why. |
| 2020-10-23 19:29:10 | <dminuoso> | blip: Ask Richard Eisenberg? :p |
| 2020-10-23 19:29:12 | → | christo joins (~chris@81.96.113.213) |
| 2020-10-23 19:29:49 | <dminuoso> | Almost confident it's an GHC engineering problem |
| 2020-10-23 19:30:35 | <blip> | I'm solving that in a very ugly and unsafe way with Symbols |
| 2020-10-23 19:30:38 | <dminuoso> | blip: See note [Recursion and promoting data constructors] |
| 2020-10-23 19:30:50 | <dminuoso> | in compiler/GHC/Tc/TyCl.hs |
| 2020-10-23 19:30:58 | → | dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net) |
| 2020-10-23 19:31:23 | → | aarvar joins (~foewfoiew@50.35.43.33) |
| 2020-10-23 19:31:43 | <dminuoso> | Mmm that note doesnt actually contain something useful |
| 2020-10-23 19:32:14 | <dminuoso> | But perhaps this would loop the kind checker when the data declaration is checked? |
| 2020-10-23 19:32:26 | → | N3RGY joins (~N3RGY@65.141.87.122) |
| 2020-10-23 19:33:08 | × | ubert quits (~Thunderbi@p200300ecdf10db38e6b318fffe838f33.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2020-10-23 19:33:12 | <blip> | I think it would loop if you would reference the same Constructor |
| 2020-10-23 19:33:28 | <blip> | data A = B (Proxy 'B) |
| 2020-10-23 19:33:56 | <blip> | Or mutal recursion: data A = B (Proxy 'C) | C (Proxy 'B) |
| 2020-10-23 19:34:23 | <dminuoso> | blip: again, this is probably better asked in #ghc, the ghc dev mailing list or the issue tracker. :) |
| 2020-10-23 19:34:27 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-10-23 19:34:31 | × | N3RGY quits (~N3RGY@65.141.87.122) (Client Quit) |
| 2020-10-23 19:34:52 | <blip> | dminuoso: ok, thanks. I'll ponder it a bit and ask tomorrow in #ghc |
| 2020-10-23 19:35:16 | <dminuoso> | The mailing list is likely a better candidate |
| 2020-10-23 19:35:39 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-23 19:35:45 | <blip> | ok |
| 2020-10-23 19:37:10 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2020-10-23 19:40:16 | × | isovector1 quits (~isovector@172.103.216.166) (Quit: Leaving) |
| 2020-10-23 19:42:05 | × | erolm_a quits (~erolm_a@62.18.213.68) (Ping timeout: 240 seconds) |
| 2020-10-23 19:43:01 | → | erolm_a joins (~erolm_a@62.18.213.68) |
| 2020-10-23 19:45:29 | → | jbox joins (~atlas@unaffiliated/jbox) |
| 2020-10-23 19:45:38 | × | falafel quits (~falafel@71-34-132-121.clsp.qwest.net) (Ping timeout: 258 seconds) |
| 2020-10-23 19:46:42 | → | thir joins (~thir@p200300f27f19de001ce90606181a98e7.dip0.t-ipconnect.de) |
| 2020-10-23 19:47:04 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-23 19:47:50 | × | erolm_a quits (~erolm_a@62.18.213.68) (Ping timeout: 272 seconds) |
| 2020-10-23 19:48:04 | → | erolm_a joins (~erolm_a@62.18.213.68) |
| 2020-10-23 19:48:48 | × | elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Read error: Connection reset by peer) |
| 2020-10-23 19:50:45 | → | elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) |
| 2020-10-23 19:51:39 | <blip> | dminuoso: another question, is there a function Foo with following properties: `data A = B; Foo 'B = "B" :: Symbol` |
| 2020-10-23 19:52:02 | <blip> | like ShowType from the type error messages, but which returns a Symbol and not a Text |
| 2020-10-23 19:53:25 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 2020-10-23 19:53:47 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-10-23 19:54:10 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-10-23 19:55:43 | <dminuoso> | blip: There's only the bits for type errors |
| 2020-10-23 19:55:46 | × | notnatebtw quits (~nate@110.138.18.157) (Quit: WeeChat 2.9) |
| 2020-10-23 19:56:32 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2020-10-23 19:56:57 | <blip> | hm, i'll try to unsafeCoerce, perhaps it's under the hood the same |
| 2020-10-23 19:56:59 | × | Quarl quits (~Quarl@94.191.136.110.mobile.tre.se) (Read error: Connection reset by peer) |
| 2020-10-23 19:57:30 | <dminuoso> | unsafeCoerce on the type level? |
| 2020-10-23 19:57:34 | <dminuoso> | We have that? |
| 2020-10-23 19:57:37 | × | thir quits (~thir@p200300f27f19de001ce90606181a98e7.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2020-10-23 19:58:05 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2020-10-23 19:58:14 | <blip> | with proxies |
| 2020-10-23 19:59:06 | <blip> | unsafeCoerce :: KnownSymbol a => Proxy ErrorMessage -> Proxy a |
| 2020-10-23 19:59:07 | <blip> | ? |
| 2020-10-23 19:59:45 | × | alp quits (~alp@2a01:e0a:58b:4920:552d:a100:fe9e:8159) (Ping timeout: 272 seconds) |
| 2020-10-23 20:01:26 | <dminuoso> | blip: What's your intention here? |
| 2020-10-23 20:02:02 | <blip> | I want to get the name of a promoted constructor as a Symbol |
| 2020-10-23 20:02:44 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-23 20:03:00 | → | asheshambasta joins (~user@ptr-e1lysawl9rr13i61o92.18120a2.ip6.access.telenet.be) |
| 2020-10-23 20:04:01 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Remote host closed the connection) |
| 2020-10-23 20:04:08 | <ghoulguy> | To get constructors as symbols I'd expect you to have to write some TH to actually generate the code |
| 2020-10-23 20:04:45 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
| 2020-10-23 20:04:48 | <ghoulguy> | Like a: type family AsSymbol (a :: k) :: Symbol -- and then a bunch of generated instances |
| 2020-10-23 20:05:36 | <blip> | If they aren't promoted it would work via generics |
| 2020-10-23 20:06:52 | × | asheshambasta quits (~user@ptr-e1lysawl9rr13i61o92.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2020-10-23 20:06:57 | <ghoulguy> | yeah, looks like it |
| 2020-10-23 20:06:59 | <blip> | Yeah, I'd love to avoid TH |
| 2020-10-23 20:07:04 | → | notnatebtw joins (~nate@110.138.18.157) |
| 2020-10-23 20:08:15 | <ghoulguy> | >>> data T = C deriving (Generic) |
| 2020-10-23 20:08:15 | <ghoulguy> | >>> :kind! Rep T () |
| 2020-10-23 20:08:15 | <ghoulguy> | Rep T () :: * = D1 ('MetaData "T" "Ghci3" "interactive" 'False) (C1 ('MetaCons "C" 'PrefixI 'False) U1) () |
| 2020-10-23 20:08:45 | <ghoulguy> | "T" is a Symbol there |
| 2020-10-23 20:08:57 | <blip> | Yes, and "C" as well. |
| 2020-10-23 20:10:47 | → | mirrorbird joins (~psutcliff@2a00:801:42b:7891:16b1:e53f:55b2:15e1) |
| 2020-10-23 20:11:49 | → | irc_user joins (uid423822@gateway/web/irccloud.com/x-alxceqcksustqekt) |
| 2020-10-23 20:11:52 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-23 20:12:48 | × | texasmynsted quits (~texasmyns@185.240.246.92) (Remote host closed the connection) |
| 2020-10-23 20:12:50 | → | bartemius joins (~bartemius@109-252-20-20.nat.spd-mgts.ru) |
| 2020-10-23 20:13:27 | → | texasmynsted joins (~texasmyns@185.240.246.92) |
| 2020-10-23 20:14:13 | × | ggole quits (~ggole@2001:8003:8119:7200:553e:28c1:9eff:faae) (Quit: Leaving) |
All times are in UTC.