Logs: liberachat/#haskell
| 2021-08-20 21:29:29 | <[exa]> | (also, "function are values") |
| 2021-08-20 21:30:38 | → | Megant joins (~kaitsu@user/megant) |
| 2021-08-20 21:30:42 | <[exa]> | technically, Monoid is also "value"-only now (the "function" is in Semigroup) |
| 2021-08-20 21:31:48 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 250 seconds) |
| 2021-08-20 21:31:48 | <ixlun> | They are very close to what I'm after. I'm trying to do something like https://pastebin.com/mQ4JEScb |
| 2021-08-20 21:32:01 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-20 21:32:35 | <ixlun> | so each type that implements ParsableSection has to define it's own ID. Then in the 'parse' function, I can deduce the id from the type that's passed in. |
| 2021-08-20 21:33:42 | <hpc> | sectionId needs to have k somewhere in its type |
| 2021-08-20 21:33:45 | <[exa]> | you'd need to run the sectionId with a type application though, because otherwise there's no way how it can see which instance it belongs to |
| 2021-08-20 21:33:55 | <[exa]> | consider Proxy |
| 2021-08-20 21:34:13 | <[exa]> | (or something related) |
| 2021-08-20 21:35:10 | × | Megant quits (~kaitsu@user/megant) (Ping timeout: 240 seconds) |
| 2021-08-20 21:35:28 | <[exa]> | and yeah, as hpc says -- I'd really vote for `sectionId :: k -> Word16` |
| 2021-08-20 21:35:46 | <[exa]> | it will allow you to parametrize the stuff by additional data |
| 2021-08-20 21:38:10 | <ixlun> | But then wouldn't I run into a chicken and egg scenario? In that the parse funciton yields a 'k' but I need to construct one to call sectionId? |
| 2021-08-20 21:38:48 | <ixlun> | and parse needs to call sectionId before it can do the parse |
| 2021-08-20 21:39:28 | → | oxide_ joins (~lambda@user/oxide) |
| 2021-08-20 21:39:52 | <hpc> | in that case go with Proxy |
| 2021-08-20 21:40:10 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2021-08-20 21:41:32 | <ixlun> | Cool, then I guess the type signature would be: sectionId :: Proxy k? |
| 2021-08-20 21:41:38 | × | o1lo01ol1o quits (~o1lo01ol1@5.181.115.89.rev.vodafone.pt) (Remote host closed the connection) |
| 2021-08-20 21:41:51 | → | o1lo01ol1o joins (~o1lo01ol1@5.181.115.89.rev.vodafone.pt) |
| 2021-08-20 21:42:08 | <ixlun> | sorry: sectionId :: Proxy k -> Word16 |
| 2021-08-20 21:42:19 | <hpc> | yep |
| 2021-08-20 21:42:31 | <c_wraith> | that works, though you might do better with sectionId :: proxy k -> Word16 |
| 2021-08-20 21:42:43 | <c_wraith> | making that p lowercase does some nice things |
| 2021-08-20 21:43:06 | <hpc> | sectionId Proxy @Foo |
| 2021-08-20 21:43:24 | <c_wraith> | In particular, it lets you pass values of other types that you might already have lying around in |
| 2021-08-20 21:43:49 | <c_wraith> | And parametricity guarantees you can't try to *use* the value |
| 2021-08-20 21:44:29 | <hpc> | not that you can do much with a Proxy value in the first place ;) |
| 2021-08-20 21:44:53 | <c_wraith> | can't do much, but you can at least pattern match on it |
| 2021-08-20 21:45:02 | <c_wraith> | Which can cause things to happen |
| 2021-08-20 21:45:14 | <[exa]> | o wow lowercase proxy |
| 2021-08-20 21:45:17 | <[exa]> | gooooooooood |
| 2021-08-20 21:45:26 | <[exa]> | (thanks!) |
| 2021-08-20 21:45:51 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2021-08-20 21:46:14 | <monochrom> | This is why I would write "p k -> Word16" instead. |
| 2021-08-20 21:47:50 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 250 seconds) |
| 2021-08-20 21:48:07 | × | norias quits (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2021-08-20 21:49:15 | <hpc> | just be careful, this is the gateway drug to f s t a b :D |
| 2021-08-20 21:52:38 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-20 21:53:09 | <ixlun> | Hmm okay. I gave it ago, and I'm getting an error. Here is the full code: https://termbin.com/r6qo |
| 2021-08-20 21:54:45 | <hpc> | might need scoped type variables? |
| 2021-08-20 21:54:52 | <monochrom> | Yeah, that. |
| 2021-08-20 21:55:06 | × | doyougnu quits (~user@c-73-25-202-122.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2021-08-20 21:56:35 | <ixlun> | Here is the error https://termbin.com/7klc |
| 2021-08-20 21:56:44 | <monochrom> | local "foo :: Bar a" means "foo :: forall a. Bar a" i.e. "foo :: Bar nothing_to_do_with_other_types" |
| 2021-08-20 21:57:46 | <ixlun> | Issue still persists with scoped type variables |
| 2021-08-20 21:58:17 | <monochrom> | You do have to write more than turning on the extension. |
| 2021-08-20 21:58:48 | <monochrom> | you have to now say "parseSection :: forall a m. (ParsableSection a, MonadError String m) => CodePlug -> ..." |
| 2021-08-20 21:59:18 | <ixlun> | Ahh, so when I say 'p = Proxy :: Proxy a'. the 'a' is a different type variable and doesn 't refer to the ParsableSection 'a'? |
| 2021-08-20 22:00:16 | → | oldsk00l_ joins (~znc@ec2-3-124-242-227.eu-central-1.compute.amazonaws.com) |
| 2021-08-20 22:00:23 | <ixlun> | Ahhhh, so that's what forall means? it means that if 'a' or 'm' is used in the below code, it refers to the 'a' or 'm' in the type signature of the function? |
| 2021-08-20 22:00:46 | × | oldsk00l quits (~znc@ec2-18-170-87-228.eu-west-2.compute.amazonaws.com) (Ping timeout: 252 seconds) |
| 2021-08-20 22:00:57 | <monochrom> | "forall" is a reserved word that also has meanings under other extensions. |
| 2021-08-20 22:01:29 | <monochrom> | So the inventor of this extension decides to hitchhike this reserved word. |
| 2021-08-20 22:01:46 | <monochrom> | and it works beatifully, there is no conflict. |
| 2021-08-20 22:02:01 | × | kenran quits (~kenran@200116b82b157f00af733520c5a4c898.dip.versatel-1u1.de) (Quit: WeeChat info:version) |
| 2021-08-20 22:02:03 | <ixlun> | So it's using forall in the context of scopedtypevariables? |
| 2021-08-20 22:02:07 | <monochrom> | The need to add some syntax is because backward compatibility. |
| 2021-08-20 22:02:13 | <hpc> | one could even say forall has only one meaning, and multiple applications of that meaning |
| 2021-08-20 22:02:22 | <hpc> | since it's really just bringing a new type variable into scope |
| 2021-08-20 22:04:14 | <ixlun> | Nice. Always wondered why I saw forall peppered on bits of haskell code. |
| 2021-08-20 22:04:39 | <hpc> | if you want to go down a fun mathematical rabbit hole, https://en.wikipedia.org/wiki/Universal_quantification |
| 2021-08-20 22:08:09 | <ixlun> | Thanks for the link. That's defiantly one to look at! Anyway code is working great now. Thanks for the help all! |
| 2021-08-20 22:12:40 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-08-20 22:16:40 | × | oxide_ quits (~lambda@user/oxide) (Quit: oxide_) |
| 2021-08-20 22:17:59 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-08-20 22:21:03 | × | jess quits (~jess@libera/staff/jess) () |
| 2021-08-20 22:22:52 | → | Megant joins (megant@user/megant) |
| 2021-08-20 22:27:36 | × | son0p quits (~ff@181.136.122.143) (Remote host closed the connection) |
| 2021-08-20 22:28:33 | → | tommd joins (~tommd@75-164-130-101.ptld.qwest.net) |
| 2021-08-20 22:29:22 | × | Megant quits (megant@user/megant) (Ping timeout: 252 seconds) |
| 2021-08-20 22:37:40 | → | Tuplanolla joins (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) |
| 2021-08-20 22:37:45 | <Cajun> | and for RankNTypes, doesnt it allow you to restrict a type variable from "escaping" like ST does? whats the other use(s) (if there are any) of it in RankNTypes? |
| 2021-08-20 22:38:19 | → | alphabeta joins (~kilolympu@cpc92710-cmbg20-2-0-cust265.5-4.cable.virginm.net) |
| 2021-08-20 22:38:32 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 250 seconds) |
| 2021-08-20 22:39:06 | × | kilolympus quits (~kilolympu@cpc92710-cmbg20-2-0-cust265.5-4.cable.virginm.net) (Ping timeout: 258 seconds) |
| 2021-08-20 22:39:56 | <monochrom> | To actually write rank-n types at all. |
| 2021-08-20 22:40:45 | <monochrom> | How else can "(∀r. r -> (r -> r) -> r) -> Natural" be expressed. |
| 2021-08-20 22:41:03 | × | MQ-17J quits (~MQ-17J@2607:fb90:8824:bf5d:8f75:f298:534b:ce5e) (Read error: Connection reset by peer) |
| 2021-08-20 22:41:25 | → | MQ-17J joins (~MQ-17J@8.6.144.209) |
| 2021-08-20 22:41:48 | <Cajun> | well what does that express about `r` that isnt already? |
| 2021-08-20 22:41:54 | <monochrom> | interpreter :: (∀a. MyFunctor a -> IO a) -> Free MyFunctor a -> IO a |
| 2021-08-20 22:42:33 | <monochrom> | (∀r. r -> (r -> r) -> r) -> Natural ≠ ∀r. (r -> (r -> r) -> r) -> Natural |
| 2021-08-20 22:43:34 | <Cajun> | in that interpreter line, the qualified `a` /~ the outside `a`, correct? |
| 2021-08-20 22:43:43 | <monochrom> | right |
| 2021-08-20 22:46:20 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9557dc14868c6ad3e278.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 2021-08-20 22:47:41 | → | norias joins (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-08-20 22:47:51 | × | norias quits (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Client Quit) |
| 2021-08-20 22:51:11 | <Cajun> | so whats the purpose of `ExplicitForAll`? does it behave like `ScopedTypeVariables`? i dont see why it would be useful to have `forall`s where it is implicit, or when it would be useful to abuse the `forall-or-nothing` rule |
| 2021-08-20 22:52:07 | <geekosaur> | just to be complete, I think, so both RankNTypes and ScopedTypeVariables can "depend on" it |
| 2021-08-20 22:52:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-08-20 22:52:36 | <Cajun> | oh well that makes sense |
| 2021-08-20 22:52:39 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-20 22:53:20 | <monochrom> | I was not the author of ExplicitForAll, I don't know their purpose. |
| 2021-08-20 22:53:54 | <monochrom> | But my philosophy is that implicit quantification has always been a source of confusion, not a source of simplification. |
| 2021-08-20 22:54:32 | <monochrom> | Implicit forall is why people mistake induction for circular logic. |
| 2021-08-20 22:55:51 | <Cajun> | i believe anything that almost entirely leaves the realm of computer science-y stuff (like quantification imo) is when it trips up people the most, but thats coming from little experience |
| 2021-08-20 22:56:23 | <geekosaur> | and ExplicitForalls doesn't mean you always have to write them, it just makes forall a keyword, so it's kinda confusingly named |
All times are in UTC.