Logs: freenode/#haskell
| 2021-03-03 00:52:28 | → | sablib joins (~sablib@171.113.165.91) |
| 2021-03-03 00:53:23 | × | m0rphism1 quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 245 seconds) |
| 2021-03-03 00:54:05 | <zebrag> | thinking hard... |
| 2021-03-03 00:54:26 | × | sw1nn quits (~sw1nn@2a00:23c6:2385:3a00:9310:964a:9231:59c9) (Ping timeout: 240 seconds) |
| 2021-03-03 00:54:52 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-negexpmuxmakobfg) (Quit: Connection closed for inactivity) |
| 2021-03-03 00:55:05 | <monochrom> | "pure f <*> pure x = pure (f x)" is straight from an Applicative law. |
| 2021-03-03 00:55:30 | <zebrag> | Maybe... I'll try harder to involve the Ap case |
| 2021-03-03 00:55:59 | <monochrom> | Your earlier liftAp question is the interesting one. |
| 2021-03-03 00:56:07 | COLE-H | is now known as cole-h |
| 2021-03-03 00:56:35 | <zebrag> | yes, when I use liftAp, I get answers I don't yet understand |
| 2021-03-03 00:56:36 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-03-03 00:58:45 | × | geyaeb quits (~geyaeb@gateway/tor-sasl/geyaeb) (Ping timeout: 268 seconds) |
| 2021-03-03 00:58:46 | × | fiQ2 quits (~fiQ@mirkk.ninja) (Quit: ZNC - https://znc.in) |
| 2021-03-03 00:58:47 | × | Philonous quits (~Philonous@unaffiliated/philonous) (Quit: ZNC - https://znc.in) |
| 2021-03-03 00:58:55 | → | geyaeb_ joins (~geyaeb@gateway/tor-sasl/geyaeb) |
| 2021-03-03 00:59:16 | → | Philonous joins (~Philonous@unaffiliated/philonous) |
| 2021-03-03 00:59:17 | → | fiQ2 joins (~fiQ@mirkk.ninja) |
| 2021-03-03 01:01:18 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 245 seconds) |
| 2021-03-03 01:01:46 | → | d34df00d joins (~d34df00d@104-14-27-213.lightspeed.austtx.sbcglobal.net) |
| 2021-03-03 01:02:08 | <monochrom> | The definition of Ap looks suspiciously like "a list of f things to do". |
| 2021-03-03 01:03:49 | <monochrom> | Ap (the data constructor) sounds like a list node, Pure sounds like marking end of list. |
| 2021-03-03 01:03:56 | × | sablib quits (~sablib@171.113.165.91) (Ping timeout: 240 seconds) |
| 2021-03-03 01:04:16 | <zebrag> | I was about to ask ;) |
| 2021-03-03 01:04:50 | <zebrag> | I see... |
| 2021-03-03 01:05:30 | <zebrag> | `:t case (liftAp (Just 4)) of {Pure x -> x; Ap apfa pafab -> undefined}` is returning undefined |
| 2021-03-03 01:05:48 | <zebrag> | I have to "evaluate" the undefined thing |
| 2021-03-03 01:05:54 | → | sablib joins (~sablib@171.113.165.91) |
| 2021-03-03 01:05:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-03-03 01:06:29 | <monochrom> | I took a look at the source code. liftAp a = Ap a (Pure id). |
| 2021-03-03 01:06:36 | <zebrag> | hum |
| 2021-03-03 01:06:38 | <zebrag> | nice |
| 2021-03-03 01:06:42 | <zebrag> | haven't seen that |
| 2021-03-03 01:07:57 | → | sw1nn joins (~sw1nn@2a00:23c7:622f:2c00:df3:76c2:ae90:b3b4) |
| 2021-03-03 01:11:01 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 2021-03-03 01:11:11 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 265 seconds) |
| 2021-03-03 01:11:17 | <monochrom> | I think Ap is a singly linked list of "f things to do". So I think its <*> is concatenating two such lists. liftAp is making a singleton, thus "Ap x (Pure id)". |
| 2021-03-03 01:12:11 | <monochrom> | To be sure, there is more. Each "f thing to do" also has an "answer" (of type 'a'). |
| 2021-03-03 01:12:22 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:2d2c:7153:bdbb:6201) (Remote host closed the connection) |
| 2021-03-03 01:12:58 | <monochrom> | Here is what you do (or what you expect the computer to do) for those answers. |
| 2021-03-03 01:13:23 | <zebrag> | that raises an error: :t case (liftAp (Just (4 :: Int))) of {Ap a b -> a; _ -> undefined} |
| 2021-03-03 01:13:24 | × | sm2n quits (~sm2n@bras-base-hmtnon143hw-grc-15-70-54-78-219.dsl.bell.ca) (Remote host closed the connection) |
| 2021-03-03 01:13:42 | → | sm2n joins (~sm2n@bras-base-hmtnon143hw-grc-15-70-54-78-219.dsl.bell.ca) |
| 2021-03-03 01:13:54 | <zebrag> | that doesn't: case (liftAp (Just (4 :: Int))) of {Ap a b -> 7; _ -> undefined} |
| 2021-03-03 01:14:15 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 256 seconds) |
| 2021-03-03 01:14:18 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-03-03 01:14:46 | <zebrag> | "because type variable ‘a1’ would escape its scope" |
| 2021-03-03 01:15:12 | <zebrag> | gadt... |
| 2021-03-03 01:15:39 | <monochrom> | The first "f thing" to do in the list --- so you're looking at the first node, say Ap (m :: f a) (ms :: Ap f (a->b)) --- well that m gives you an answer of type a. Then recursively the things in the rest of the list, ms, when the dust settles it gives you an answer of type a->b. The expectation is you apply the latter to the former to get a final answer. |
| 2021-03-03 01:16:21 | <zebrag> | ok |
| 2021-03-03 01:16:42 | <monochrom> | So I expect <*> to be like (++) in terms of the data structure, but also additional complication to honour the processing of answers. |
| 2021-03-03 01:16:52 | × | FortuneZero quits (3223b878@50.35.184.120) (Quit: Connection closed) |
| 2021-03-03 01:17:55 | <zebrag> | `:t case (liftAp (Just (4 :: Int))) of {Ap a (Pure b) -> b a; _ -> undefined}` "occur check error" |
| 2021-03-03 01:18:03 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:2d2c:7153:bdbb:6201) |
| 2021-03-03 01:19:38 | <zebrag> | beside that the sentence with "f thing" is very interesting |
| 2021-03-03 01:20:54 | <monochrom> | Have you seen or written fmap for Ap? |
| 2021-03-03 01:21:45 | <monochrom> | ho hum Ap has to be a GADT I guess |
| 2021-03-03 01:22:04 | <zebrag> | Just as you said, forgot to lift it |
| 2021-03-03 01:22:12 | <zebrag> | `case (liftAp (Just (4 :: Int))) of {Ap a (Pure b) -> b <$> a; _ -> undefined}` |
| 2021-03-03 01:22:15 | <monochrom> | no deriving functor sob sob |
| 2021-03-03 01:23:19 | <zebrag> | Now with all that I get a `Just 4` |
| 2021-03-03 01:25:06 | <zebrag> | I do not yet have the correct intuition about "functor" as a "f thing" to do. That intuition seems pivotal with free applicative |
| 2021-03-03 01:25:22 | <zebrag> | But I still don't get it well |
| 2021-03-03 01:26:43 | <zebrag> | In the paper https://arxiv.org/abs/1403.0749 they speak about it a lot, but I don't yet have the grasp of it |
| 2021-03-03 01:26:51 | <monochrom> | Hrm, I'm surprised that Functor (Ap f) does not need Functor f. I need to rethink this. |
| 2021-03-03 01:26:56 | nitrix_ | is now known as nitrix |
| 2021-03-03 01:27:14 | × | hendursa1 quits (~weechat@gateway/tor-sasl/hendursaga) (Quit: hendursa1) |
| 2021-03-03 01:27:33 | → | hendursaga joins (~weechat@gateway/tor-sasl/hendursaga) |
| 2021-03-03 01:28:45 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 2021-03-03 01:28:55 | <zebrag> | that's weird; even though we don't see the requirement they use `fmap` of `f` |
| 2021-03-03 01:30:50 | → | epicte7us joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 2021-03-03 01:31:11 | <zebrag> | hum, I'm mistaken |
| 2021-03-03 01:34:40 | × | ep1ctetus quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Ping timeout: 276 seconds) |
| 2021-03-03 01:35:29 | × | nineonin_ quits (~nineonine@50.216.62.2) (Ping timeout: 260 seconds) |
| 2021-03-03 01:35:35 | → | ddellacosta joins (~ddellacos@86.106.143.10) |
| 2021-03-03 01:39:56 | × | ddellacosta quits (~ddellacos@86.106.143.10) (Ping timeout: 240 seconds) |
| 2021-03-03 01:43:11 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:2d2c:7153:bdbb:6201) (Remote host closed the connection) |
| 2021-03-03 01:44:07 | <monochrom> | Functor f is not needed because the Ap case is an existential type. |
| 2021-03-03 01:44:52 | <monochrom> | So you're trying to code up fmap :: (x->y) -> Ap f x -> Ap f y, and you're coding the Ap case. |
| 2021-03-03 01:44:56 | × | sm2n quits (~sm2n@bras-base-hmtnon143hw-grc-15-70-54-78-219.dsl.bell.ca) (Ping timeout: 240 seconds) |
| 2021-03-03 01:45:25 | × | apache801 quits (~rishi@wsip-70-168-153-252.oc.oc.cox.net) (Ping timeout: 256 seconds) |
| 2021-03-03 01:45:39 | <monochrom> | fmap (f :: x->y) (Ap (m :: t) (ms :: Ap f (t->x)) = Ap ??? ??? |
| 2021-03-03 01:45:43 | → | jacks2 joins (~bc8134e3@217.29.117.252) |
| 2021-03-03 01:46:25 | <monochrom> | This is existential in t. "for some type t that you will not be told what". So first of all you will never be doing "fmap f m". |
| 2021-03-03 01:46:29 | <monochrom> | Err sorry, typo |
| 2021-03-03 01:46:38 | <monochrom> | fmap (f :: x->y) (Ap (m :: f t) (ms :: Ap f (t->x)) = Ap ??? ??? |
| 2021-03-03 01:47:09 | × | Sheilong quits (uid293653@gateway/web/irccloud.com/x-oegwsfxufkjwphyx) () |
| 2021-03-03 01:48:17 | <monochrom> | And if you don't use "fmap" on m, you won't be using f's fmap ever. |
| 2021-03-03 01:48:40 | <zebrag> | (reading, was afk) |
| 2021-03-03 01:49:11 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-03 01:49:17 | × | epicte7us quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 2021-03-03 01:49:30 | → | drbean_ joins (~drbean@TC210-63-209-35.static.apol.com.tw) |
| 2021-03-03 01:49:32 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-03 01:49:52 | <zebrag> | (Ap case existential, check) |
| 2021-03-03 01:50:00 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:2d2c:7153:bdbb:6201) |
| 2021-03-03 01:51:48 | × | leah2 quits (~leah@vuxu.org) (Ping timeout: 260 seconds) |
| 2021-03-03 01:52:25 | → | apache801 joins (~rishi@wsip-70-168-153-252.oc.oc.cox.net) |
| 2021-03-03 01:53:26 | → | leah2 joins (~leah@vuxu.org) |
| 2021-03-03 01:54:15 | <zebrag> | I manually lifted the `b` there: `case (liftAp (Just (4 :: Int))) of {Ap a (Pure b) -> b <$> a; _ -> undefined}` |
| 2021-03-03 01:54:33 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 264 seconds) |
| 2021-03-03 01:55:12 | <zebrag> | But isn't `a` escaping then? |
All times are in UTC.