Logs on 2023-04-12 (liberachat/#haskell)
| 00:00:03 | → | mauke_ joins (~mauke@user/mauke) |
| 00:01:31 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 240 seconds) |
| 00:01:31 | mauke_ | is now known as mauke |
| 00:01:35 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 00:02:01 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 00:02:52 | Lord_of_Life_ | is now known as Lord_of_Life |
| 00:06:17 | × | ix quits (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) (Quit: WeeChat 3.8) |
| 00:10:14 | × | heraldo quits (~heraldo@user/heraldo) (Ping timeout: 246 seconds) |
| 00:16:06 | <jackdk> | Hi Dr. Maxwarror! |
| 00:17:34 | × | Vq quits (~vq@90-227-192-206-no77.tbcn.telia.com) (Ping timeout: 265 seconds) |
| 00:18:18 | <geekosaur> | they left |
| 00:19:26 | → | Vq joins (~vq@90-227-192-206-no77.tbcn.telia.com) |
| 00:24:00 | × | mjs2600 quits (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 00:25:18 | → | chanceyan joins (~chanceyan@user/chanceyan) |
| 00:25:40 | → | mjs2600 joins (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
| 00:26:37 | → | glguy joins (~glguy@libera/staff-emeritus/glguy) |
| 00:30:57 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 00:34:21 | × | fbytez quits (~uid@user/fbytez) (Quit: byte byte) |
| 00:34:39 | → | fbytez joins (~uid@2001:bc8:2117:100::) |
| 00:37:33 | <Axman6> | Goodbye, Dr. Maxwarrior, you dshall be missed |
| 00:37:51 | <Axman6> | s/ds/s/g |
| 00:38:11 | <Axman6> | (ds has no place existing anywhere) |
| 00:40:33 | <Axman6> | % :t only |
| 00:40:33 | <yahb2> | <interactive>:1:1: error: Variable not in scope: only |
| 00:40:47 | <Axman6> | % import Control.Lens |
| 00:40:48 | <yahb2> | <no location info>: error: ; Could not find module ‘Control.Lens’ ; It is not a module in the current program, or in any known package. |
| 00:40:53 | <Axman6> | :( |
| 00:41:14 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 00:41:19 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 00:43:02 | <Axman6> | (only :: Eq a => a -> Prism' a () -- for anyone playing along at home) |
| 00:45:45 | <jackdk> | :t only |
| 00:45:46 | <lambdabot> | (Eq a, Choice p, Applicative f) => a -> p () (f ()) -> p a (f a) |
| 00:47:09 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 00:47:10 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 00:47:10 | → | wroathe joins (~wroathe@user/wroathe) |
| 00:52:04 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 252 seconds) |
| 00:52:36 | → | aweinstock joins (~aweinstoc@cpe-74-76-189-75.nycap.res.rr.com) |
| 00:53:59 | → | cheater_ joins (~Username@user/cheater) |
| 00:57:27 | × | cheater quits (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 00:57:36 | cheater_ | is now known as cheater |
| 01:01:47 | <erisco> | are there equivalently general solutions for finding the fixpoint other than fix :: (a -> a) -> a ? for example, why not loop :: (a -> Either a b) -> a -> b ? |
| 01:02:31 | × | cheater quits (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 01:02:47 | → | zer0bitz_ joins (~zer0bitz@2001:2003:f443:d600:c8fb:80d:3f21:d12f) |
| 01:03:15 | <Axman6> | :t let loop f x = fix (\case Left a -> f a; Right b -> b) . Left in loop |
| 01:03:16 | <lambdabot> | error: |
| 01:03:16 | <lambdabot> | • Couldn't match expected type ‘Either a1 b0 -> c1’ |
| 01:03:16 | <lambdabot> | with actual type ‘Either t1 b1’ |
| 01:03:27 | <Axman6> | :t let loop f = fix (\case Left a -> f a; Right b -> b) . Left in loop |
| 01:03:28 | <lambdabot> | error: |
| 01:03:28 | <lambdabot> | • Couldn't match expected type ‘Either a1 b0 -> c1’ |
| 01:03:28 | <lambdabot> | with actual type ‘Either t1 b1’ |
| 01:03:35 | → | jinsun joins (~jinsun@user/jinsun) |
| 01:03:43 | <Axman6> | I'm bad at Haskell |
| 01:04:10 | × | zer0bitz quits (~zer0bitz@2001:2003:f443:d600:8072:a2d3:32b3:1df4) (Ping timeout: 252 seconds) |
| 01:05:01 | <erisco> | you could go down a line of reasoning such as fix can become loop but loop cannot become fix, but then the question is, what is an example where fix suffices and loop does not? |
| 01:05:28 | <jackdk> | Axman6: `loop = fix $ \recur f -> either (recur f) id . f`? |
| 01:07:10 | <jackdk> | Hm, can you write `fix` in terms of `loop`? |
| 01:07:22 | <Axman6> | yeah that was my next question |
| 01:07:47 | <Axman6> | can you get the same behaviour as fix (1:)? |
| 01:08:47 | <erisco> | fix is about a fix point, and loop isn't, at least not obviously, but they both can be seen as implementations of recursion |
| 01:09:15 | <erisco> | I am not sure that you necessarily need fix for recursion, ie I am unaware of an example that cannot be implemented with loop |
| 01:09:44 | <Axman6> | it seems to be that loop forces a particular ordering to evaluation too, you can't progress without evaluating the Either, which feels different to the substitution of the function into itself |
| 01:10:14 | → | cheater joins (~Username@user/cheater) |
| 01:10:27 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:12:07 | → | cheater_ joins (~Username@user/cheater) |
| 01:13:55 | <Axman6> | Currently going through Optics by Example, TIL about beside; definitely need to file that one away |
| 01:14:31 | × | cheater quits (~Username@user/cheater) (Ping timeout: 240 seconds) |
| 01:15:32 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 01:15:39 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 01:16:27 | → | cheater__ joins (~Username@user/cheater) |
| 01:16:27 | cheater__ | is now known as cheater |
| 01:16:34 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:16:51 | <erisco> | we say that imperative loops and functional recursion are two ways to go about the same thing (operationally) ... I am gleaning this impression that the difference really is only found in the semantics |
| 01:17:03 | <monochrom> | erisco: Are you ruling out ones = 1 : ones? Or do you know how to get ones from loop? |
| 01:18:11 | × | cheater_ quits (~Username@user/cheater) (Ping timeout: 250 seconds) |
| 01:18:35 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 248 seconds) |
| 01:18:39 | <c_wraith> | yeah, I don't see how loop can handle corecursion at all |
| 01:19:16 | <erisco> | sort of but not in the way you'd want |
| 01:20:36 | <erisco> | loop (\f -> Left (f . f)) (1:) |
| 01:21:28 | <monochrom> | does "take 1 (loop (\f -> Left (f . f)) (1:))" terminate and give [1]? |
| 01:22:03 | <erisco> | no |
| 01:22:11 | <monochrom> | I ask because I am too lazy to either ask what "loop" does (no, the type does not give enough information) or check the implementation given so far. |
| 01:22:40 | <monochrom> | But you know what loop does and you can quickly work out my take-1 example in your head. |
| 01:23:09 | <erisco> | https://hackage.haskell.org/package/extra-1.7.13/docs/src/Control.Monad.Extra.html#loop |
| 01:24:06 | → | cheater_ joins (~Username@user/cheater) |
| 01:24:28 | <monochrom> | If you prefer imperative programming, main = do { s <- getLine; putStrLn ("hello " ++ s); main } is a prototype of a whole class of useful programs. |
| 01:24:47 | <monochrom> | e.g., web apps are that on steroid. |
| 01:24:48 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 01:25:17 | <monochrom> | Can you write web apps with loop? |
| 01:25:50 | → | cheater__ joins (~Username@user/cheater) |
| 01:25:50 | cheater__ | is now known as cheater |
| 01:26:08 | <erisco> | somehow I didn't expect you to ever ask such a question :P |
| 01:26:27 | <jackdk> | :t interact |
| 01:26:28 | <lambdabot> | (String -> String) -> IO () |
| 01:26:38 | <c_wraith> | and if you don't see the punchline coming - fix can do that. |
| 01:27:14 | <c_wraith> | I actually find fix most useful for ad-hoc loops in IO where I need to close over a previously-generated value. |
| 01:27:57 | <monochrom> | Yeah, "do = { .... ; let {myloop = ... myloop ...}; myloop ...}" gets old sometimes. |
| 01:28:41 | <monochrom> | "do = { ... ; fix (\myloop -> ... myloop ...) ...}" is sometimes nicer to the eyes. |
| 01:28:55 | × | cheater_ quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 01:29:13 | <monochrom> | Although, sometimes I find that unsatisfactory too. Haven't found a really beautiful solution. |
| 01:30:06 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::5) (Ping timeout: 265 seconds) |
| 01:30:22 | <monochrom> | Actually, I have found a really beautiful solution, but it's heresy: Reinstate flow charts. |
| 01:30:52 | <erisco> | so it seems what we're identifying is there is a difference in what you can see on the outside, in that we cannot see what loop is doing until it stops at a Right, whereas, at least with guarded recursion, we can see what fix is doing |
| 01:31:13 | <monochrom> | No. |
| 01:31:26 | <erisco> | k what is it then |
| 01:32:28 | <monochrom> | "take 1 ones" hardly qualifies as "see inside what it's doing". It's an emphatically blackbox observation. |
| 01:33:20 | <monochrom> | And running my main example too, I am merely saying I am at the terminal entering some input and hoping for some output, some interaction. |
| 01:33:47 | <erisco> | both the loop version and the fix version of building a list of ones operationally builds a list of ones, but we cannot access that list in the case of loop |
| 01:33:53 | <monochrom> | Interacting with the computer is clearly blackbox outside by definition. No one is running a debugger or strace. |
| 01:34:32 | <erisco> | we can say the same of this IO action |
| 01:34:36 | <monochrom> | Or at least I am not running a debugger or strace. |
| 01:34:54 | <c_wraith> | fix f reduces to a call to f with some argument. loop f reduces to a call to loop (when f is returning a Left, anyway) |
| 01:35:51 | <c_wraith> | that's roughly the same as the difference between foldr and foldl |
| 01:36:28 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 01:36:38 | <monochrom> | "main = mapM_ print ones" is also a blackbox outside observation. |
| 01:36:50 | <erisco> | so now I am wondering what we might think if loop was generalised to: |
| 01:36:51 | <erisco> | loop :: Monad m => (a -> m (Either a b)) -> a -> m b |
| 01:36:51 | <erisco> | loop f x = f x >>= \r -> case r of Left y -> loop f y; Right z -> pure z |
| 01:37:02 | <monochrom> | I see spamming or I see darkness. |
| 01:38:07 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 250 seconds) |
| 01:39:43 | <c_wraith> | erisco: isn't that loopM, the next definition in that file? |
| 01:39:46 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 01:39:59 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 01:40:00 | <erisco> | yep |
| 01:40:14 | <monochrom> | My hunch is that using free theorems, the type "forall m. Monad m => ..." says that we can gain a lot of information by setting m = Identity. |
| 01:40:35 | <monochrom> | In fact, s/information/information on limitations/ |
| 01:41:08 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::3) |
| 01:41:59 | → | jinsun joins (~jinsun@user/jinsun) |
| 01:42:13 | <c_wraith> | erisco: did you see where I was going with the foldr/foldl comparison? |
| 01:42:16 | <monochrom> | Now, if you upgrade to MonadPlus and try to use <|> somewhere, that will be a lot of interesting. |
| 01:42:27 | <erisco> | c_wraith, yes |
| 01:42:35 | <monochrom> | (In that case setting m = [] tells us a lot.) |
| 01:42:59 | <monochrom> | s/a lot of/a lot more/ |
| 01:43:15 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 01:43:30 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 01:44:28 | × | ix quits (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) (Client Quit) |
| 01:44:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Ping timeout: 260 seconds) |
| 01:44:44 | <erisco> | monochrom, well, when m = IO then your greeter program is implementable in the intended way |
| 01:47:20 | <monochrom> | Oh then I guess m = Cont [Integer] will get ones=1:ones done. |
| 01:47:58 | <erisco> | thanks I was trying to figure that one out :) and maybe fix is in there somewhere too |
| 01:53:20 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 260 seconds) |
| 01:53:26 | <erisco> | there is the idea of termination vs productivity, and it seems vaguely that loop is useful when you have termination and loopM or fix is useful when you have termination or just productivity |
| 01:54:37 | <erisco> | well these are good thoughts, thanks for the conversation |
| 01:55:32 | → | cheater joins (~Username@user/cheater) |
| 01:56:46 | → | jinsun joins (~jinsun@user/jinsun) |
| 01:58:18 | <monochrom> | Termination was an ancient 1960s idea when access to computers was barred and you submitted a program before 9PM and some one else on night shift ran it at 4AM for 5 minutes and you woke up at 8AM and collected the result (well, one could hope). |
| 01:58:25 | → | razetime1 joins (~Thunderbi@117.193.5.39) |
| 01:58:50 | <monochrom> | Today productivity aka interactive responsiveness is the actual requirement. |
| 01:59:10 | × | razetime quits (~Thunderbi@117.193.5.39) (Ping timeout: 276 seconds) |
| 01:59:10 | razetime1 | is now known as razetime |
| 02:01:07 | × | xff0x quits (~xff0x@ai098135.d.east.v6connect.net) (Ping timeout: 276 seconds) |
| 02:02:32 | <erisco> | yeah I wouldn't argue with that but there seem to be semantic differences that are interesting and might motivate the choice of one over the other |
| 02:03:11 | <monochrom> | And here is how to use loop and Cont for ones=1:ones https://paste.tomsmeding.com/qzzaNKfH |
| 02:03:51 | <erisco> | nice |
| 02:04:03 | <c_wraith> | you can do it with Writer instead |
| 02:04:09 | hugo- | is now known as hugo |
| 02:04:27 | <monochrom> | Oh the difference goes even beyond semantics. It completely changes how you prove correctness. |
| 02:05:09 | <monochrom> | Most formal methods invented for 1960s batch-mode computing are rendered useless for interactive programs. |
| 02:07:59 | <erisco> | What I was looking at with fix vs loop is that with fix you have these bottomless expressions, whereas with with loop you do not. Because I am interested in always being able to reduce an expression to some normal value, fix was posing a problem... I know there is some information lattice game you can play with the semantics to sort this out as well |
| 02:08:25 | → | ix joins (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) |
| 02:08:25 | <[Leary]> | erisco: You might be interested in `rec :: Functor f => (f (LFP f * a) -> a) -> LFP f -> a` and its dual `corec :: Functor f => (a -> f (GFP f + a)) -> a -> GFP f`. They can be written in the strongly-normalising System F, so despite encoding recursion, they're guaranteed to "terminate" and "produce" respectively. |
| 02:09:40 | <erisco> | so a simple example is fix (1+) versus loop (\x -> Left (1 + x)) 0 ... neither terminate, but the loop is operationally counting up the integers, whereas fix is building an infinite expression |
| 02:10:08 | <monochrom> | erisco: OK, fix in terms of loop+Cont: https://paste.tomsmeding.com/sL5V7uql |
| 02:10:25 | <monochrom> | "That covers everything now" :) |
| 02:10:28 | <erisco> | [Leary], thanks |
| 02:11:52 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 02:11:57 | → | _xor joins (~xor@74.215.46.17) |
| 02:12:12 | <erisco> | monochrom, very nice |
| 02:13:00 | <erisco> | there are echoes of code reviews playing in my head about your variable naming but very nice :P |
| 02:13:24 | <monochrom> | Oh, it really was just "since ones = fix (1:), wherever I see 1:foo I just generalize it to f foo". |
| 02:14:03 | × | _xor quits (~xor@74.215.46.17) (Client Quit) |
| 02:14:36 | <monochrom> | Right? (Or Left? Haha) I had "1 : k (Left ())" so it's just "f (k (Left ()))" in general. |
| 02:15:30 | × | td_ quits (~td@i5387091F.versanet.de) (Ping timeout: 255 seconds) |
| 02:16:34 | → | nate1 joins (~nate@98.45.169.16) |
| 02:17:05 | → | td_ joins (~td@i53870927.versanet.de) |
| 02:18:08 | × | rburkholder quits (~blurb@96.45.2.121) (Ping timeout: 248 seconds) |
| 02:18:13 | <monochrom> | Unfortunately every iteration it keeps a new copy of "Right z -> pure z" just in case, so memory usage grows. |
| 02:18:42 | <monochrom> | Err no, that can't be right. |
| 02:19:33 | × | Katarushisu quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Ping timeout: 255 seconds) |
| 02:20:17 | → | Katarushisu joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 02:22:45 | <monochrom> | Nah there is no memory growth, it's OK. |
| 02:22:58 | × | Me-me quits (~me-me@2602:ff16:3:0:1:dc:beef:d00d) (Remote host closed the connection) |
| 02:24:14 | → | Me-me joins (~me-me@user/me-me) |
| 02:24:59 | × | mei quits (~mei@user/mei) (Killed (tantalum.libera.chat (Nickname regained by services))) |
| 02:25:04 | → | mei joins (~mei@user/mei) |
| 02:34:23 | → | rburkholder joins (~blurb@96.45.2.121) |
| 02:44:40 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::3) (Ping timeout: 260 seconds) |
| 02:45:35 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:46:37 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 276 seconds) |
| 02:49:17 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 02:51:19 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 02:53:46 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 02:54:52 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::3) |
| 02:55:26 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::3) (Remote host closed the connection) |
| 02:58:38 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:58:38 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:58:38 | finn_elija | is now known as FinnElija |
| 03:01:25 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 265 seconds) |
| 03:04:38 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 03:05:53 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 255 seconds) |
| 03:09:48 | × | ix quits (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) (Quit: WeeChat 3.8) |
| 03:13:15 | → | ix joins (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) |
| 03:13:35 | × | ix quits (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) (Client Quit) |
| 03:14:27 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 255 seconds) |
| 03:19:18 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 265 seconds) |
| 03:22:19 | × | Square quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 03:30:52 | → | ix joins (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) |
| 03:31:55 | × | ix quits (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) (Client Quit) |
| 03:35:03 | → | ix joins (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) |
| 03:35:05 | × | razetime quits (~Thunderbi@117.193.5.39) (Ping timeout: 268 seconds) |
| 03:35:11 | × | ix quits (~ix@2a02:8012:281f:0:5a9c:fcff:fe09:a026) (Client Quit) |
| 03:41:03 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 03:41:22 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 03:42:45 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 03:46:57 | → | fernand joins (~fernand@179.156.34.250) |
| 03:47:18 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 03:58:52 | → | institor joins (~absentia@user/institor) |
| 04:13:28 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 265 seconds) |
| 04:14:33 | → | dibblego joins (~dibblego@122-199-1-30.ip4.superloop.au) |
| 04:14:34 | × | dibblego quits (~dibblego@122-199-1-30.ip4.superloop.au) (Changing host) |
| 04:14:34 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 04:19:11 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 04:22:24 | × | fernand quits (~fernand@179.156.34.250) (Ping timeout: 248 seconds) |
| 04:26:28 | <Clinton[m]> | If anyone knows a bit about using generics in Haskell, I'd appreciate it if they have a look at this question: https://stackoverflow.com/questions/75991896/generically-iterating-over-accessors-of-a-product-type |
| 04:26:39 | → | dsrt^ joins (~dsrt@c-76-105-96-13.hsd1.ga.comcast.net) |
| 04:32:49 | → | mbuf joins (~Shakthi@49.207.178.186) |
| 04:36:28 | → | trev joins (~trev@user/trev) |
| 04:37:38 | → | dipper joins (~dipper@203.168.11.65) |
| 04:38:00 | <probie> | Clinton[m]: are you sure the types are right in that question? Or do you mean something like `productAccessorsToList :: ... => (forall b. c b => (a -> b) -> t) -> [a -> t]`? |
| 04:43:28 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 04:44:51 | → | freeside joins (~mengwong@50.216.111.242) |
| 04:44:53 | <Clinton[m]> | <probie> "Clinton: are you sure the..." <- No, it should be `-> [t]`, not `-> [a -> t]`. Given a type `a` with field `b`, an accessor for that field is of type `a -> b`. I've got a function that takes an accessor forall b. (i.e. forall b. a -> b) and produces some type `t`. I want those in a list. |
| 04:46:42 | <Clinton[m]> | It's almost like `productToList`, but instead of iterating over the values (which of course, needs an actual value of type `a`, and then iterate over the fields `b`) i iterate over the accessors which are `a -> b`, and hence there's now no need to pass an actual value. |
| 04:47:14 | × | chanceyan quits (~chanceyan@user/chanceyan) (Quit: Client closed) |
| 04:47:39 | → | chanceyan joins (~chanceyan@user/chanceyan) |
| 04:48:46 | <probie> | Clinton[m]: Right. I get what you mean now. I must still be half-asleep |
| 04:50:58 | <institor> | wew |
| 04:51:14 | <institor> | some hardcore types in `Generics.SOP` |
| 04:52:12 | <Axman6> | They're not really too scary |
| 04:54:09 | <institor> | :t id |
| 04:54:11 | <lambdabot> | a -> a |
| 04:54:34 | <institor> | :t (hcollapse . hcmap (Proxy :: Proxy c) (mapIK f)) |
| 04:54:35 | <lambdabot> | error: |
| 04:54:35 | <lambdabot> | Variable not in scope: hcollapse :: b0 -> c |
| 04:54:35 | <lambdabot> | error: |
| 04:54:46 | <institor> | :import Generics.SOP |
| 04:54:50 | <institor> | ehh... |
| 04:55:47 | → | JScript joins (~JScript@45.248.77.94) |
| 04:55:51 | × | JScript quits (~JScript@45.248.77.94) (Max SendQ exceeded) |
| 04:56:08 | <Axman6> | lambdabot can't import new modules IIRC, yahb2 can but needs to have it installed |
| 04:56:19 | → | JScript joins (~JScript@45.248.77.94) |
| 04:56:39 | × | JScript quits (~JScript@45.248.77.94) (Max SendQ exceeded) |
| 04:57:15 | → | JScript joins (~JScript@45.248.77.94) |
| 04:58:10 | <institor> | :!@t id |
| 04:59:17 | <c_wraith> | Axman6: lambdabot can, but it has the same restriction. and also the restriction that safe haskell allows the module |
| 05:04:23 | <c_wraith> | > compilerVersion |
| 05:04:24 | <lambdabot> | error: Variable not in scope: compilerVersion |
| 05:04:30 | <c_wraith> | @let import System.Info |
| 05:04:31 | <lambdabot> | Defined. |
| 05:04:33 | <c_wraith> | > compilerVersion |
| 05:04:34 | <lambdabot> | Version {versionBranch = [8,10], versionTags = []} |
| 05:05:11 | <institor> | > let import |
| 05:05:13 | <lambdabot> | <hint>:1:5: error: parse error on input ‘import’ |
| 05:05:19 | <institor> | @let import Generics.SOP |
| 05:05:20 | <lambdabot> | /sandbox/tmp/.L.hs:132:1: error: |
| 05:05:20 | <lambdabot> | Could not find module ‘Generics.SOP’ |
| 05:05:20 | <lambdabot> | Use -v (or `:set -v` in ghci) to see a list of the files searched for. |
| 05:05:24 | <institor> | rip |
| 05:05:29 | <institor> | generics-sop> Registering library for generics-sop-0.5.1.2.. |
| 05:05:31 | <institor> | Completed 2 action(s). |
| 05:14:45 | → | michalz joins (~michalz@185.246.204.107) |
| 05:17:06 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 05:17:52 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 05:20:25 | × | ddellacosta quits (~ddellacos@146.70.171.100) (Ping timeout: 250 seconds) |
| 05:21:13 | × | mniip_ quits (mniip@libera/staff/mniip) (Quit: This page is intentionally left blank) |
| 05:21:18 | → | mniip joins (mniip@libera/staff/mniip) |
| 05:26:51 | × | remexre quits (~remexre@user/remexre) (Read error: Connection reset by peer) |
| 05:28:05 | × | JScript quits (~JScript@45.248.77.94) (Remote host closed the connection) |
| 05:29:13 | <institor> | i mean |
| 05:29:17 | <institor> | i'm not sure it typechecks |
| 05:29:28 | → | remexre joins (~remexre@user/remexre) |
| 05:30:22 | <institor> | > type family AllN (h :: (k -> Type) -> l -> Type) (c :: k -> Constraint) :: l -> Constraint |
| 05:30:24 | <lambdabot> | <hint>:1:1: error: parse error on input ‘type’ |
| 05:30:32 | <institor> | `(c :: k -> Constraint)` |
| 05:33:59 | <institor> | @hoogle hcmap |
| 05:33:59 | <lambdabot> | Generics.SOP hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k) . c a => f a -> f' a) -> h f xs -> h f' xs |
| 05:33:59 | <lambdabot> | Data.SOP hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a . c a => f a -> f' a) -> h f xs -> h f' xs |
| 05:33:59 | <lambdabot> | Data.SOP.Classes hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a . c a => f a -> f' a) -> h f xs -> h f' xs |
| 05:34:22 | <institor> | ghci> :t hcmap |
| 05:34:24 | <institor> | hcmap |
| 05:34:26 | <institor> | :: forall {k} {l} {h :: (k -> *) -> l -> *} {c :: k -> Constraint} |
| 05:34:28 | <institor> | {xs :: l} {proxy :: (k -> Constraint) -> *} {f :: k -> *} |
| 05:34:30 | <institor> | {f' :: k -> *}. |
| 05:43:30 | <institor> | error: |
| 05:43:32 | <institor> | • Couldn't match kind ‘*’ with ‘* -> Constraint’ |
| 05:43:33 | <institor> | When matching types |
| 05:43:35 | <institor> | proxy0 :: (* -> Constraint) -> * |
| 05:43:37 | <institor> | Proxy :: * -> * |
| 05:43:40 | <institor> | Expected: proxy0 c1 |
| 05:43:41 | <institor> | Actual: Proxy c0 |
| 05:43:44 | <institor> | • In the first argument of ‘hcmap’, namely ‘(Proxy :: (Proxy c))’ |
| 05:45:42 | <probie> | Clinton[m]: does something like https://paste.tomsmeding.com/XgcL37pd meet your requirements? |
| 05:46:40 | → | offtherock joins (~blurb@96.45.2.121) |
| 05:48:39 | <probie> | I may have just moved `accessors` into a where without cleaning up the signature xD |
| 05:49:16 | × | rburkholder quits (~blurb@96.45.2.121) (Ping timeout: 255 seconds) |
| 05:49:53 | → | kenran joins (~user@user/kenran) |
| 05:50:28 | <probie> | https://paste.tomsmeding.com/J0P2flH7 is a bit neater |
| 05:56:50 | → | gurkenglas joins (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) |
| 05:57:11 | <Axman6> | institor: please don't do that |
| 05:57:15 | <Axman6> | @where paste |
| 05:57:15 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 06:02:45 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 255 seconds) |
| 06:04:29 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 06:10:02 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 246 seconds) |
| 06:13:44 | <Clinton[m]> | <probie> "Clinton: does something like..." <- Very very nice! I've shortened your code to this btw:... (full message at <https://libera.ems.host/_matrix/media/v3/download/libera.chat/454a2e2151b69ebd0e721beb99b7a571241dbf2f>) |
| 06:14:08 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 06:14:33 | → | mastarija joins (~mastarija@2a05:4f46:e03:6000:a9d6:2c1d:3bed:e943) |
| 06:16:00 | <Clinton[m]> | Thanks probie ! |
| 06:21:56 | <Clinton[m]> | probie: can you explain what `genAccs` is doing? |
| 06:24:14 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:e94a:711d:cca5:b3e) |
| 06:25:08 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 06:28:30 | <Clinton[m]> | probie: if you've got time that is, I can probably just dig through the types and work it out myself |
| 06:28:36 | <Clinton[m]> | probie: but thank you again! |
| 06:30:59 | <probie> | Clinton[m]: It generates the accessor functions. If it were just over lists, it'd be something like `f :: [b] -> [[a] -> a]`, `f [] = []; f (_:xs) = head: (map (. tail) (f xs))` |
| 06:31:31 | <probie> | It takes a list describing the shape, and from that produces a list of functions, where the nth element of that list is a function which takes a list and returns the nth element |
| 06:31:44 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 06:34:28 | → | acidjnk joins (~acidjnk@p200300d6e715c435781b7adab6bb3c42.dip0.t-ipconnect.de) |
| 06:38:04 | <probie> | Given a type like `NP I '[Int, Char, Bool]` the base case gives us a `NP ((->) NP I '[]) '[]`, next we produce a `NP ((->) NP I '[Bool]) '[Bool]` next, a `NP ((->) NP I '[Char, Bool]) '[Char, Bool]` and then a `NP ((->) NP I '[Int, Char, Bool]) '[Int, Char, Bool]` |
| 06:39:49 | <probie> | and then `accessor` just takes that final result and turns it into a `NP ((->) a) '[Int, Char, Bool]` (assuming SOP.ProductCode a ~ '[Int, Char, Bool]) |
| 06:40:22 | <probie> | s/accessor/accessors/ |
| 06:43:15 | × | freeside quits (~mengwong@50.216.111.242) (Ping timeout: 255 seconds) |
| 06:43:18 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 06:43:18 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 06:43:18 | → | wroathe joins (~wroathe@user/wroathe) |
| 06:44:08 | → | freeside joins (~mengwong@50.216.111.242) |
| 06:47:13 | × | razetime quits (~Thunderbi@117.193.5.39) (Quit: See You Space Cowboy) |
| 06:47:51 | <probie> | tl;dr, genAccs produces a list like `[head, head . tail, head . tail . tail, head . tail . tail . tail...` of the needed length |
| 06:48:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 06:48:47 | × | freeside quits (~mengwong@50.216.111.242) (Ping timeout: 264 seconds) |
| 06:50:22 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 276 seconds) |
| 06:57:58 | × | son0p quits (~ff@181.136.122.143) (Ping timeout: 268 seconds) |
| 07:02:13 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 07:03:40 | <jackdk> | probie: `[car, cadr, caadr, caaadr, ...`? |
| 07:19:24 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 07:20:16 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 276 seconds) |
| 07:24:50 | → | freeside joins (~mengwong@50.216.111.242) |
| 07:28:22 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:30:50 | × | MasseR46 quits (thelounge@2001:bc8:47a0:1521::1) (Quit: The Lounge - https://thelounge.chat) |
| 07:31:58 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 07:37:28 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 07:37:58 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 07:38:17 | <fendor[m]> | can I say in lens, this tuple has at least the size three? I want to write some code that works with a three element tuple as well as five element tuple, but the last two values are irrelevant to me. |
| 07:38:39 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 07:39:13 | <kuribas> | fendor[m]: just turn the 5-tuple in a 3-tuple before the function then? |
| 07:39:23 | <kuribas> | Or write a single "adapter" function. |
| 07:40:03 | × | vglfr quits (~vglfr@88.155.17.187) (Read error: Connection reset by peer) |
| 07:42:07 | <fendor[m]> | right, that's what I was going to do, but I was wondering whether lens may be giving me something already |
| 07:43:13 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (*.net *.split) |
| 07:43:13 | × | freeside quits (~mengwong@50.216.111.242) (*.net *.split) |
| 07:43:13 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (*.net *.split) |
| 07:43:13 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (*.net *.split) |
| 07:43:13 | × | pieguy128_ quits (~pieguy128@bras-base-mtrlpq5031w-grc-50-65-93-192-141.dsl.bell.ca) (*.net *.split) |
| 07:43:13 | × | jwiegley_ quits (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) (*.net *.split) |
| 07:43:13 | × | Sauvin quits (~sauvin@user/Sauvin) (*.net *.split) |
| 07:43:13 | × | gry quits (st@botters/gry) (*.net *.split) |
| 07:43:13 | × | institor quits (~absentia@user/institor) (*.net *.split) |
| 07:43:13 | × | xstill_5 quits (xstill@fimu/xstill) (*.net *.split) |
| 07:43:13 | × | xsarnik quits (xsarnik@lounge.fi.muni.cz) (*.net *.split) |
| 07:43:14 | × | dunj3 quits (~dunj3@kingdread.de) (*.net *.split) |
| 07:43:14 | × | turlando quits (~turlando@user/turlando) (*.net *.split) |
| 07:43:14 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (*.net *.split) |
| 07:43:14 | × | adium quits (adium@user/adium) (*.net *.split) |
| 07:43:14 | × | mcglk quits (~mcglk@131.191.19.145) (*.net *.split) |
| 07:43:14 | × | byorgey quits (~byorgey@155.138.238.211) (*.net *.split) |
| 07:43:14 | × | micro quits (~micro@user/micro) (*.net *.split) |
| 07:43:14 | × | davean quits (~davean@davean.sciesnet.net) (*.net *.split) |
| 07:43:14 | × | anderson quits (~ande@user/anderson) (*.net *.split) |
| 07:43:14 | × | madnight quits (~madnight@static.59.103.201.195.clients.your-server.de) (*.net *.split) |
| 07:43:14 | × | Cheery quits (~cheery@server-239-7.tentacle.cloud) (*.net *.split) |
| 07:43:14 | × | phileasfogg quits (~phileasfo@user/phileasfogg) (*.net *.split) |
| 07:43:14 | × | kraftwerk28 quits (~kraftwerk@178.62.210.83) (*.net *.split) |
| 07:43:14 | × | Dykam quits (Dykam@dykam.nl) (*.net *.split) |
| 07:43:14 | × | meejah quits (~meejah@rutas.meejah.ca) (*.net *.split) |
| 07:43:14 | × | heath1 quits (~heath@user/heath) (*.net *.split) |
| 07:43:14 | × | noctux1 quits (Zx24REiiwW@user/noctux) (*.net *.split) |
| 07:43:14 | × | dfordvm quits (~dfordivam@tk2-219-19469.vs.sakura.ne.jp) (*.net *.split) |
| 07:43:14 | × | guygastineau quits (~guygastin@137.184.131.156) (*.net *.split) |
| 07:43:14 | × | davl_ quits (~davl@207.154.228.18) (*.net *.split) |
| 07:43:14 | × | robbert-vdh quits (~robbert@robbertvanderhelm.nl) (*.net *.split) |
| 07:43:14 | × | ario quits (~ario@159.65.220.102) (*.net *.split) |
| 07:43:14 | × | defanor quits (~defanor@tart.uberspace.net) (*.net *.split) |
| 07:43:14 | × | hank_ quits (~hank@45-33-24-80.ip.linodeusercontent.com) (*.net *.split) |
| 07:43:15 | × | DigitalKiwi quits (~kiwi@137.184.156.191) (*.net *.split) |
| 07:43:15 | × | nicole quits (ilbelkyr@libera/staff/ilbelkyr) (*.net *.split) |
| 07:43:22 | → | comerijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 07:43:24 | → | byorgey joins (~byorgey@155.138.238.211) |
| 07:43:25 | → | xsarnik joins (xsarnik@lounge.fi.muni.cz) |
| 07:43:27 | → | dunj3 joins (~dunj3@kingdread.de) |
| 07:43:28 | → | defanor joins (~defanor@tart.uberspace.net) |
| 07:43:31 | → | institor joins (~absentia@66.234.62.215) |
| 07:43:31 | → | nicole joins (ilbelkyr@libera/staff/ilbelkyr) |
| 07:43:35 | → | micro joins (~micro@a9.lence.net) |
| 07:43:43 | → | ario joins (~ario@159.65.220.102) |
| 07:43:44 | → | jwiegley joins (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 07:43:52 | → | dfordvm joins (~dfordivam@tk2-219-19469.vs.sakura.ne.jp) |
| 07:43:58 | × | micro quits (~micro@a9.lence.net) (Changing host) |
| 07:43:58 | → | micro joins (~micro@user/micro) |
| 07:44:35 | → | Cheery joins (~cheery@server-239-7.tentacle.cloud) |
| 07:44:35 | → | freeside joins (~mengwong@50.216.111.242) |
| 07:44:40 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 07:44:51 | → | xstill_ joins (xstill@fimu/xstill) |
| 07:45:00 | → | noctux1 joins (vBYKluURgE@karif.server-speed.net) |
| 07:45:37 | → | Dykam joins (Dykam@dykam.nl) |
| 07:45:38 | → | Sauvin joins (~sauvin@user/Sauvin) |
| 07:45:41 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-50-65-93-192-141.dsl.bell.ca) |
| 07:45:41 | → | turlando joins (~turlando@user/turlando) |
| 07:45:44 | → | madnight joins (~madnight@static.59.103.201.195.clients.your-server.de) |
| 07:45:53 | → | enoq joins (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) |
| 07:46:05 | → | phileasfogg joins (~phileasfo@user/phileasfogg) |
| 07:46:06 | → | anderson joins (~ande@user/anderson) |
| 07:46:08 | → | DigitalKiwi joins (~kiwi@2604:a880:400:d0::1ca0:e001) |
| 07:46:09 | → | kraftwerk28 joins (~kraftwerk@178.62.210.83) |
| 07:46:19 | → | davl joins (~davl@207.154.228.18) |
| 07:46:24 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 07:46:35 | → | RMSBach joins (~guygastin@137.184.131.156) |
| 07:46:38 | → | davean joins (~davean@davean.sciesnet.net) |
| 07:46:43 | → | heath1 joins (~heath@user/heath) |
| 07:46:56 | → | adium joins (adium@user/adium) |
| 07:47:01 | → | robbert-vdh joins (~robbert@robbertvanderhelm.nl) |
| 07:47:45 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 07:48:43 | → | meejah joins (~meejah@rutas.meejah.ca) |
| 07:49:21 | <kuribas> | Why do I it easy, when there is a complicated solution? |
| 07:50:48 | <c_wraith> | kuribas: the lenses for tuple access are already polytypic... |
| 07:50:53 | → | mcglk joins (~mcglk@131.191.19.145) |
| 07:51:11 | <c_wraith> | > (1,2,3) ^. _3 |
| 07:51:12 | <lambdabot> | 3 |
| 07:51:16 | <c_wraith> | > (1,2,3,4,5) ^. _3 |
| 07:51:18 | <lambdabot> | 3 |
| 07:51:45 | <mauke> | inb4 costate comonad coalgebra |
| 07:51:47 | <kuribas> | c_wraith: sure, but they'll complicate the function signature. |
| 07:52:04 | <kuribas> | Btw, I would likely use a record instead of a tuple. |
| 07:52:25 | <fendor[m]> | kuribas: since it is in the context of beam, it is not as easy as I would like it to be |
| 07:52:39 | <fendor[m]> | or I am just not smart enough |
| 07:52:40 | <c_wraith> | I mean, they complicate it in exactly the way that says "this data structure has a third element" |
| 07:53:31 | <kuribas> | fendor[m]: ah right ... Yeah, I find beam tends to be quite complicated. |
| 07:53:57 | <fendor[m]> | it is, it is... Cool, but very complicated. |
| 07:55:11 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:00:58 | × | institor quits (~absentia@66.234.62.215) (Changing host) |
| 08:00:58 | → | institor joins (~absentia@user/institor) |
| 08:10:03 | × | enoq quits (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) (Quit: enoq) |
| 08:11:22 | → | vpan joins (~0@mail.elitnet.lt) |
| 08:12:22 | → | enoq joins (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) |
| 08:19:27 | → | Guest12345 joins (~Guest1234@79.191.65.29.ipv4.supernova.orange.pl) |
| 08:20:01 | × | Guest12345 quits (~Guest1234@79.191.65.29.ipv4.supernova.orange.pl) (Quit: Connection closed) |
| 08:21:25 | → | barcisz joins (~barcisz@79.191.65.29.ipv4.supernova.orange.pl) |
| 08:28:21 | <[exa]> | would be nice if GHC or hlint spewed a warning like "You might want to finally name the fields in this 6-tuple" |
| 08:29:32 | <Rembane> | Isn't it possible to add custom hlint rules? |
| 08:29:45 | <Rembane> | ...or is that me who has hallucinated that when on too much mountain dew? |
| 08:31:05 | <[exa]> | well, you can always download the hlint source and just add them, which kinda matches the mountain dew solution |
| 08:31:07 | → | jtza8 joins (~user@165.255.63.78) |
| 08:31:33 | <Rembane> | Too much mountain dew. I hoped there was a .hlint-rules file in the project folder. |
| 08:31:51 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Remote host closed the connection) |
| 08:32:14 | → | __monty__ joins (~toonn@user/toonn) |
| 08:35:15 | × | zer0bitz_ quits (~zer0bitz@2001:2003:f443:d600:c8fb:80d:3f21:d12f) () |
| 08:37:58 | <jtza8> | I've got a small personal project that I'm trying to build for my Termux environment on my android phone. I've tried to build my project directly on my phone, but I seem to run out of memory. Are there any known tricks I could use to build something in a limited-memory environment? |
| 08:39:04 | <jtza8> | I'm using GHC 9.2.5, cabal-install and the cabal.config from the Stackage lts-20.11. |
| 08:39:41 | <jtza8> | The largest dependancy is probably scotty. |
| 08:41:07 | → | zer0bitz joins (~zer0bitz@2001:2003:f443:d600:c8fb:80d:3f21:d12f) |
| 08:41:43 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 08:44:09 | ← | olle parts (~olle@h-155-4-129-160.NA.cust.bahnhof.se) () |
| 08:51:04 | × | raym quits (~ray@user/raym) (Ping timeout: 255 seconds) |
| 08:55:01 | <tomsmeding> | jtza8: using cabal build -j1, for starters |
| 08:55:55 | <tomsmeding> | you may also try to set 'ghc-options: +RTS -M2G -RTS', which sets GHC's maximum heap size to 2 GiB |
| 08:56:05 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 08:56:11 | → | mncheck joins (~mncheck@193.224.205.254) |
| 08:56:14 | <tomsmeding> | (change the 2 to whatever you want, note that "heap size 2GiB" does not necessarily mean "resident memory usage 2GiB") |
| 08:56:27 | <tomsmeding> | also turn off optimisations, i.e. ghc-options: -O0 |
| 08:56:48 | <tomsmeding> | (there's probably a cabal.project flag for the latter) |
| 08:57:05 | → | zer0bitz_ joins (~zer0bitz@2001:2003:f443:d600:4118:2d56:8c2b:a747) |
| 08:57:48 | × | zer0bitz_ quits (~zer0bitz@2001:2003:f443:d600:4118:2d56:8c2b:a747) (Client Quit) |
| 08:58:16 | × | zer0bitz quits (~zer0bitz@2001:2003:f443:d600:c8fb:80d:3f21:d12f) (Ping timeout: 252 seconds) |
| 08:59:36 | × | mikess quits (~sam@user/mikess) (Ping timeout: 255 seconds) |
| 09:00:08 | × | joebe[m] quits (~joebematr@2001:470:69fc:105::3:2c53) (Quit: You have been kicked for being idle) |
| 09:01:51 | → | ubert joins (~Thunderbi@2a02:8109:abc0:6434:2d8a:83f8:5c8d:71a3) |
| 09:02:23 | <jtza8> | tomsmeding: Thank you for your answer. I realise it's a bit of a foolhardy thing to do, but if this works I won't need to try and figure out how to get cross-compiling to work just yet. :P |
| 09:02:49 | <tomsmeding> | jtza8: I've been in a similar situation trying to compile stuff on a cheap VPS |
| 09:03:00 | <tomsmeding> | at some point I gave up and gave the thing 4 GiB of swap space |
| 09:03:12 | → | zer0bitz joins (~zer0bitz@2001:2003:f443:d600:4118:2d56:8c2b:a747) |
| 09:03:23 | <tomsmeding> | that was just enough to get aeson and vector to compile, iirc |
| 09:03:38 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 09:03:40 | <tomsmeding> | (though I didn't disable optimisations) |
| 09:04:08 | <__monty__> | jtza8: FWIW, I hear cross-compilation can be pretty "easy" using Nix. |
| 09:04:33 | <tomsmeding> | question is, does nix support termux-android as a compilation target |
| 09:04:41 | <tomsmeding> | which undoubtedly is not quite the usual ARM target |
| 09:05:19 | <__monty__> | I didn't think the Termux part would matter? |
| 09:05:27 | <tomsmeding> | libraries and stuff are in weird places |
| 09:05:39 | <tomsmeding> | but yeah maybe it matters less than I fear |
| 09:06:03 | tomsmeding | wonders how much the termux ghc is patched |
| 09:06:25 | <__monty__> | I don't actually have experience with cross-compiling so, caveat emptor. |
| 09:08:19 | × | ft quits (~ft@p4fc2a88b.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:10:22 | × | forell quits (~forell@user/forell) (Quit: ZNC - https://znc.in) |
| 09:10:32 | → | son0p joins (~ff@181.136.122.143) |
| 09:11:46 | <jtza8> | __monty__: Haskell.nix seems to be a good way to go. And they have support for Android (which has a non-GNU libc.) |
| 09:12:38 | <jtza8> | I'm just a little new to Nix too. Although it's been a delight to use so far. |
| 09:12:41 | → | forell joins (~forell@user/forell) |
| 09:19:36 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 09:22:03 | → | zeenk joins (~zeenk@2a02:2f04:a307:2300::7fe) |
| 09:23:07 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 3.8) |
| 09:25:55 | → | NiceBird joins (~NiceBird@185.133.111.196) |
| 09:27:12 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 09:27:42 | × | megaTherion quits (~therion@unix.io) (Quit: ZNC 1.8.2 - https://znc.in) |
| 09:28:34 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 09:29:25 | → | megaTherion joins (~therion@unix.io) |
| 09:30:20 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Quit: use-value) |
| 09:30:24 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 09:32:19 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 09:37:13 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 09:37:49 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Ping timeout: 250 seconds) |
| 09:39:52 | → | zmt00 joins (~zmt00@user/zmt00) |
| 09:42:16 | → | raym joins (~ray@user/raym) |
| 09:43:01 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 250 seconds) |
| 09:44:35 | ← | jtza8 parts (~user@165.255.63.78) (ERC 5.4 (IRC client for GNU Emacs 28.2)) |
| 09:46:19 | × | chanceyan quits (~chanceyan@user/chanceyan) (Quit: Client closed) |
| 09:50:34 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 10:02:51 | → | cfricke joins (~cfricke@user/cfricke) |
| 10:05:29 | → | vglfr joins (~vglfr@88.155.5.190) |
| 10:07:08 | → | gtdg joins (~gtdg@user/gtdg) |
| 10:15:03 | × | dsrt^ quits (~dsrt@c-76-105-96-13.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 10:16:59 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 10:23:25 | × | vglfr quits (~vglfr@88.155.5.190) (Ping timeout: 240 seconds) |
| 10:24:22 | → | vglfr joins (~vglfr@88.155.5.190) |
| 10:25:38 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 265 seconds) |
| 10:25:44 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 10:39:41 | → | JScript joins (~JScript@144.48.39.6) |
| 10:42:28 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 10:49:19 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 250 seconds) |
| 11:10:28 | × | razetime quits (~Thunderbi@117.193.5.39) (Quit: See You Space Cowboy) |
| 11:14:47 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:17:27 | → | xff0x joins (~xff0x@ai098135.d.east.v6connect.net) |
| 11:17:59 | → | kei joins (~kei@42.105.220.41) |
| 11:27:22 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 11:33:23 | × | paulpaul1076 quits (~textual@95-29-5-208.broadband.corbina.ru) (Remote host closed the connection) |
| 11:38:53 | × | kei quits (~kei@42.105.220.41) (Ping timeout: 260 seconds) |
| 11:41:15 | → | kei joins (~kei@42.105.218.54) |
| 11:41:30 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 11:42:24 | × | pyook quits (~puke@user/puke) (Ping timeout: 248 seconds) |
| 11:42:29 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 255 seconds) |
| 11:43:11 | → | pyook joins (~puke@user/puke) |
| 11:45:16 | hopelessness[m] | uploaded an image: (118KiB) < https://libera.ems.host/_matrix/media/v3/download/matrix.org/EKEKSNMTzltbkddHsOfuNQvW/SmartSelect_20230412_134458_Firefox.jpg > |
| 11:45:18 | <hopelessness[m]> | literally wow |
| 11:45:45 | <tomsmeding> | hopelessness[m]: where's that from? |
| 11:45:45 | <hopelessness[m]> | someone that writes haskell like this should not write about it |
| 11:45:51 | <hopelessness[m]> | just... don't |
| 11:46:00 | <tomsmeding> | but yes the spacing is kinda... off |
| 11:46:08 | <hopelessness[m]> | tutorialspoint ... they are awful |
| 11:46:42 | <hopelessness[m]> | tomsmeding: not even the formatting, I can look beyond that |
| 11:46:42 | <tomsmeding> | wonder what ghc version they have running on the backend |
| 11:46:46 | <tomsmeding> | true |
| 11:47:10 | <hopelessness[m]> | it's just horrible code, like they are trying to use it as an imperative language |
| 11:47:37 | <hopelessness[m]> | they nest do-blocks for no reason |
| 11:47:50 | <tomsmeding> | well, they're inside an if |
| 11:48:39 | <comerijn> | tbh, the biggest crime there is the then/else indentation |
| 11:48:44 | <comerijn> | the rest looks mostly fine, tbh |
| 11:49:11 | <tomsmeding> | ghc 8.8 apparently |
| 11:49:16 | <comerijn> | Pretty sure that requires one of those stupid relaxed if syntax rules that I'm not even sure are a part of 2010 |
| 11:49:20 | <tomsmeding> | (System.Info.compilerVersion) |
| 11:49:30 | <hopelessness[m]> | they are "initializing" the list with something they are ignoring |
| 11:50:17 | <hopelessness[m]> | it's really really odd |
| 11:50:35 | <tomsmeding> | oh lol what |
| 11:50:45 | <tomsmeding> | I didn't even try to read what it was actually doing |
| 11:51:12 | <hopelessness[m]> | yeah, exactly |
| 11:51:58 | × | mud quits (~mud@user/kadoban) (Ping timeout: 276 seconds) |
| 11:52:01 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 11:53:00 | <int-e> | . o O ( Today I learned: In Haskell, the empty list is denoted as [-1]. But in order to print it, you have to call `init` first. ) |
| 11:54:38 | <darkling> | I think the icon in the top right is important. You clearly have to edit it first before it'll run. |
| 11:54:43 | <tomsmeding> | wait until you need an empty list of non-numbers |
| 11:55:01 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 265 seconds) |
| 11:55:16 | <tomsmeding> | it will actually run, though not usefully because the system provides no input on stdin |
| 12:01:48 | <int-e> | darkling: It does work as written though. |
| 12:02:45 | <darkling> | My brain just says that something that looks so horrible has no right to work. :) |
| 12:03:08 | <int-e> | darkling: Actually, it *did* work as written up to ghc 8.10 |
| 12:03:12 | <int-e> | https://downloads.haskell.org/ghc/latest/docs/users_guide/bugs.html#context-free-syntax |
| 12:03:45 | <int-e> | (9.0 changed the language default to Haskell2010 rather than Haskell98) |
| 12:05:09 | <tomsmeding> | didn't they change it to GHC2021 instead? |
| 12:05:22 | <int-e> | tomsmeding: Uh, maybe. |
| 12:05:29 | <int-e> | darkling: I do agree, however, that it shouldn't work; accepting this totally defeats the purose of indentation. |
| 12:06:31 | × | razetime quits (~Thunderbi@117.193.5.39) (Quit: See You Space Cowboy) |
| 12:08:10 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 260 seconds) |
| 12:09:09 | <int-e> | Oh I got it all wrong. 9.2 changed the default language, to GHC2021. |
| 12:09:34 | <int-e> | And that atrociously indented code is still accepted by default in 9.0 |
| 12:11:48 | × | kei quits (~kei@42.105.218.54) (Quit: Client closed) |
| 12:12:54 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 12:31:33 | × | kenran quits (~user@user/kenran) (Ping timeout: 255 seconds) |
| 12:53:38 | × | razetime quits (~Thunderbi@117.193.5.39) (Remote host closed the connection) |
| 12:54:40 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 13:05:43 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 13:08:06 | <juri_> | oh, thank god, that screenshot isn't my code. |
| 13:09:19 | × | razetime quits (~Thunderbi@117.193.5.39) (Quit: See You Space Cowboy) |
| 13:10:31 | <juri_> | i've been working on my slicer for long enough, and it's become large enough, that on occasion, i go to a section of the program i haven't had to touch in a long time, go "who wrote this crap?", then think oh. its me. i wrote that utter shite. |
| 13:11:52 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Quit: use-value) |
| 13:13:33 | → | biberu joins (~biberu@user/biberu) |
| 13:15:06 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 13:15:46 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Client Quit) |
| 13:16:28 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 13:18:11 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Client Quit) |
| 13:20:51 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 13:23:16 | → | paulpaul1076 joins (~textual@95-29-5-208.broadband.corbina.ru) |
| 13:27:34 | → | razetime joins (~Thunderbi@117.193.5.39) |
| 13:28:38 | × | razetime quits (~Thunderbi@117.193.5.39) (Client Quit) |
| 13:31:46 | → | gensyst joins (~gensyst@user/gensyst) |
| 13:32:15 | → | zer0bitz_ joins (~zer0bitz@2001:2003:f443:d600:1d40:2e2d:a29f:cc19) |
| 13:32:48 | × | zer0bitz quits (~zer0bitz@2001:2003:f443:d600:4118:2d56:8c2b:a747) (Ping timeout: 246 seconds) |
| 13:34:24 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 13:34:35 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 13:34:42 | <gensyst> | When you have "extra-libraries" in .cabal, why does Nix/haskellPackages seem to grab these things from the haskellPackages as opposed to the top-level nixpkgs? |
| 13:34:56 | <gensyst> | extra-libraries are supposed to be system libraries right? |
| 13:34:56 | → | __monty__ joins (~toonn@user/toonn) |
| 13:36:47 | → | MasseR46 joins (thelounge@2001:bc8:47a0:1521::1) |
| 13:37:54 | → | kenran joins (~user@user/kenran) |
| 13:40:08 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 13:41:10 | <Artem[m]> | gensyst: you may have better luck asking in the Nix Haskell Matrix room https://matrix.to/#/#haskell:nixos.org |
| 13:47:30 | × | xff0x quits (~xff0x@ai098135.d.east.v6connect.net) (Quit: xff0x) |
| 13:49:05 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 240 seconds) |
| 13:52:49 | → | xff0x joins (~xff0x@2405:6580:b080:900:22cb:546d:6546:a19b) |
| 13:53:44 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 13:55:46 | → | angelore joins (~u0_a291@37.214.66.179) |
| 13:56:10 | × | angelore quits (~u0_a291@37.214.66.179) (Client Quit) |
| 13:59:30 | → | mikess joins (~sam@user/mikess) |
| 14:01:01 | → | Square joins (~Square4@user/square) |
| 14:02:51 | → | ddellacosta joins (~ddellacos@146.70.166.152) |
| 14:06:34 | <yin> | is the set of legal symbols for infix type synonyms the same as for any infix function? |
| 14:08:41 | <comerijn> | yin: I think so |
| 14:10:41 | → | thegeekinside joins (~thegeekin@189.217.90.138) |
| 14:11:21 | <yin> | oh but we can start a type synonym with : |
| 14:15:30 | × | michalz quits (~michalz@185.246.204.107) (Ping timeout: 255 seconds) |
| 14:15:33 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 14:15:49 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 14:16:06 | → | __monty__ joins (~toonn@user/toonn) |
| 14:16:58 | → | notzmv joins (~zmv@user/notzmv) |
| 14:17:37 | <comerijn> | yin: Originaly you *had* to use : for type synonyms, because they followed the logic that the valid syntax for them matches constructors (and : is the canonical "capital" symbol used for infix constructors) |
| 14:18:20 | <comerijn> | yin: At some point they relaxed to the rule for infix type synonyms to no longer require a starting :, abandonning the constructor naming scheme that applies for "normal" type synonyms, etc. |
| 14:18:37 | <comerijn> | Hence the inconsistency |
| 14:18:55 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:e94a:711d:cca5:b3e) (Quit: WeeChat 2.8) |
| 14:20:07 | <yin> | i came across some code that had non-: infix type synonyms and found it weird. thanks for the explanation |
| 14:24:02 | → | jero98772 joins (~jero98772@190.158.28.80) |
| 14:26:25 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 250 seconds) |
| 14:27:25 | × | JScript quits (~JScript@144.48.39.6) (Ping timeout: 240 seconds) |
| 14:30:41 | × | freeside quits (~mengwong@50.216.111.242) (Ping timeout: 265 seconds) |
| 14:31:16 | <probie> | They seem fairly common these days, especially when the type synonym looks like an arrow |
| 14:31:23 | × | ddellacosta quits (~ddellacos@146.70.166.152) (Quit: WeeChat 3.8) |
| 14:31:34 | <albet70> | what's eDSLs? |
| 14:32:11 | <Square> | embedded DSL? |
| 14:32:30 | → | ddellacosta joins (~ddellacos@146.70.166.152) |
| 14:34:20 | <Square> | http://wiki.haskell.org/Embedded_domain_specific_language |
| 14:37:11 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 14:37:40 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 14:41:57 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Ping timeout: 256 seconds) |
| 14:42:33 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.8) |
| 14:46:54 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:53:07 | × | hueso quits (~root@user/hueso) (Ping timeout: 260 seconds) |
| 14:54:46 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Quit: WeeChat 3.8) |
| 14:58:14 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 14:58:29 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 14:59:49 | × | ddellacosta quits (~ddellacos@146.70.166.152) (Ping timeout: 276 seconds) |
| 15:01:12 | → | ddellacosta joins (~ddellacos@143.244.47.83) |
| 15:01:29 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:02:30 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 15:05:59 | × | zeenk quits (~zeenk@2a02:2f04:a307:2300::7fe) (Quit: Konversation terminated!) |
| 15:23:12 | × | kenran quits (~user@user/kenran) (Ping timeout: 248 seconds) |
| 15:27:21 | × | mcglk quits (~mcglk@131.191.19.145) (Quit: (seeya)) |
| 15:28:53 | <probie> | Is there much prior art on generics that support GADTs, or is this a mostly empty space? I can find kind-generics which seems seldom used. Are there other approaches? |
| 15:35:35 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 15:39:21 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Quit: use-value) |
| 15:40:01 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 15:41:44 | → | cheater_ joins (~Username@user/cheater) |
| 15:43:39 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 15:43:40 | cheater_ | is now known as cheater |
| 15:44:28 | × | mbuf quits (~Shakthi@49.207.178.186) (Quit: Leaving) |
| 15:46:13 | × | gtdg quits (~gtdg@user/gtdg) (Ping timeout: 260 seconds) |
| 15:49:00 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Quit: use-value) |
| 15:49:40 | × | mikess quits (~sam@user/mikess) (Ping timeout: 252 seconds) |
| 15:49:46 | <TheMatten[m]> | <probie> "Is there much prior art on..." <- I have an old prototype of generics interface using `DataKinds` - I think it should be extensible with support for GADTs by adding existential and dictionary constructor: https://gitlab.com/thematten/simple-generics/-/blob/master/src/Generics/Simple.hs |
| 15:51:20 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:95f6:6e4e:c0f4:2cf2) |
| 15:57:20 | × | dipper quits (~dipper@203.168.11.65) (Ping timeout: 248 seconds) |
| 15:57:30 | → | econo joins (uid147250@user/econo) |
| 15:58:36 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 15:59:01 | × | vpan quits (~0@mail.elitnet.lt) (Quit: Leaving.) |
| 16:04:59 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 16:08:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 16:14:36 | → | freeside joins (~mengwong@68.65.175.90) |
| 16:16:01 | × | jle` quits (~jle`@cpe-23-240-75-236.socal.res.rr.com) (Ping timeout: 265 seconds) |
| 16:17:38 | → | jle` joins (~jle`@cpe-23-240-75-236.socal.res.rr.com) |
| 16:18:11 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 264 seconds) |
| 16:18:25 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 260 seconds) |
| 16:18:56 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Quit: use-value) |
| 16:19:56 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 16:20:04 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 16:20:58 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Client Quit) |
| 16:23:08 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:95f6:6e4e:c0f4:2cf2) (Quit: WeeChat 2.8) |
| 16:32:03 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 16:42:37 | × | zmt00 quits (~zmt00@user/zmt00) (Quit: Leaving) |
| 16:53:14 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 17:00:55 | × | Alex_test quits (~al_test@178.34.162.18) (Quit: ;-) |
| 17:01:34 | × | AlexZenon quits (~alzenon@178.34.162.18) (Quit: ;-) |
| 17:02:31 | × | AlexNoo quits (~AlexNoo@178.34.162.18) (Quit: Leaving) |
| 17:03:25 | × | ubert quits (~Thunderbi@2a02:8109:abc0:6434:2d8a:83f8:5c8d:71a3) (Remote host closed the connection) |
| 17:03:39 | → | ubert joins (~Thunderbi@2a02:8109:abc0:6434:bd33:950c:bf25:e78b) |
| 17:05:55 | → | kimjetwav joins (~user@2607:fea8:235e:b600:f874:36b2:8b2c:6f8c) |
| 17:06:17 | → | mikess joins (~sam@user/mikess) |
| 17:07:10 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 17:09:02 | → | AlexNoo joins (~AlexNoo@178.34.162.18) |
| 17:11:07 | → | Square2 joins (~Square4@user/square) |
| 17:11:12 | × | mikess quits (~sam@user/mikess) (Ping timeout: 246 seconds) |
| 17:13:16 | × | Square quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 17:16:34 | → | hochata joins (~user@user/hochata) |
| 17:16:54 | → | AlexZenon joins (~alzenon@178.34.162.18) |
| 17:17:07 | × | ubert quits (~Thunderbi@2a02:8109:abc0:6434:bd33:950c:bf25:e78b) (Quit: ubert) |
| 17:17:15 | → | hochata` joins (~user@2806:104e:1b:41de:3e48:b302:2801:10c5) |
| 17:18:25 | × | hochata` quits (~user@2806:104e:1b:41de:3e48:b302:2801:10c5) (Client Quit) |
| 17:18:41 | × | hochata quits (~user@user/hochata) (Client Quit) |
| 17:19:08 | → | hochata joins (~user@user/hochata) |
| 17:23:11 | → | olle joins (~olle@h-155-4-129-160.NA.cust.bahnhof.se) |
| 17:24:26 | → | irrgit joins (~irrgit@86.106.90.226) |
| 17:25:17 | <olle> | Regarding deferred If you *can* defer, say, a write, *should* you defer it? |
| 17:25:26 | <olle> | Regarding deferred effects* |
| 17:26:51 | <olle> | Consider a process_order function that also writes a new order to the database after a number of calculations. Would you prefer to have it handing you an effect object instead of a success result? |
| 17:27:46 | → | Alex_test joins (~al_test@178.34.162.18) |
| 17:30:03 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 17:33:19 | → | mikess joins (~sam@user/mikess) |
| 17:37:10 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 17:38:06 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 17:38:54 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 17:39:14 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) |
| 17:50:37 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: sdvfsjsl) |
| 18:01:54 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 18:02:16 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 18:02:35 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 18:03:50 | → | ubert joins (~Thunderbi@p200300ecdf114f00fa3b3daf889d0c1b.dip0.t-ipconnect.de) |
| 18:03:58 | × | zer0bitz_ quits (~zer0bitz@2001:2003:f443:d600:1d40:2e2d:a29f:cc19) () |
| 18:08:09 | × | ubert quits (~Thunderbi@p200300ecdf114f00fa3b3daf889d0c1b.dip0.t-ipconnect.de) (Client Quit) |
| 18:08:37 | → | zer0bitz joins (~zer0bitz@2001:2003:f443:d600:1d40:2e2d:a29f:cc19) |
| 18:13:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 18:15:28 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 276 seconds) |
| 18:17:08 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 18:18:43 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 18:18:47 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 18:18:49 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 18:21:35 | → | LenarHoyt joins (~LenarHoyt@2a02:908:f13:daa3:d857:3f2f:13fa:1d70) |
| 18:26:12 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 18:28:47 | → | codaraxis__ joins (~codaraxis@user/codaraxis) |
| 18:32:32 | × | codaraxis quits (~codaraxis@user/codaraxis) (Ping timeout: 248 seconds) |
| 18:34:20 | × | Angelz quits (Angelz@user/angelz) (Quit: IRCNow and Forever!) |
| 18:50:04 | × | matijja quits (~matijja@193.77.181.201) (Quit: ZNC 1.8.2 - https://znc.in) |
| 18:50:50 | → | matijja joins (~matijja@193.77.181.201) |
| 18:57:09 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 19:12:04 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3438:d5fd:19ed:dac6) (Quit: use-value) |
| 19:12:20 | <nomagno> | In the Maybe monad, is Nothing a special case of Just foo ? |
| 19:12:43 | <Rembane> | No, they are two different cases of Maybe foo. |
| 19:13:47 | <[exa]> | what is a "special case" |
| 19:14:06 | <nomagno> | Well, specific case |
| 19:14:25 | <[exa]> | what metric of specificity? |
| 19:14:45 | × | freeside quits (~mengwong@68.65.175.90) (Ping timeout: 240 seconds) |
| 19:14:57 | <[exa]> | like, they are 2 completely different constructors with 2 completely different implementations of the bind (and other things) |
| 19:16:36 | <hopelessness[m]> | Maybe is a sum type (meaning a type that can assume multiple different forms), specifically it is either `Nothing` or `Just a` where `a` is something "contained" in the maybe |
| 19:16:46 | <hopelessness[m]> | these are called constructors in haskell |
| 19:19:38 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 19:21:42 | <nomagno> | Is Maybe in the monad form a monad, or a sum type of monads? I'm trying to build some kind of mental relationship between the monadic laws and Maybe |
| 19:22:01 | <hopelessness[m]> | what I explained has nothing to do with monads |
| 19:22:12 | <hopelessness[m]> | Maybe (the type) is a monad |
| 19:22:46 | → | Square joins (~Square@user/square) |
| 19:22:47 | <hopelessness[m]> | the specific constructors are simply how the type is internally constructed |
| 19:23:29 | × | Square2 quits (~Square4@user/square) (Ping timeout: 246 seconds) |
| 19:24:18 | → | mei joins (~mei@user/mei) |
| 19:26:24 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 248 seconds) |
| 19:26:25 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 256 seconds) |
| 19:26:39 | → | ft joins (~ft@p4fc2a88b.dip0.t-ipconnect.de) |
| 19:27:34 | <nomagno> | I'm going to use the Wikipedia definition's terms here. A value of type `Maybe` has to look like `M T`. So in `m x`, the `x` can't be empty, that doesn't make sense and then `>>=` stops working. But if `Nothing` is the `x` when a function returns a value of type `Maybe` with specific value `Nothing`, `x` doesn't have type `T`, it has type `T + [some type with the only value "Nothing"] `... |
| 19:27:42 | → | freeside joins (~mengwong@68.65.175.90) |
| 19:27:59 | <c_wraith> | nomagno: you're conflating value and type levels |
| 19:28:06 | <nomagno> | I'm thinking about it wrong here, but I don't know how I'm thinking about it wrong |
| 19:28:19 | <c_wraith> | nomagno: in 'm x', those are both *type* expressions |
| 19:28:20 | <hopelessness[m]> | Nothing is not Just (Nothing) |
| 19:29:01 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 19:29:38 | <ncf> | "A value of type `Maybe`" is already wrong: Maybe is not a type, it's a type constructor |
| 19:29:57 | <nomagno> | A value of type Maybe T, alright |
| 19:30:08 | <c_wraith> | for instance, `Nothing :: Maybe Integer' and `Just 5 :: Maybe Integer' may have different value-level structures, but both have the type Maybe Integer |
| 19:30:14 | <ncf> | a value of type Maybe T looks like Nothing or Just t (for some t : T) |
| 19:31:35 | <nomagno> | But that makes no sense, if `Maybe T` looks like `Nothing`, then it doesn't hold that `unit x >>= f iff f(x)`... Or maybe it does? |
| 19:31:48 | <c_wraith> | once again, those are different levels |
| 19:31:53 | <c_wraith> | types and values are different |
| 19:32:02 | <c_wraith> | Think about them separately |
| 19:32:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 19:32:37 | <c_wraith> | `unit x' cannot be `Nothing' |
| 19:32:50 | <c_wraith> | (in haskell, unit is usually spelled "pure") |
| 19:33:02 | <nomagno> | So, if unit x cannot be Nothing, f(x) is just not? |
| 19:33:14 | <ncf> | the unit of the Maybe monad is Just :: a -> Maybe a |
| 19:33:44 | <ncf> | the law you're talking about says that Just x >>= f == f x, which is just part of the definition of >>= for Maybe |
| 19:34:08 | <ncf> | the other part says what happens to Nothing |
| 19:34:19 | <nomagno> | But, the law specifically does not talk about Nothing? |
| 19:34:50 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 19:34:59 | <c_wraith> | true. the law doesn't define all the behavior. it just puts a constraint on it |
| 19:35:31 | <nomagno> | But, we still have that same monad of type M T... Wait no, bind returns a monad of type M U, oooooh |
| 19:35:31 | <c_wraith> | the type-specific implementation defines all the behavior. And if it's lawful, it obeys the constraints. |
| 19:36:20 | <nomagno> | This means that `Nothing >>= f` doesn't have an "obligation to be a valid statement" at all, according to the monad laws? |
| 19:36:29 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 19:36:29 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 19:36:36 | <c_wraith> | yeah. I think any presentation of the laws that doesn't give the types of the free variables is seriously lacking |
| 19:36:47 | <hopelessness[m]> | what do you mean by valid statement? |
| 19:36:57 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 19:37:03 | <hopelessness[m]> | monad laws don't really apply here |
| 19:37:19 | <ncf> | that's a value, not a statement |
| 19:37:23 | <hopelessness[m]> | hopelessness[m]: non-compiler enforced laws I should say |
| 19:37:25 | <c_wraith> | actually, the laws do apply. |
| 19:37:27 | <hopelessness[m]> | * non-compiler/type enforced |
| 19:37:30 | → | gmg joins (~user@user/gehmehgeh) |
| 19:37:35 | <c_wraith> | Because of the associativity law |
| 19:37:56 | <c_wraith> | but the identity laws don't apply |
| 19:38:09 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 19:38:10 | × | gurkenglas quits (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 19:38:36 | <nomagno> | If f expects an Int, it can't be fed Nothing, even if Nothing is a Maybe Int? Is this correct? Or is Nothing just its own monadic type M U now? |
| 19:39:11 | <c_wraith> | so the first part is absolutely true. `Nothing >>= f' cannot call f |
| 19:39:56 | <c_wraith> | So the only way to produce a total, type-checking result is for `Nothing >>= _ = Nothing' |
| 19:40:09 | <hopelessness[m]> | `Nothing >>= f` will always evaluate to `Nothing` because it's defined that way (`Nothing >>= _ = Nothing`) |
| 19:40:59 | <c_wraith> | Note that that isn't because of the monad laws - it's due to parametricity |
| 19:41:17 | <nomagno> | c_wraith: that's a violation of the left-identity law though, no? |
| 19:41:29 | <hopelessness[m]> | no |
| 19:41:37 | <hopelessness[m]> | return a = Just a |
| 19:41:47 | <hopelessness[m]> | return will never give you a Nothing |
| 19:42:19 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 250 seconds) |
| 19:42:25 | <c_wraith> | (parametricity is a separate big thing. It's more important than anything about monads in really understanding Haskell types.) |
| 19:42:31 | <hopelessness[m]> | s//`/, s//` (or rather `return = pure` which is the same thing in the end)/ |
| 19:43:57 | <ncf> | if f expects an Int, it doesn't expect a Maybe Int |
| 19:44:03 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 250 seconds) |
| 19:44:21 | <nomagno> | But `>>=` is supposed to fix that |
| 19:44:44 | <hopelessness[m]> | ehhh, I understand what you mean but it's not really correct |
| 19:45:04 | <ncf> | >>= fixes that in the specific case where f also *produces* a Maybe something |
| 19:45:13 | <hopelessness[m]> | but we are using ambiguous language - what is "expects" for a function? |
| 19:45:27 | <hopelessness[m]> | unless I'm just being stupid right now |
| 19:45:29 | <ncf> | that is, if f :: Int -> Maybe b, then (>>= f) :: Maybe Int -> Maybe b |
| 19:45:43 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 260 seconds) |
| 19:46:14 | <ncf> | you can see Maybe as representing a "possible failure", and >>= as saying "carry over the possible failure of the input into the output" |
| 19:48:19 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 19:48:23 | <nomagno> | if we have `x` with type `Maybe Int`, `f` with type `Int -> Maybe Int`, and `g` with type `Int -> Maybe Int`; `x >>= f >>= g`. If `f` returns `Nothing`, what does `g(...)` look like now? |
| 19:48:38 | <nomagno> | That's as close to my actual question as I've gotten |
| 19:49:12 | <hopelessness[m]> | g is g, the entire expression will return Nothing |
| 19:49:15 | <ncf> | if f returns Nothing, then the entire computation evaluates to Nothing |
| 19:49:49 | <nomagno> | But `g` expects an `Int`, and `f` has returned a `Maybe Int`, which has a specific `>>=` implementation, not two! |
| 19:49:50 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 19:49:55 | <nomagno> | Or CAN it have two? |
| 19:49:58 | <ddellacosta> | nomagno: maybe it would help to just look at the code? https://hackage.haskell.org/package/base-4.18.0.0/docs/src/GHC.Base.html#line-1133 |
| 19:50:06 | <hopelessness[m]> | `>>=` handles both cases |
| 19:50:10 | <nomagno> | Oh, if-then-else clause inside the `>>=`, lol |
| 19:50:15 | <nomagno> | Yeah I just realized writing it out |
| 19:50:21 | <hopelessness[m]> | there is no if-else |
| 19:50:25 | <hopelessness[m]> | just pattern matching |
| 19:50:56 | <nomagno> | Well, I understood now |
| 19:50:57 | <nomagno> | Jeez I didn't even consider >>= handling it like that |
| 19:50:57 | <nomagno> | Thanks! |
| 19:51:05 | × | freeside quits (~mengwong@68.65.175.90) (Ping timeout: 240 seconds) |
| 19:51:14 | <nomagno> | So THIS is what "computation policy" means |
| 19:52:30 | <c_wraith> | I suppose that's no worse than any other phrase I've seen used |
| 19:53:04 | ← | olle parts (~olle@h-155-4-129-160.NA.cust.bahnhof.se) () |
| 19:55:40 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 19:56:38 | <nomagno> | So, when `>>=` handles `Nothing`, it's handling a value that hasn't been constructed with `unit`, freeing it from the left-identity and right-identity laws? |
| 19:57:06 | <c_wraith> | correct |
| 19:57:34 | <c_wraith> | (the associativity law does still put some requirements on its behavior) |
| 20:00:32 | → | gurkenglas joins (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) |
| 20:00:35 | → | johnw joins (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 20:01:06 | <johnw> | Is anyone using GNU global with Haskell files? I have Pygments setup and gtags --explain shows that it's processing the file as a Haskell file, but it finds zero definitions, not in any of my files. |
| 20:02:14 | <nomagno> | `>>=` may also perform additional computations with the result of `f`? |
| 20:02:42 | <c_wraith> | nomagno: sure. Look at the Monad instance for Writer, for example |
| 20:03:26 | ← | johnw parts (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (ERC 5.4 (IRC client for GNU Emacs 28.2)) |
| 20:03:30 | <c_wraith> | Well. don't. It's a mess because of historical reasons involving trying to share as much code as possible :) |
| 20:03:36 | <nomagno> | Yes, but in the Monad instance for Writer, it's never touching the "boxed" part, only the "box", if thay makes sense |
| 20:03:37 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:03:48 | <c_wraith> | true |
| 20:03:56 | <c_wraith> | and that's sort of what the laws say it must do |
| 20:05:21 | <nomagno> | You can easily bypass this by having a version of unit that isn't unit though, right? And everything constructed with this unitClone would similarly not be helt to the identity laws |
| 20:05:41 | <nomagno> | Though you start to degrade the usefulness of monads then, I guess |
| 20:05:48 | <hopelessness[m]> | no |
| 20:05:58 | <c_wraith> | The whole point of Monad is that it's *only* that specific interface |
| 20:06:03 | <hopelessness[m]> | you cannot construct types outside of the constructors |
| 20:06:12 | <nomagno> | Ahhhhh |
| 20:06:15 | <c_wraith> | anything outside of that interface isn't part of Monad. It's part of something else |
| 20:06:33 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 20:06:33 | <nomagno> | Wait, so Nothing is only allowed because it's a constant? |
| 20:06:40 | <hopelessness[m]> | because it's a constructor of the Maybe type |
| 20:06:47 | <c_wraith> | Nothing is allowed because you know you're working with Maybe |
| 20:06:59 | <hopelessness[m]> | data Maybe a = Just a | Nothing |
| 20:07:27 | <c_wraith> | If you were working with the generic interface, on the other hand, you wouldn't have Nothing available because you wouldn't know m ~ Maybe |
| 20:07:29 | × | barcisz quits (~barcisz@79.191.65.29.ipv4.supernova.orange.pl) (Quit: Connection closed) |
| 20:07:31 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 20:07:32 | × | gensyst quits (~gensyst@user/gensyst) (Quit: Leaving) |
| 20:08:48 | <nomagno> | I'm not talking about Haskell anymore here, sorry for not clarifying. In the general case, you COULD have all sorts of values that are M T but constructed in weird ways not through unit, no? It takes away the point of monads, but still |
| 20:09:27 | → | Guest|81 joins (~Guest|81@200.19.106.219) |
| 20:09:57 | <hopelessness[m]> | what are you talking about then? |
| 20:09:58 | <hopelessness[m]> | Category theory? |
| 20:10:05 | <c_wraith> | 1. yes, you can have all sorts of additional stuff. 2. It doesn't take away the point of monads, because it's *outside the scope*. forming a monad just means that it has a specific structure. It says nothing at all about any other structures that may be present. |
| 20:10:32 | <nomagno> | I'm trying to understand monads conceptually |
| 20:10:55 | <hopelessness[m]> | so category theory? |
| 20:11:03 | × | LenarHoyt quits (~LenarHoyt@2a02:908:f13:daa3:d857:3f2f:13fa:1d70) (Ping timeout: 260 seconds) |
| 20:11:33 | <nomagno> | If I say yes, I'd immediately go over my knowledge pay grade, so no, but otherwise yes |
| 20:11:57 | <nomagno> | I'm happy enough as-is though |
| 20:12:31 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 20:12:35 | <nomagno> | It's clear to me now what can and can't be done through the "obvious" interfaces |
| 20:13:33 | <hopelessness[m]> | nomagno: Understanding monads in the context of haskell is essentially understanding them conceptually |
| 20:14:53 | <hopelessness[m]> | what helped me is to instead call monads `flatMappable` or `Chainable` - that's all `>>=` is, a flatmap (flatten . map)` where flatten is an operation `m (m a)) -> m a` |
| 20:15:07 | <hopelessness[m]> | s/flatMappable/FlatMappable/ |
| 20:15:09 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 20:15:39 | <hopelessness[m]> | * what helped me is to instead call monads `FlatMappable` or `Chainable` - that's all `>>=` is, a flatmap `(flatten . map)`, where flatten is an operation `m (m a)) -> m a` |
| 20:16:03 | <hopelessness[m]> | * what helped me is to instead call monads `FlatMappable` or `Chainable` - that's all `>>=` is, a flatmap `(flatten . map)`, where flatten is an operation `Monad m => m (m a) -> m a` |
| 20:16:15 | <nomagno> | You could have `MyCustomMonadType = Just a | Perhaps a`, no? And then you could have the `>>=` implementation ignore the identity laws if it handles a value of the form `Perhaps a` |
| 20:16:41 | <hopelessness[m]> | that should be called MyCustomMaybeType - but yes |
| 20:16:56 | <hopelessness[m]> | you can ignore some laws, those that are not type-enforced |
| 20:17:02 | <hopelessness[m]> | which you should not do |
| 20:17:14 | <nomagno> | I said the identity laws, the first two of the three |
| 20:17:40 | <hopelessness[m]> | those would have to be non-total in the case of Maybe |
| 20:17:41 | <nomagno> | And only when handling Perhaps a, which is NOT unit a, that's Just a in this context |
| 20:18:06 | <hopelessness[m]> | Oh, I didn't read it right |
| 20:18:13 | <ncf> | i don't think there's a lawful monad instance on that type |
| 20:18:29 | <ncf> | (there is if you make it Left a | Right b, which is Either a b) |
| 20:19:09 | → | Angelz joins (Angelz@angelz.oddprotocol.org) |
| 20:19:11 | <hopelessness[m]> | but then the monad is only over one of the type parameters |
| 20:19:31 | <ncf> | yes |
| 20:19:55 | × | comerijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 20:19:57 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 20:20:17 | <nomagno> | Makes enough sense |
| 20:20:49 | <ncf> | hm there are valid monads on that, actually |
| 20:21:02 | <ncf> | your type is isomorphic to (a, Bool), so any monoid on Bool gives you a monad |
| 20:21:34 | <ncf> | i think i was thinking of data Pair a = Pair a a (which i think also has a monad, but it's not obvious) |
| 20:21:35 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 246 seconds) |
| 20:21:47 | <nomagno> | ncf: it is isomorphic to (a, Bool), yes, a was either constructed with one constructor or the other :P |
| 20:21:59 | <nomagno> | m a * |
| 20:22:12 | <hopelessness[m]> | but you can make any type with one type parameter an (unlawful) monad instance, simply with `(>>=) = error ":("` or `(>>=) = (>>=)`; simply making it evaluate to bottom |
| 20:22:27 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 20:23:43 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 20:24:58 | <hopelessness[m]> | * but you can make any type with kind `* -> *` (I hope this is right, im not good with kinds) an (unlawful) monad instance, simply with `(>>=) = error ":("` or `(>>=) = (>>=)`; simply making it evaluate to bottom |
| 20:28:50 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 20:29:07 | → | MajorBiscuit joins (~MajorBisc@31-23-159.netrun.cytanet.com.cy) |
| 20:31:12 | ← | retropikzel parts (9d1a4f9f46@2604:bf00:561:2000::ce) () |
| 20:32:11 | → | retropikzel joins (9d1a4f9f46@2604:bf00:561:2000::ce) |
| 20:36:23 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 20:36:32 | → | freeside joins (~mengwong@68.65.175.90) |
| 20:37:30 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 20:40:57 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 20:44:03 | × | Guest|81 quits (~Guest|81@200.19.106.219) (Quit: Connection closed) |
| 20:45:56 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:53:44 | → | zeenk joins (~zeenk@2a02:2f04:a307:2300::7fe) |
| 20:54:45 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 20:54:45 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 20:54:45 | → | wroathe joins (~wroathe@user/wroathe) |
| 21:01:25 | × | jero98772 quits (~jero98772@190.158.28.80) (Ping timeout: 240 seconds) |
| 21:03:39 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 255 seconds) |
| 21:04:47 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 21:08:06 | × | ix quits (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) (Quit: WeeChat 3.8) |
| 21:09:36 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 21:10:24 | × | ix quits (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) (Client Quit) |
| 21:13:16 | → | gry joins (st@botters/gry) |
| 21:14:01 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::2) |
| 21:20:13 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 21:23:45 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 21:24:44 | × | ix quits (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) (Client Quit) |
| 21:26:10 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 21:27:59 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:32:45 | × | NiceBird quits (~NiceBird@185.133.111.196) (Ping timeout: 240 seconds) |
| 21:35:30 | → | segfaultfizzbuzz joins (~segfaultf@108.211.201.53) |
| 21:41:34 | × | MajorBiscuit quits (~MajorBisc@31-23-159.netrun.cytanet.com.cy) (Quit: WeeChat 3.6) |
| 21:50:42 | → | heraldo joins (~heraldo@user/heraldo) |
| 21:57:10 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:57:36 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 22:01:16 | sm[i]_ | is now known as sm[i] |
| 22:01:17 | × | sm[i] quits (~user@li229-222.members.linode.com) (Changing host) |
| 22:01:17 | → | sm[i] joins (~user@plaintextaccounting/sm) |
| 22:01:52 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 22:08:02 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) (Remote host closed the connection) |
| 22:09:49 | × | vglfr quits (~vglfr@88.155.5.190) (Ping timeout: 265 seconds) |
| 22:11:25 | × | gurkenglas quits (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 22:13:05 | → | gurkenglas joins (~gurkengla@dynamic-046-114-183-221.46.114.pool.telefonica.de) |
| 22:14:09 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 22:16:38 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 22:16:51 | × | mastarija quits (~mastarija@2a05:4f46:e03:6000:a9d6:2c1d:3bed:e943) (Quit: WeeChat 3.7.1) |
| 22:19:35 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c10:cd7b:75b2:cda6) |
| 22:21:52 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 22:25:38 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:27:44 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:33:12 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 22:35:16 | × | hrberg quits (~quassel@171.79-160-161.customer.lyse.net) (Quit: No Ping reply in 180 seconds.) |
| 22:36:57 | × | gurkenglas quits (~gurkengla@dynamic-046-114-183-221.46.114.pool.telefonica.de) (Ping timeout: 250 seconds) |
| 22:38:10 | × | son0p quits (~ff@181.136.122.143) (Read error: Connection reset by peer) |
| 22:39:50 | × | acidjnk quits (~acidjnk@p200300d6e715c435781b7adab6bb3c42.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 22:41:33 | → | hrberg joins (~quassel@171.79-160-161.customer.lyse.net) |
| 22:45:36 | → | son0p joins (~ff@181.136.122.143) |
| 22:47:45 | × | segfaultfizzbuzz quits (~segfaultf@108.211.201.53) (Ping timeout: 240 seconds) |
| 22:52:10 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 22:54:01 | → | dsrt^ joins (~dsrt@c-76-105-96-13.hsd1.ga.comcast.net) |
| 22:55:39 | × | xff0x quits (~xff0x@2405:6580:b080:900:22cb:546d:6546:a19b) (Ping timeout: 260 seconds) |
| 22:56:21 | × | enoq quits (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) (Quit: enoq) |
| 22:57:04 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 22:57:14 | → | xff0x joins (~xff0x@178.255.149.135) |
| 23:01:52 | × | mncheck quits (~mncheck@193.224.205.254) (Ping timeout: 248 seconds) |
| 23:04:09 | → | acidjnk joins (~acidjnk@p200300d6e715c441781b7adab6bb3c42.dip0.t-ipconnect.de) |
| 23:04:25 | → | Guest|83 joins (~Guest|83@181.165.69.16) |
| 23:04:42 | × | xff0x quits (~xff0x@178.255.149.135) (Ping timeout: 255 seconds) |
| 23:05:18 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:06:27 | → | xff0x joins (~xff0x@2405:6580:b080:900:22cb:546d:6546:a19b) |
| 23:10:04 | <Guest|83> | Hi! I tried to put 'ghci' in a terminal but it only gives me error. Do you know how to solve it? |
| 23:13:41 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 23:16:07 | <geekosaur> | how did you install ghc? |
| 23:16:36 | × | acidjnk quits (~acidjnk@p200300d6e715c441781b7adab6bb3c42.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 23:17:00 | → | acidjnk joins (~acidjnk@p200300d6e715c441781b7adab6bb3c42.dip0.t-ipconnect.de) |
| 23:19:28 | <Guest|83> | I intalled visual code and then a haskell extension |
| 23:19:38 | → | mud joins (~mud@user/kadoban) |
| 23:21:09 | <geekosaur> | that is likely to have not updated your `PATH`. look for ~/.ghcup/env |
| 23:21:33 | <geekosaur> | more to the point, do `source ~/.ghcup/env` in your shell |
| 23:22:13 | <geekosaur> | then you'll want to update your shell dotfiles to do that for you; manually installed ghcup will prompt you about it and optionally do it for you, but via vscode it won |
| 23:22:14 | <geekosaur> | 't |
| 23:22:36 | × | acidjnk quits (~acidjnk@p200300d6e715c441781b7adab6bb3c42.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 23:22:58 | <geekosaur> | (if you're on Windows, there's probably something similar but I can't help) |
| 23:23:00 | → | acidjnk joins (~acidjnk@p200300d6e715c441253eea476ad09ae4.dip0.t-ipconnect.de) |
| 23:24:11 | <Guest|83> | I 'm on Windows hahhaha |
| 23:25:01 | <geekosaur> | hm. maerwald? |
| 23:27:35 | <geekosaur> | hm. if he's not around, you could try posting on discourse.haskell.org |
| 23:27:56 | <geekosaur> | (I think it's a bit late for him) |
| 23:31:27 | <Guest|83> | okey, thanks |
| 23:37:43 | → | wavewave joins (~wavewave@135-180-26-28.fiber.dynamic.sonic.net) |
| 23:41:51 | × | wavewave quits (~wavewave@135-180-26-28.fiber.dynamic.sonic.net) (Quit: Client closed) |
| 23:47:43 | → | Axma91218 joins (~Axman6@user/axman6) |
| 23:47:55 | × | pyook quits (~puke@user/puke) (Quit: Quit) |
| 23:49:01 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 23:51:05 | → | pyook joins (~puke@user/puke) |
| 23:54:04 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 23:55:06 | <sm> | hehe of course you are |
| 23:56:16 | × | codaraxis__ quits (~codaraxis@user/codaraxis) (Ping timeout: 248 seconds) |
| 23:56:55 | → | Square2 joins (~Square4@user/square) |
| 23:58:18 | → | pavonia joins (~user@user/siracusa) |
| 23:58:58 | → | mauke_ joins (~mauke@user/mauke) |
| 23:59:18 | <sm> | Guest|83, how about rerunning the standard ghcup installer yourself: https://haskell.org/ghcup |
| 23:59:18 | <sm> | I believe that will be safe, and won't duplicate your haskell installation, but may do a more thorough setup for you, like this PATH setup: https://github.com/haskell/ghcup-hs/blob/master/scripts/bootstrap/bootstrap-haskell.ps1#L91 |
| 23:59:58 | × | Square quits (~Square@user/square) (Ping timeout: 276 seconds) |
All times are in UTC on 2023-04-12.