Logs: liberachat/#haskell
| 2021-07-09 11:35:19 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-07-09 11:37:34 | → | warnz joins (~warnz@2600:1700:77c0:5610:edd9:472d:4b89:9ab8) |
| 2021-07-09 11:40:03 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-09 11:42:03 | × | warnz quits (~warnz@2600:1700:77c0:5610:edd9:472d:4b89:9ab8) (Ping timeout: 252 seconds) |
| 2021-07-09 11:45:38 | × | azeem quits (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-07-09 11:46:35 | → | epolanski joins (uid312403@id-312403.brockwell.irccloud.com) |
| 2021-07-09 11:58:05 | × | jippiedoe quits (~david@2a02-a44c-e14e-1-e2b1-5b1f-ad9a-57c9.fixed6.kpn.net) (Ping timeout: 255 seconds) |
| 2021-07-09 11:59:04 | → | dunj3 joins (~dunj3@2001:16b8:30aa:f100:5749:57d0:4660:97ec) |
| 2021-07-09 11:59:57 | → | acidjnk_new joins (~acidjnk@p200300d0c72b9550509afe7c5cdd8ef5.dip0.t-ipconnect.de) |
| 2021-07-09 12:00:23 | <AWizzArd> | dminuoso: have you implemented Single Sign-On? |
| 2021-07-09 12:01:30 | <dminuoso> | No. |
| 2021-07-09 12:03:02 | × | acidjnk quits (~acidjnk@p200300d0c72b9563509afe7c5cdd8ef5.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2021-07-09 12:03:23 | → | coeus joins (~coeus@b2b-92-50-96-34.unitymedia.biz) |
| 2021-07-09 12:05:42 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 252 seconds) |
| 2021-07-09 12:06:50 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-09 12:07:33 | <viluon> | hello, I have a question about generics-sop again. In pretty-sop's function `prettyValFor`, in the second equation, there's an auxiliary map for infix constructors (https://github.com/well-typed/pretty-sop/blob/master/src/Generics/SOP/PrettyVal.hs#L42-L45). It has the type `forall x y. NP (K Value) '[x, y] -> Value`, but is seemingly applied in a context where it is not known that `xs ~ '[x, y]`. How come this typechecks? |
| 2021-07-09 12:08:05 | × | phma quits (phma@2001:5b0:211c:858:db7c:9aeb:2bd8:1b08) (Read error: Connection reset by peer) |
| 2021-07-09 12:08:25 | <viluon> | I thought the `xs ~ '[x, y]` equivalence came as a consequence of pattern-matching on the `Infix` constructor of `ConstructorInfo`, but `ConstructorInfo` is not a GADT |
| 2021-07-09 12:11:55 | × | fluffyballoon quits (~fluffybal@199.204.58.62) (Ping timeout: 246 seconds) |
| 2021-07-09 12:12:51 | → | Pickchea joins (~private@user/pickchea) |
| 2021-07-09 12:15:00 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-07-09 12:15:21 | × | anandprabhu quits (~anandprab@94.202.243.198) (Quit: Leaving) |
| 2021-07-09 12:17:59 | → | azeem joins (~azeem@dynamic-adsl-84-220-226-129.clienti.tiscali.it) |
| 2021-07-09 12:23:11 | → | lortabac joins (~lortabac@95.138.56.124) |
| 2021-07-09 12:24:45 | → | phma joins (phma@2001:5b0:212a:c338:e904:270b:aa2b:a4ce) |
| 2021-07-09 12:31:03 | <kosmikus> | viluon: `ConstructorInfo` *is* a GADT. |
| 2021-07-09 12:31:18 | <kosmikus> | viluon: what makes you think otherwise? |
| 2021-07-09 12:31:40 | <viluon> | oh, am I confused? I'm probably confused https://hackage.haskell.org/package/generics-sop-0.5.1.1/docs/src/Generics.SOP.Type.Metadata.html#ConstructorInfo |
| 2021-07-09 12:31:55 | <kosmikus> | ah |
| 2021-07-09 12:32:17 | <kosmikus> | that explains your confusion indeed |
| 2021-07-09 12:32:23 | <kosmikus> | the right definition is here: https://hackage.haskell.org/package/generics-sop-0.5.1.1/docs/src/Generics.SOP.Metadata.html#ConstructorInfo |
| 2021-07-09 12:32:44 | <kosmikus> | generics-sop has two methods of providing metadata |
| 2021-07-09 12:32:53 | <kosmikus> | one is that metadata is a term-level structure |
| 2021-07-09 12:33:07 | <kosmikus> | the datatypes for this are defined in `Generics.SOP.Metadata` |
| 2021-07-09 12:33:15 | <kosmikus> | (and have the GADT) |
| 2021-07-09 12:33:24 | <viluon> | haha, that's mightily confusing. Thanks for clearing it up! |
| 2021-07-09 12:33:25 | <kosmikus> | this is what's being used by `pretty-sop`. |
| 2021-07-09 12:33:38 | <kosmikus> | the other is that the entire metadata can be lifted to the type-level. |
| 2021-07-09 12:33:48 | <kosmikus> | and that uses "simple" datatypes. |
| 2021-07-09 12:33:59 | <kosmikus> | primarily because there was a time when GADTs could not be promoted. |
| 2021-07-09 12:34:20 | <kosmikus> | this is no longer the case. it might be worth exploring whether the two could be unified better. |
| 2021-07-09 12:35:15 | <kosmikus> | but then again, even though GADTs can be lifted now, the type-level programming world is still different from the term-level programming world, so promoted GADTs don't quite behave as one might expect of GADTs. |
| 2021-07-09 12:35:35 | <Gurkenglas_> | Is there a language that compiles to python, has IDE support, and is more like Haskell? |
| 2021-07-09 12:35:39 | Gurkenglas_ | is now known as Gurkenglas |
| 2021-07-09 12:36:18 | <viluon> | Gurkenglas haven't tried, but I heard of https://github.com/evhub/coconut |
| 2021-07-09 12:36:30 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 252 seconds) |
| 2021-07-09 12:36:36 | <darklambda> | how's coconut these days? |
| 2021-07-09 12:36:38 | <kosmikus> | Idris typically has backends for everything, but not necessarily backends of a very robust quality. |
| 2021-07-09 12:37:14 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-09 12:38:10 | <viluon> | if I had a nickel every time I'm confused about something that would be cleared up by jump-to-definition, I would have at least one nickel today |
| 2021-07-09 12:38:33 | <viluon> | HLS is wonderful but I wish it could jump to hackage sources as well |
| 2021-07-09 12:39:07 | <kosmikus> | perhaps that will be possible some day. |
| 2021-07-09 12:39:26 | <kosmikus> | HLS is evolving so quickly, it's amazing. |
| 2021-07-09 12:39:50 | <Gurkenglas> | could you download acme-everything and just goto definition? |
| 2021-07-09 12:40:13 | × | ukari quits (~ukari@user/ukari) (Remote host closed the connection) |
| 2021-07-09 12:40:14 | <dminuoso> | acme-everything sadly doesn't build, and quchen is too lazy to fix it. |
| 2021-07-09 12:40:27 | <dminuoso> | We ought to start a petition. |
| 2021-07-09 12:40:48 | → | ukari joins (~ukari@user/ukari) |
| 2021-07-09 12:41:20 | → | pbrisbin joins (~patrick@pool-173-49-147-28.phlapa.fios.verizon.net) |
| 2021-07-09 12:42:10 | <Gurkenglas> | the problem is that when you import lens and build your package goto definition doesnt work on lens, right? shouldnt it be possible to tell cabal/stack to put all the source in the local folder before building it? |
| 2021-07-09 12:42:13 | × | pbrisbin quits (~patrick@pool-173-49-147-28.phlapa.fios.verizon.net) (Client Quit) |
| 2021-07-09 12:44:45 | → | pbrisbin joins (~patrick@pool-173-49-147-28.phlapa.fios.verizon.net) |
| 2021-07-09 12:47:27 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-07-09 12:48:26 | <fendor> | iirc, with a bit of hacking, you can goto hackage libs with hls |
| 2021-07-09 12:48:33 | → | rostero joins (uid236576@id-236576.tooting.irccloud.com) |
| 2021-07-09 12:48:51 | <fendor> | it's not stable yet, though |
| 2021-07-09 12:49:43 | × | jneira quits (~jneira@212.8.115.226) (Quit: Client closed) |
| 2021-07-09 12:51:20 | <Gurkenglas> | you mean, the required hacking is likely to change in the future so it's not worth adding it as a command to stack and hls? |
| 2021-07-09 12:51:54 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 252 seconds) |
| 2021-07-09 12:52:12 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-09 12:53:34 | <fendor> | yep |
| 2021-07-09 12:53:40 | <fendor> | based on hie files, iirc |
| 2021-07-09 12:54:08 | × | fef quits (~thedawn@user/thedawn) (Remote host closed the connection) |
| 2021-07-09 13:01:03 | → | fluffyballoon joins (~fluffybal@pat-verona-i.epic.com) |
| 2021-07-09 13:01:15 | → | alx741 joins (~alx741@186.178.108.75) |
| 2021-07-09 13:03:48 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-07-09 13:06:17 | → | zebrag joins (~chris@user/zebrag) |
| 2021-07-09 13:15:46 | × | hendursa1 quits (~weechat@user/hendursaga) (Quit: hendursa1) |
| 2021-07-09 13:16:47 | → | hendursaga joins (~weechat@user/hendursaga) |
| 2021-07-09 13:19:35 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-07-09 13:21:52 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 2021-07-09 13:22:11 | → | biberu joins (~biberu@user/biberu) |
| 2021-07-09 13:22:14 | × | statusbot quits (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Remote host closed the connection) |
| 2021-07-09 13:22:29 | → | statusbot joins (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) |
| 2021-07-09 13:24:25 | × | pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-57-65-92-163-194.dsl.bell.ca) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-07-09 13:24:43 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-57-65-92-163-194.dsl.bell.ca) |
| 2021-07-09 13:24:54 | × | viluon quits (uid453725@id-453725.brockwell.irccloud.com) (Ping timeout: 252 seconds) |
| 2021-07-09 13:25:27 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 252 seconds) |
| 2021-07-09 13:25:32 | → | viluon joins (uid453725@id-453725.brockwell.irccloud.com) |
| 2021-07-09 13:26:00 | × | ishutin_ quits (~ishutin@87-97-88-250.pool.digikabel.hu) (Ping timeout: 252 seconds) |
| 2021-07-09 13:26:24 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-07-09 13:26:45 | → | ishutin joins (~ishutin@87-97-88-250.pool.digikabel.hu) |
| 2021-07-09 13:27:18 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:44e3:e9f0:ea4d:f039) |
| 2021-07-09 13:28:00 | × | Katarushisu quits (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 2021-07-09 13:28:18 | → | Katarushisu joins (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net) |
| 2021-07-09 13:29:36 | × | kuribas quits (~user@ptr-25vy0i8xkirhfn6k3n1.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2021-07-09 13:30:02 | → | kuribas joins (~user@ptr-25vy0i8xkirhfn6k3n1.18120a2.ip6.access.telenet.be) |
| 2021-07-09 13:30:24 | × | typedfern_ quits (~Typedfern@185.red-83-57-142.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 2021-07-09 13:31:38 | → | warnz joins (~warnz@2600:1700:77c0:5610:edd9:472d:4b89:9ab8) |
| 2021-07-09 13:31:41 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:44e3:e9f0:ea4d:f039) (Ping timeout: 255 seconds) |
All times are in UTC.