Logs: liberachat/#haskell
| 2021-08-13 20:41:21 | → | azeem joins (~azeem@176.200.230.183) |
| 2021-08-13 20:41:33 | → | jgeerds joins (~jgeerds@55d45555.access.ecotel.net) |
| 2021-08-13 20:41:34 | → | krjst joins (~krjst@2604:a880:800:c1::16b:8001) |
| 2021-08-13 20:41:40 | <hololeap> | I'm having a hard time figuring out why the type system thinks there's an ambiguous variable here: http://sprunge.us/L7lj5i |
| 2021-08-13 20:42:44 | <hololeap> | I used ScopedTypeVariables and littered it with enough type information that it should be able to figure it out, I would think |
| 2021-08-13 20:44:01 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-13 20:44:19 | × | chisui quits (~chisui@200116b8642cd800d092c544b616cc73.dip.versatel-1u1.de) (Ping timeout: 246 seconds) |
| 2021-08-13 20:46:06 | → | norias joins (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-08-13 20:47:44 | → | oats joins (~thomas@user/oats) |
| 2021-08-13 20:49:25 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2021-08-13 20:50:41 | × | norias quits (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2021-08-13 20:51:16 | → | zyklotomic joins (~ethan@2604:a880:800:10::79f:8001) |
| 2021-08-13 20:51:16 | <falsifian> | hololeap: What error do you see? I'm not sure where to look. |
| 2021-08-13 20:51:38 | <falsifian> | hololeap: Oops, I see it's in the comment at the bottom |
| 2021-08-13 20:51:57 | → | heath joins (~heath@user/heath) |
| 2021-08-13 20:52:26 | <hololeap> | yeah. what I'm trying to do is a little unusual so I may have confused myself |
| 2021-08-13 20:52:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-13 20:53:17 | → | energizer joins (~energizer@user/energizer) |
| 2021-08-13 20:55:19 | → | aravk joins (~aravk@user/aravk) |
| 2021-08-13 20:56:41 | → | norias joins (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-08-13 20:57:08 | <falsifian> | I haven't fully understood your function, but shouldn't the output of applyExtraArgs have type r, rather than WithExtraArgs as r? |
| 2021-08-13 20:57:22 | <falsifian> | I thought the point is to apply the extra arguments, so you get the resulting r value |
| 2021-08-13 20:58:36 | <hololeap> | the final output _is_ r, since WithExtraArgs eventually results in r |
| 2021-08-13 20:59:40 | <falsifian> | hololeap: Say as is [Int, Int] and r is Char. Your function is taking an ExtraArgsSing [Int, Int], and a WithExtraArgs as r (which is Int -> Int -> Char I think), and returning a (Int -> Int -> Char) |
| 2021-08-13 20:59:49 | <falsifian> | According to the type signature for applyExtraArgs |
| 2021-08-13 20:59:52 | <falsifian> | I'd expect it to return just Char |
| 2021-08-13 21:00:22 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 268 seconds) |
| 2021-08-13 21:00:22 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 268 seconds) |
| 2021-08-13 21:00:29 | <falsifian> | Did you mean to write ... -> WithExtraArgs as' r? |
| 2021-08-13 21:00:38 | <falsifian> | or something like that |
| 2021-08-13 21:00:53 | <hololeap> | well, there needs to be a way for the caller of applyExtraArgs to pass in the arguments |
| 2021-08-13 21:01:37 | <hololeap> | so in your example, the applyExtraArgs would become: ExtraArgsSing '[Int,Int] -> (Int -> Int -> Char) -> Int -> Int -> Char |
| 2021-08-13 21:02:00 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-08-13 21:02:12 | × | xff0x quits (~xff0x@2001:1a81:5278:5300:7b4f:e6f2:6a79:44e0) (Ping timeout: 245 seconds) |
| 2021-08-13 21:02:17 | <falsifian> | I'm confused. Could you just write applyExtraArgs _ x = x? |
| 2021-08-13 21:02:45 | <falsifian> | As the definition for the function |
| 2021-08-13 21:03:12 | <falsifian> | (Before, I was thinking an ExtraArgsSing as actually includes the a values, but I guess it doesn't.) |
| 2021-08-13 21:03:17 | <hololeap> | that's what the case for the empty type-level list does: applyExtraArgs NoExtraArgs x = x |
| 2021-08-13 21:03:17 | → | xff0x joins (~xff0x@2001:1a81:5278:5300:e19e:51f3:462a:7dce) |
| 2021-08-13 21:03:37 | <falsifian> | hololeap: But wouldn't my definition satisfy the type signature you wrote? |
| 2021-08-13 21:04:04 | <falsifian> | Can you give an example of how withExtraArgs could be used? |
| 2021-08-13 21:04:24 | <hololeap> | hm, maybe I'm overcomplicating it... |
| 2021-08-13 21:06:00 | → | burnsidesLlama joins (~burnsides@client-8-91.eduroam.oxuni.org.uk) |
| 2021-08-13 21:06:41 | × | fabfianda quits (~fabfianda@mob-5-91-126-104.net.vodafone.it) (Ping timeout: 248 seconds) |
| 2021-08-13 21:07:05 | <hololeap> | falsifian: for example: f :: WithExtraArgs '[Int,Int] Char ; applyExtraArgs f 3 4 :: Char |
| 2021-08-13 21:07:14 | → | fabfianda joins (~fabfianda@37.183.255.57) |
| 2021-08-13 21:08:49 | × | kor1 quits (~kor1@user/kor1) (Ping timeout: 248 seconds) |
| 2021-08-13 21:09:25 | ← | jao parts (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) () |
| 2021-08-13 21:09:37 | × | dmwit quits (~dmwit@pool-108-28-26-143.washdc.fios.verizon.net) (Ping timeout: 268 seconds) |
| 2021-08-13 21:09:54 | <hololeap> | anyway, the reason why it's this complicated is because I need to expand on this idea so that I can have a nested structure, where the extra args are passed down to the children that need them. |
| 2021-08-13 21:10:25 | × | burnsidesLlama quits (~burnsides@client-8-91.eduroam.oxuni.org.uk) (Ping timeout: 258 seconds) |
| 2021-08-13 21:11:11 | → | dmwit joins (~dmwit@pool-108-28-26-143.washdc.fios.verizon.net) |
| 2021-08-13 21:12:21 | <hololeap> | there will need to be a value-level witness of the type-level rose tree that will be involved, so that the apply function knows which child to pass the argument to |
| 2021-08-13 21:12:32 | <hololeap> | it's like the santa claus of functional programming |
| 2021-08-13 21:13:32 | → | spaceshipnow joins (~spaceship@75-164-208-223.ptld.qwest.net) |
| 2021-08-13 21:13:41 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-08-13 21:13:55 | <monochrom> | and the children live in tree houses built throughout the christmas tree... |
| 2021-08-13 21:15:11 | × | spaceshipnow quits (~spaceship@75-164-208-223.ptld.qwest.net) (Client Quit) |
| 2021-08-13 21:21:37 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 248 seconds) |
| 2021-08-13 21:23:40 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-13 21:23:51 | → | pfurla joins (~pfurla@ool-3f8fcb0f.dyn.optonline.net) |
| 2021-08-13 21:25:14 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2021-08-13 21:27:01 | <hololeap> | I think I understand why GHC is getting confused... it doesn't have a way to know that `WithExtraArgs '[Int, Int] r` and `WithExtraArgs '[Int] r` are talking about the same 'r' |
| 2021-08-13 21:27:24 | × | pfurla_ quits (~pfurla@ool-3f8fcb0f.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 2021-08-13 21:28:32 | <hololeap> | and I don't know how to assure it of that. WithExtraArgs cannot be injective, since there is no specific relationship between the arguments and 'r' |
| 2021-08-13 21:30:13 | <hololeap> | so I might have to pass in the arguments as a single data structure instead |
| 2021-08-13 21:31:19 | <falsifian> | hololeap: I don't really understand your end goal, but I wonder if it really requires all this type-level trickery. |
| 2021-08-13 21:31:35 | <falsifian> | Do you have an example of how it would be used, if you got it working? |
| 2021-08-13 21:32:14 | <hololeap> | I'd have to show you the end product and then you could decide if it's necessary or not. there's too much to explain |
| 2021-08-13 21:32:33 | <falsifian> | hololeap: Sounds like you're on a fun adventure :) |
| 2021-08-13 21:33:11 | <hololeap> | heh |
| 2021-08-13 21:36:05 | <hololeap> | the best I can do to sum it up is: there is a typeclass that defines a form field, and this form field may have children attached as a type family FieldChildTypes |
| 2021-08-13 21:36:43 | <hololeap> | the children have a state that remembers if they have been filled and if they are valid, which is passed up through the tree to their ancestors |
| 2021-08-13 21:37:19 | <hololeap> | there is also a render function for this typeclass, but occasionally the render function needs extra arguments passed to it, due to the way the rendering system works |
| 2021-08-13 21:37:48 | <hololeap> | so rendering an ancestor will require passing in extra arguments for all the decendents that need them... |
| 2021-08-13 21:39:18 | × | stefan-_ quits (~cri@42dots.de) (Ping timeout: 256 seconds) |
| 2021-08-13 21:39:48 | <hololeap> | so there is also a FieldExtraArgs type family within this typeclass which holds the extra arguments needed to render, if there are any |
| 2021-08-13 21:40:32 | <hololeap> | and then I need a way to apply them, hence my attempt to make way to have a dynamic number of arguments for a function |
| 2021-08-13 21:41:41 | <hololeap> | hope that makes sense |
| 2021-08-13 21:42:08 | <falsifian> | hololeap: That sounds like a lot to think about. All I can suggest for now is: have you studied how printf works? |
| 2021-08-13 21:42:33 | <falsifian> | Other than that it's beyond me :) |
| 2021-08-13 21:42:41 | <hololeap> | falsifian: that's a good idea |
| 2021-08-13 21:43:23 | × | retroid_ quits (~retro@5ec19a54.skybroadband.com) (Ping timeout: 258 seconds) |
| 2021-08-13 21:43:26 | → | stefan-_ joins (~cri@42dots.de) |
| 2021-08-13 21:43:27 | → | econo joins (uid147250@user/econo) |
| 2021-08-13 21:50:17 | × | azeem quits (~azeem@176.200.230.183) (Ping timeout: 258 seconds) |
| 2021-08-13 21:50:41 | → | azeem joins (~azeem@176.200.230.183) |
| 2021-08-13 21:54:30 | × | xff0x quits (~xff0x@2001:1a81:5278:5300:e19e:51f3:462a:7dce) (Ping timeout: 258 seconds) |
| 2021-08-13 21:55:18 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-08-13 21:55:27 | → | xff0x joins (~xff0x@2001:1a81:5278:5300:2655:c9ee:974:3c59) |
| 2021-08-13 21:56:30 | <Las[m]> | falsifian: There are people who are using Idris compiled to JS |
| 2021-08-13 21:56:41 | <Las[m]> | But I think the focus is more on use with Node honestly |
| 2021-08-13 21:57:16 | × | vysn quits (~vysn@user/vysn) (Remote host closed the connection) |
| 2021-08-13 21:57:17 | <Las[m]> | https://github.com/idris-lang/Idris2/blob/main/docs/source/backends/javascript.rst |
| 2021-08-13 21:57:47 | <Las[m]> | I personally think Idris is fine for use in production compared to something like raw JavaScript |
| 2021-08-13 21:58:01 | → | haykam1 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-08-13 21:58:05 | <Las[m]> | There aren't that many serious bugs |
| 2021-08-13 21:59:45 | × | haykam quits (~haykam@static.100.2.21.65.clients.your-server.de) (Read error: Connection reset by peer) |
| 2021-08-13 22:02:22 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-08-13 22:04:17 | × | jtomas quits (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) (Ping timeout: 248 seconds) |
All times are in UTC.