2022-10-28 00:06:10 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 00:10:22 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
2022-10-28 00:11:03 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
2022-10-28 00:11:13 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
2022-10-28 00:11:46 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
2022-10-28 00:13:13 +0200 | boxscape | (~boxscape@81.191.27.107) (Remote host closed the connection) |
2022-10-28 00:19:54 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
2022-10-28 00:20:33 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 00:23:47 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2022-10-28 00:24:27 +0200 | mncheck | (~mncheck@193.224.205.254) (Ping timeout: 272 seconds) |
2022-10-28 00:30:39 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 00:35:51 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
2022-10-28 00:36:03 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 00:37:57 +0200 | Kaipei | (~Kaiepi@108.175.84.104) (Ping timeout: 240 seconds) |
2022-10-28 00:38:57 +0200 | acidjnk_new | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2022-10-28 00:38:57 +0200 | acidjnk | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2022-10-28 00:40:17 +0200 | dkeohane | (~dkeohane@csm-wl-dhcp-205-230.mines.edu) (Ping timeout: 272 seconds) |
2022-10-28 00:41:12 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-10-28 00:46:04 +0200 | boxscape | (~boxscape@81.191.27.107) |
2022-10-28 00:46:06 +0200 | boxscape | boxscape_ |
2022-10-28 00:49:18 +0200 | jakalx | (~jakalx@base.jakalx.net) |
2022-10-28 00:49:26 +0200 | aaronv | (~aaronv@user/aaronv) |
2022-10-28 00:50:14 +0200 | iteratee | (~kyle@162.218.222.107) |
2022-10-28 00:51:16 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2022-10-28 00:55:05 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: Exeunt juan@acm.org) |
2022-10-28 00:55:17 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-10-28 01:02:03 +0200 | <talismanick> | How do I desugar `\x -> do {foo x; bar}`? |
2022-10-28 01:03:03 +0200 | <jackdk> | @undo \x -> do {foo x; bar} |
2022-10-28 01:03:03 +0200 | <lambdabot> | \ x -> foo x >> bar |
2022-10-28 01:03:07 +0200 | <alexfmpe[m]> | desugar? |
2022-10-28 01:03:54 +0200 | <talismanick> | jackdk: huh, that... was simpler than I thought |
2022-10-28 01:04:11 +0200 | <jackdk> | The rules are in s3.14 of the report: https://www.haskell.org/onlinereport/exps.html |
2022-10-28 01:04:14 +0200 | <davean> | alexfmpe[m]: desugaring is the process of translating the syntax sugar into the base code the sugar represents |
2022-10-28 01:04:34 +0200 | <davean> | talismanick: do notation is VERY simple |
2022-10-28 01:05:08 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
2022-10-28 01:05:08 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
2022-10-28 01:08:04 +0200 | phma | (phma@2001:5b0:211f:9a38:3171:77a0:4a89:d9f6) (Read error: Connection reset by peer) |
2022-10-28 01:08:39 +0200 | phma | (~phma@host-67-44-208-88.hnremote.net) |
2022-10-28 01:08:58 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 01:09:42 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
2022-10-28 01:10:57 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 01:11:44 +0200 | <talismanick> | Might as well ask now... if I have a scoped-typevar lambda, how might I make it pointfree? |
2022-10-28 01:12:16 +0200 | <Axman6> | "scoped-typevar lambda"? |
2022-10-28 01:12:42 +0200 | <talismanick> | \(err :: IOError) -> foo . bar $ show err |
2022-10-28 01:13:19 +0200 | <hpc> | (foo . bar . show :: IOError -> Something Else) -- or something like that |
2022-10-28 01:13:23 +0200 | <Axman6> | foo . bar . show @IOError |
2022-10-28 01:14:13 +0200 | AlexNoo | (~AlexNoo@178.34.162.124) (Read error: Connection reset by peer) |
2022-10-28 01:14:35 +0200 | nibelungen | (~asturias@2001:19f0:7001:638:5400:3ff:fef3:8725) (Quit: ZNC 1.8.2+deb1+focal2 - https://znc.in) |
2022-10-28 01:14:36 +0200 | AlexNoo | (~AlexNoo@178.34.162.124) |
2022-10-28 01:14:44 +0200 | nibelungen | (~asturias@2001:19f0:7001:638:5400:3ff:fef3:8725) |
2022-10-28 01:14:48 +0200 | sa | (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 264 seconds) |
2022-10-28 01:15:27 +0200 | <talismanick> | the former worked |
2022-10-28 01:16:20 +0200 | <alexfmpe[m]> | you can also ask lambdabot for pointfree transformations (in a DM so as not to spam chat) |
2022-10-28 01:16:20 +0200 | <alexfmpe[m]> | example: |
2022-10-28 01:16:28 +0200 | <alexfmpe[m]> | @pl (err :: IOError) -> foo . bar $ show err |
2022-10-28 01:16:29 +0200 | <lambdabot> | (line 1, column 20): |
2022-10-28 01:16:29 +0200 | <lambdabot> | unexpected '>' |
2022-10-28 01:16:29 +0200 | <lambdabot> | expecting operator |
2022-10-28 01:16:41 +0200 | <alexfmpe[m]> | huuuh what |
2022-10-28 01:16:42 +0200 | <talismanick> | The latter complained about "illegal visible application" |
2022-10-28 01:17:06 +0200 | <geekosaur> | "@pl" doesn't understand types in patterns |
2022-10-28 01:17:08 +0200 | <talismanick> | alexfmpe[m]: I'm asking because pointfree doesn't support anything to do with explicit typing or do-notation :) |
2022-10-28 01:17:40 +0200 | <geekosaur> | "@. pl undo" is a thing for the latter, though |
2022-10-28 01:17:40 +0200 | <alexfmpe[m]> | "support anything" ? I'd expect it to be completely independent |
2022-10-28 01:17:49 +0200 | sa | (sid1055@id-1055.tinside.irccloud.com) |
2022-10-28 01:17:52 +0200 | <geekosaur> | it still has to be able to parse it |
2022-10-28 01:17:53 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) (Quit: Leaving.) |
2022-10-28 01:18:04 +0200 | <geekosaur> | it's not using ghc for that parse |
2022-10-28 01:18:17 +0200 | <geekosaur> | it's a simple substitution engine |
2022-10-28 01:18:39 +0200 | redmp | (~redmp@mobile-166-170-43-64.mycingular.net) |
2022-10-28 01:19:07 +0200 | polo | (~polo@user/polo) |
2022-10-28 01:19:26 +0200 | <hpc> | @pl \case of example -> example |
2022-10-28 01:19:26 +0200 | <lambdabot> | const (const id) |
2022-10-28 01:19:27 +0200 | <alexfmpe[m]> | talismanick: `z = foo . bar . show @IOError` worked for me just fine with {-# LANGUAGE TypeApplications #-} |
2022-10-28 01:19:51 +0200 | <talismanick> | so... many... extensions |
2022-10-28 01:20:06 +0200 | <hpc> | er, that wasn't quite right, but in any event that's an example of something that should have been completely different |
2022-10-28 01:21:12 +0200 | <alexfmpe[m]> | you usually only need that one to disambiguate, which is likely not the case for you if the other version worked |
2022-10-28 01:21:44 +0200 | <alexfmpe[m]> | but imagine if you had something like |
2022-10-28 01:21:44 +0200 | <alexfmpe[m]> | show . parse |
2022-10-28 01:22:07 +0200 | <alexfmpe[m]> | that'd work for any Show a, so the type needs to be provided somehow |
2022-10-28 01:23:36 +0200 | <alexfmpe[m]> | er, show . read |
2022-10-28 01:24:11 +0200 | <Axman6> | IMO Type Applications should be enabled by default, they're just so useful |
2022-10-28 01:25:53 +0200 | redmp | (~redmp@mobile-166-170-43-64.mycingular.net) (Ping timeout: 272 seconds) |
2022-10-28 01:26:49 +0200 | <yushyin> | Axman6: they are for GHC2021, https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/control.html#extension-GHC2021 |
2022-10-28 01:27:07 +0200 | <Axman6> | Success! |
2022-10-28 01:28:50 +0200 | darkstardevx | (~darkstard@50.126.124.156) (Remote host closed the connection) |
2022-10-28 01:29:50 +0200 | <hpc> | that's only 4 billion seconds from now! |
2022-10-28 01:30:58 +0200 | <hpc> | hmm, why only GADTSyntax and not GADTs? |
2022-10-28 01:31:17 +0200 | darkstardevx | (~darkstard@50.126.124.156) |
2022-10-28 01:31:35 +0200 | <dolio> | GADTs entails other things that might not be desirable by default. |
2022-10-28 01:31:44 +0200 | <dolio> | As I recall. |
2022-10-28 01:31:54 +0200 | <hpc> | ah, i suppose |
2022-10-28 01:35:50 +0200 | darkstardevx | (~darkstard@50.126.124.156) (Max SendQ exceeded) |
2022-10-28 01:37:23 +0200 | <geekosaur> | RankNTypes which kinda kills type inference |
2022-10-28 01:38:57 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 01:39:42 +0200 | <hpc> | lol that would do it |
2022-10-28 01:40:38 +0200 | <hpc> | hmm, GADTs doesn't imply RankNTypes though? https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/gadt.html seems perfectly fine to me |
2022-10-28 01:41:23 +0200 | <hpc> | maybe it's MonoLocalBinds though |
2022-10-28 01:41:41 +0200 | <hpc> | i haven't had any issues with it, but i can see someone getting annoyed by it |
2022-10-28 01:41:47 +0200 | <geekosaur> | whoops, I meant existential quantification, not rankntyoes |
2022-10-28 01:42:05 +0200 | <geekosaur> | s/tyoes/types/ |
2022-10-28 01:43:11 +0200 | <geekosaur> | I seem to be making a bunch of dumb mistakes today 😞 |
2022-10-28 01:43:14 +0200 | <hpc> | ExistentialQuantification is in ghc2021 :P |
2022-10-28 01:43:25 +0200 | <hpc> | geekosaur: honestly, i am just relieved it's not me this time :D |
2022-10-28 01:43:29 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 244 seconds) |
2022-10-28 01:43:55 +0200 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-10-28 01:48:02 +0200 | <monochrom> | GADTs implies MonoLocalBinds because it's noticed that GADTs doesn't play well with let-polymorphism. |
2022-10-28 01:50:37 +0200 | darkstardevx | (~darkstard@50.126.124.156) |
2022-10-28 01:52:29 +0200 | darkstardevx | (~darkstard@50.126.124.156) (Max SendQ exceeded) |
2022-10-28 01:53:20 +0200 | darkstardevx | (~darkstard@50.126.124.156) |
2022-10-28 01:55:45 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 01:58:40 +0200 | chomwitt | (~chomwitt@2a02:587:dc10:8200:1ac0:4dff:fedb:a3f1) (Ping timeout: 255 seconds) |
2022-10-28 02:00:40 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2022-10-28 02:01:58 +0200 | nilradical | (~nilradica@user/naso) |
2022-10-28 02:02:41 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2022-10-28 02:02:50 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 02:03:02 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2022-10-28 02:03:07 +0200 | ubert1 | (~Thunderbi@178.165.186.249.wireless.dyn.drei.com) |
2022-10-28 02:03:27 +0200 | ubert | (~Thunderbi@178.165.169.91.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
2022-10-28 02:03:27 +0200 | ubert1 | ubert |
2022-10-28 02:03:54 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
2022-10-28 02:05:16 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 02:05:39 +0200 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
2022-10-28 02:06:25 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
2022-10-28 02:06:38 +0200 | polo | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-10-28 02:06:44 +0200 | <EvanR> | one of the monad laws is μ∘Tμ = μ∘μT where wikipedia says the thing to the right is horizontal composition of natural transformations. But T is a functor. So does it mean upgrade T to a natural transformation in the dumbest most obvious way first? |
2022-10-28 02:07:03 +0200 | ft | (~ft@p3e9bc845.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2022-10-28 02:08:09 +0200 | ft | (~ft@p508dbd59.dip0.t-ipconnect.de) |
2022-10-28 02:11:31 +0200 | polo | (~polo@user/polo) |
2022-10-28 02:11:54 +0200 | redmp | (~redmp@mobile-166-170-43-64.mycingular.net) |
2022-10-28 02:12:03 +0200 | <monochrom> | No. Instead, μT is shorthand for μ :: T a -> T (T a). It is a natural transformation from T to Compose T T. |
2022-10-28 02:12:54 +0200 | <monochrom> | Wait, is μ retunr? is μ join? |
2022-10-28 02:12:58 +0200 | <EvanR> | join |
2022-10-28 02:13:10 +0200 | <monochrom> | Ah OK, I need a correction then. |
2022-10-28 02:13:20 +0200 | <geekosaur> | looked more like a comonad to me… |
2022-10-28 02:14:08 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
2022-10-28 02:14:15 +0200 | <monochrom> | μT is shorthand for μ :: T (T (T a)) -> T (T a). It is a natural transformation from TTT to TT. |
2022-10-28 02:14:28 +0200 | <EvanR> | (either way I'm annoyed that the article is trying to pass this off as something else) |
2022-10-28 02:14:31 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
2022-10-28 02:14:41 +0200 | <dolio> | But which one? |
2022-10-28 02:14:58 +0200 | <dolio> | The answer is, the one that isn't Tμ. |
2022-10-28 02:15:20 +0200 | <monochrom> | heh yeah |
2022-10-28 02:16:17 +0200 | <monochrom> | In Haskell you would write "join . fmap join = join . join", but this could be annoying in not explicating which join acts on which type, in particular how many T's. |
2022-10-28 02:17:12 +0200 | <monochrom> | The mathematicians' favourite notation can be derived this way. |
2022-10-28 02:17:14 +0200 | <EvanR> | nice use of overloading of μ there |
2022-10-28 02:17:21 +0200 | <EvanR> | I am quite confused |
2022-10-28 02:18:11 +0200 | <monochrom> | First we agree that mathematicians have a notation equivalent to Haskell's type application. The two are not very different, so I'll write in the Haskell notation. |
2022-10-28 02:18:46 +0200 | <monochrom> | Given for example reverse :: [a] -> [a], we can write "reverse @ Int" for the [Int]->[Int] version. |
2022-10-28 02:19:42 +0200 | <EvanR> | is horizontal composition going to be in at any point xD |
2022-10-28 02:20:02 +0200 | <EvanR> | or is that a red herring |
2022-10-28 02:20:39 +0200 | slack4673 | (~slack1256@191.125.99.208) |
2022-10-28 02:22:25 +0200 | <jackdk> | Lens question: I have `list :: [A]`, `p :: Prism' A B` and `f :: B -> m C` for some monad `m`. I want to construct an `m [C]` that is built up by applying `f` to every `B` in `list` that can be found with `p`. The best I have is to `traverse f $ list ^.. folded . p`, but is there something better that I'm missing? |
2022-10-28 02:22:31 +0200 | <EvanR> | ok natural transformations produce morphisms for each type, so I think I see where you're doing with that |
2022-10-28 02:22:49 +0200 | <monochrom> | With this, the monad law can be written μ . (T . μ) = μ . (μ @ T a), to just explicate the type instantiation of one of the μ's. |
2022-10-28 02:23:15 +0200 | <EvanR> | you just composed a functor with a natural transformation... |
2022-10-28 02:23:31 +0200 | slack1256 | (~slack1256@186.11.17.82) (Ping timeout: 272 seconds) |
2022-10-28 02:24:03 +0200 | <monochrom> | Actually μ . T . (μ @ a) = μ . (μ @ T a) so both sides end with some kind of @ to make my next sentence go nicer. |
2022-10-28 02:24:25 +0200 | <dolio> | Category theorists use the functor's name for its map operation. |
2022-10-28 02:24:46 +0200 | <geekosaur> | remember the Haskell version was `fmap ...` |
2022-10-28 02:24:48 +0200 | <EvanR> | yeah I get that, but functors map morphisms not N.T.s |
2022-10-28 02:24:53 +0200 | <monochrom> | Then we "eta-reduce" away the "a" on both sides. At this points mathematicians also notice that they can conflate "." with "@" with no loss of ambiguity. |
2022-10-28 02:25:07 +0200 | <dolio> | Also, I think μT is equivalent to horizontal composition with the identity transformation from T to T. |
2022-10-28 02:25:16 +0200 | <geekosaur> | "loss of ambiguity"? |
2022-10-28 02:25:24 +0200 | <EvanR> | hence the "dumbest most obvious way" |
2022-10-28 02:25:53 +0200 | <monochrom> | With "." and "@" unified, they replace both by juxtaposition, thus μ . Tμ = μ . μT |
2022-10-28 02:26:01 +0200 | <EvanR> | oh, monochrom is using haskell, right |
2022-10-28 02:26:05 +0200 | <monochrom> | Err loss of unambiguity! Heh. |
2022-10-28 02:26:25 +0200 | <monochrom> | I was starting with Haskell then showed the transition to math notation. |
2022-10-28 02:26:56 +0200 | <monochrom> | Lastly, horizontal composition of natural transformation is just Haskell composition of polymorphic functions. |
2022-10-28 02:27:25 +0200 | <monochrom> | If you have "reverse . reverse" it's a horizontal composition of natural transformations. |
2022-10-28 02:27:35 +0200 | <dolio> | No, that one's vertical. |
2022-10-28 02:28:20 +0200 | <monochrom> | OK I had a typo. That ruined everything didn't it? |
2022-10-28 02:28:24 +0200 | <dolio> | Horizontal is where you compose α with fmap β, and it doesn't matter which order. |
2022-10-28 02:28:38 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 02:28:50 +0200 | <monochrom> | μ . (T μ) = μ . (μ @ T a) is the right starting point. |
2022-10-28 02:30:10 +0200 | <monochrom> | It is also μ . (T (μ @ a)) = μ . (μ @ T a) |
2022-10-28 02:30:47 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 02:31:09 +0200 | <EvanR> | the thing is, μ is something already, and it's not polymorphic, so what are you doing |
2022-10-28 02:31:49 +0200 | hueso | (~root@user/hueso) (Quit: No Ping reply in 180 seconds.) |
2022-10-28 02:31:59 +0200 | <EvanR> | when reading the "math version" what does your polymorphism correspond to |
2022-10-28 02:32:29 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 02:32:38 +0200 | <monochrom> | I don't understand those questions and I don't know how to answer them. |
2022-10-28 02:32:42 +0200 | <EvanR> | μ : T² -> T |
2022-10-28 02:32:49 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 02:33:06 +0200 | <EvanR> | T : C -> C |
2022-10-28 02:33:09 +0200 | hueso | (~root@user/hueso) |
2022-10-28 02:33:28 +0200 | Batzy_ | Batzy |
2022-10-28 02:33:28 +0200 | <EvanR> | so wtf is μT and Tμ xD |
2022-10-28 02:33:59 +0200 | <dolio> | Natural transformations are families of arrows that commute with arrows. |
2022-10-28 02:34:01 +0200 | <geekosaur> | are you missing that Haskell's Monad is specialized to Hask (to the extent that it's a category) but CT monads aren't? |
2022-10-28 02:34:12 +0200 | mmhat | (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.7.1) |
2022-10-28 02:34:15 +0200 | <EvanR> | (dolio says it's horizontal composition after upgrading T to a N.T., which is what I guessed originally) |
2022-10-28 02:34:20 +0200 | <monochrom> | Tμ is fmap μ. μT is μ @ T a then eta away the "a". |
2022-10-28 02:34:21 +0200 | <dolio> | Polymorphic definitions are families of arrows that commute with relations. |
2022-10-28 02:35:26 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2022-10-28 02:35:26 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2022-10-28 02:35:26 +0200 | wroathe | (~wroathe@user/wroathe) |
2022-10-28 02:35:41 +0200 | mtjm | (~mutantmel@2604:a880:2:d0::208b:d001) (Remote host closed the connection) |
2022-10-28 02:36:11 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 244 seconds) |
2022-10-28 02:36:27 +0200 | <EvanR> | geekosaur, no but now I'm wondering what difference that makes, which I'll have to come back to |
2022-10-28 02:36:54 +0200 | mtjm | (~mutantmel@2604:a880:2:d0::208b:d001) |
2022-10-28 02:37:01 +0200 | <geekosaur> | I'm probably confused, but in CT terms the Haskell one isn't polymorphic |
2022-10-28 02:37:05 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
2022-10-28 02:37:13 +0200 | <geekosaur> | I think |
2022-10-28 02:37:30 +0200 | <monochrom> | Sure. But if you s/polymorphic/natural tranformation/ then you get the CT one. |
2022-10-28 02:37:36 +0200 | <geekosaur> | that said, when you wrote "μ : T² -> T", that looks to me polymorphic in T |
2022-10-28 02:37:37 +0200 | caryhartline | (~caryhartl@107.140.218.181) (Quit: caryhartline) |
2022-10-28 02:38:12 +0200 | <geekosaur> | unless the uppercase means a specific type/NT? |
2022-10-28 02:38:32 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 02:38:55 +0200 | <EvanR> | T is a constant xD |
2022-10-28 02:38:56 +0200 | <monochrom> | No. Instead, where Haskell writes "foo :: F a -> G a", CT writes "foo :: F => G". Then you find yourself going out of your way to write pointfree at the type level. |
2022-10-28 02:39:12 +0200 | <EvanR> | (functor) |
2022-10-28 02:39:13 +0200 | <monochrom> | T is the functor being declared as a monad. |
2022-10-28 02:39:41 +0200 | <geekosaur> | oh, but we're talking about join so the inner Functor must be the same as the outer? |
2022-10-28 02:40:40 +0200 | <EvanR> | monads are endofunctors so were only dealing in 1 category at a time |
2022-10-28 02:40:41 +0200 | <monochrom> | With join you have "T (T a) -> T a" but remember you have to write it pointfree i.e. without "a" so now you have to invent some kind of T². |
2022-10-28 02:41:15 +0200 | <EvanR> | yeah T . T |
2022-10-28 02:43:25 +0200 | jargon | (~jargon@184.101.208.112) |
2022-10-28 02:44:14 +0200 | <EvanR> | you're saying Tμ is fmap join, while T is defined to map morphisms in C, rather than natural transformations or the associated map that takes objects... |
2022-10-28 02:45:03 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 02:45:06 +0200 | <monochrom> | "T" is fmap, more precisely fmap@T, when used in the context of "T <morphism here>" |
2022-10-28 02:45:33 +0200 | <EvanR> | I get that fmap is involved, I'll do some more noodling with the definition of horizontal composition, and hopefully jackdk gets their lens question answered |
2022-10-28 02:45:41 +0200 | <monochrom> | Yes, whereas Haskell writes "fmap @ Maybe", math writes "Maybe". |
2022-10-28 02:47:49 +0200 | <monochrom> | μ is a natural transformation therefore is instantiatable to a morphism, in particular in this context μ@a. |
2022-10-28 02:47:49 +0200 | <EvanR> | maybe the missing link here is how you're going from μ the N.T. to a morphism join in the category |
2022-10-28 02:48:04 +0200 | <EvanR> | ooooh |
2022-10-28 02:48:13 +0200 | <EvanR> | that's the instantiation step |
2022-10-28 02:48:31 +0200 | Midjak | (~Midjak@82.66.147.146) |
2022-10-28 02:48:50 +0200 | <monochrom> | The whole equation begins as (μ @ a) . (T (μ @ a)) = (μ @ a) . (μ @ T a) |
2022-10-28 02:49:22 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 250 seconds) |
2022-10-28 02:50:07 +0200 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2022-10-28 02:51:04 +0200 | <EvanR> | so Tμ involves fmap and μT doesn't |
2022-10-28 02:51:05 +0200 | <monochrom> | I have given a not-so-good explanation of how to get to the usual math notation. Many CT books have good explanations. |
2022-10-28 02:51:53 +0200 | <EvanR> | in any case this text "here Tμ and μT are formed by 'horizontal composition'" didn't immediately explain it |
2022-10-28 02:51:56 +0200 | <monochrom> | Emily Riehl's has one. I think Fokkingga's "gentle introduction to category theory" has one too. |
2022-10-28 02:52:08 +0200 | <monochrom> | To be honest I hate this math notation though. |
2022-10-28 02:52:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-10-28 02:52:29 +0200 | <monochrom> | Well yeah one has to learn "horizontal composition" first. |
2022-10-28 02:53:00 +0200 | <EvanR> | well that's what I was doing, and on THAT page, it says it's an operation between two natural transformations and doesn't seem to explain the functor notation |
2022-10-28 02:54:07 +0200 | <EvanR> | but now I gather it's like a functor preprocessor or postprocessor or something |
2022-10-28 02:55:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 02:56:07 +0200 | <EvanR> | though in 1 of the 2 you didn't use fmap... |
2022-10-28 02:56:38 +0200 | <monochrom> | Right. |
2022-10-28 02:57:24 +0200 | <monochrom> | μT really comes from (μ @ T a) then dropping the a and the @ |
2022-10-28 02:57:51 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2022-10-28 02:58:10 +0200 | <monochrom> | In actual math notation it's μ<sub>T a</sub> then dropping the a and promoting the T from subscript to normal text. |
2022-10-28 02:58:17 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-10-28 02:59:38 +0200 | <monochrom> | In Haskell it's "join . join = join . fmap join" so fmap happens on one side only. |
2022-10-28 02:59:45 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
2022-10-28 02:59:48 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
2022-10-28 03:00:09 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 03:00:32 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
2022-10-28 03:01:26 +0200 | <monochrom> | You should also try to independently imagine how to write code for the type sig "T (T (T a)) -> T a", you will find two ways, and they are the two sides of the law. |
2022-10-28 03:02:15 +0200 | <EvanR> | and in a monad, the two ways are equivalent? |
2022-10-28 03:02:33 +0200 | <monochrom> | Yeah the monad law says we want them to do the same thing. |
2022-10-28 03:02:49 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 03:04:12 +0200 | cytokine_storm | (~cytokine_@user/cytokine-storm/x-1083107) |
2022-10-28 03:04:42 +0200 | crns | (~netcrns@user/crns) (Ping timeout: 260 seconds) |
2022-10-28 03:05:44 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 03:06:05 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2022-10-28 03:06:09 +0200 | crns | (~netcrns@p5dc33bf3.dip0.t-ipconnect.de) |
2022-10-28 03:06:09 +0200 | crns | (~netcrns@p5dc33bf3.dip0.t-ipconnect.de) (Changing host) |
2022-10-28 03:06:09 +0200 | crns | (~netcrns@user/crns) |
2022-10-28 03:06:39 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 03:07:11 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 244 seconds) |
2022-10-28 03:07:17 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
2022-10-28 03:07:36 +0200 | <EvanR> | alright wikipedia calls Fμ and μF whiskering, there it is explained |
2022-10-28 03:08:05 +0200 | codedmart | (codedmart@2600:3c01::f03c:92ff:fefe:8511) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
2022-10-28 03:08:20 +0200 | codedmart | (codedmart@2600:3c01::f03c:92ff:fefe:8511) |
2022-10-28 03:08:26 +0200 | <monochrom> | Yeah. I should have mentioned that name. I wasn't confident; I only saw it once (in Riehl's), wasn't sure it's the common name. |
2022-10-28 03:08:42 +0200 | <monochrom> | (Then again I didn't read many CT books. Just maybe 3.) |
2022-10-28 03:09:27 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
2022-10-28 03:09:59 +0200 | <EvanR> | I already knew this notation and what it meant, forget it, but never heard of whiskering before |
2022-10-28 03:10:04 +0200 | <EvanR> | forgot* |
2022-10-28 03:10:06 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 03:10:36 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
2022-10-28 03:12:33 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Quit: Lost terminal) |
2022-10-28 03:13:09 +0200 | <EvanR> | why do I care, well I was trying to follow this blog post which says 1. a monoid is a special case of a category 2. a category is special case of a monad and 3. a monad is a special case of a monoid |
2022-10-28 03:13:17 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 03:13:29 +0200 | <EvanR> | so I got stuck making sure I knew what a monad is before he goes off the deep end making a category a monad |
2022-10-28 03:14:07 +0200 | <EvanR> | https://graphicallinearalgebra.net/2017/04/16/a-monoid-is-a-category-a-category-is-a-monad-a-monad… |
2022-10-28 03:15:37 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 03:16:43 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
2022-10-28 03:18:04 +0200 | polo_ | (~polo@user/polo) |
2022-10-28 03:18:28 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 03:20:31 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
2022-10-28 03:20:44 +0200 | polo | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-10-28 03:22:07 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 03:23:20 +0200 | polo_ | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-10-28 03:25:24 +0200 | cytokine_storm | (~cytokine_@user/cytokine-storm/x-1083107) (Quit: Quit) |
2022-10-28 03:26:13 +0200 | Natch | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 272 seconds) |
2022-10-28 03:26:56 +0200 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
2022-10-28 03:27:18 +0200 | xff0x | (~xff0x@2405:6580:b080:900:4ce0:8375:d2a4:aff0) (Ping timeout: 255 seconds) |
2022-10-28 03:28:05 +0200 | zaquest | (~notzaques@5.130.79.72) |
2022-10-28 03:29:23 +0200 | Natch | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
2022-10-28 03:30:26 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 244 seconds) |
2022-10-28 03:32:42 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
2022-10-28 03:33:59 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
2022-10-28 03:39:13 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
2022-10-28 03:39:38 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 250 seconds) |
2022-10-28 03:40:50 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
2022-10-28 03:42:49 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
2022-10-28 03:43:26 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-10-28 03:45:57 +0200 | boxscape | (~boxscape@81.191.27.107) |
2022-10-28 03:46:02 +0200 | boxscape | boxscape_1 |
2022-10-28 03:47:24 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 03:48:25 +0200 | nilradical | (~nilradica@user/naso) () |
2022-10-28 03:49:22 +0200 | boxscape_ | (~boxscape@81.191.27.107) (Ping timeout: 244 seconds) |
2022-10-28 03:50:04 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 03:51:25 +0200 | jargon | (~jargon@184.101.208.112) (Remote host closed the connection) |
2022-10-28 03:55:13 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Ping timeout: 246 seconds) |
2022-10-28 03:55:26 +0200 | gqplox | (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
2022-10-28 03:55:52 +0200 | Kaipei | (~Kaiepi@108.175.84.104) |
2022-10-28 03:56:04 +0200 | gqplox | (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) |
2022-10-28 03:58:09 +0200 | nisstyre | (~wes@li798-187.members.linode.com) (Changing host) |
2022-10-28 03:58:09 +0200 | nisstyre | (~wes@user/nisstyre) |
2022-10-28 04:01:12 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 04:07:10 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
2022-10-28 04:08:51 +0200 | td_ | (~td@83.135.9.51) (Ping timeout: 260 seconds) |
2022-10-28 04:09:10 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-10-28 04:10:20 +0200 | td_ | (~td@83.135.9.42) |
2022-10-28 04:13:25 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
2022-10-28 04:16:25 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
2022-10-28 04:16:39 +0200 | polo | (~polo@user/polo) |
2022-10-28 04:17:00 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 04:18:47 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 04:25:17 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 240 seconds) |
2022-10-28 04:26:34 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 04:28:58 +0200 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-10-28 04:30:29 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 04:31:27 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2022-10-28 04:36:12 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
2022-10-28 04:36:30 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 04:36:33 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 04:37:28 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 04:38:59 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 04:43:13 +0200 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
2022-10-28 04:44:07 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
2022-10-28 04:44:32 +0200 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) |
2022-10-28 04:45:18 +0200 | mzan | (~quassel@mail.asterisell.com) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
2022-10-28 04:46:19 +0200 | mzan | (~quassel@mail.asterisell.com) |
2022-10-28 04:46:47 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
2022-10-28 04:46:50 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
2022-10-28 04:48:58 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 246 seconds) |
2022-10-28 04:49:23 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
2022-10-28 04:49:33 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 04:51:23 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 04:52:26 +0200 | polo | (~polo@user/polo) |
2022-10-28 04:52:27 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-10-28 04:53:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 04:53:45 +0200 | <talismanick> | Is there a built-in function (context: using RIO) which is like `either` but auto-returns "mempty" on Right? |
2022-10-28 04:54:25 +0200 | <talismanick> | something like `\handleErr -> either handleErr mempty` |
2022-10-28 04:55:58 +0200 | <talismanick> | I wrote "flip either mempty <handle Left error case>" and now hlint won't shut up about "redundant flip" |
2022-10-28 04:58:03 +0200 | iteratee | (~kyle@162.218.222.107) (Ping timeout: 272 seconds) |
2022-10-28 04:59:30 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 05:00:36 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 05:01:39 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds) |
2022-10-28 05:03:35 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 05:03:42 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
2022-10-28 05:08:19 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2022-10-28 05:09:26 +0200 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-10-28 05:10:38 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2022-10-28 05:10:49 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Remote host closed the connection) |
2022-10-28 05:11:08 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-10-28 05:11:37 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
2022-10-28 05:12:09 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-10-28 05:12:37 +0200 | polo | (~polo@user/polo) |
2022-10-28 05:13:46 +0200 | vglfr | (~vglfr@145.224.100.164) (Ping timeout: 244 seconds) |
2022-10-28 05:16:18 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 252 seconds) |
2022-10-28 05:17:36 +0200 | rembo10 | (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-10-28 05:20:06 +0200 | cyphase | (~cyphase@user/cyphase) |
2022-10-28 05:20:10 +0200 | rembo10 | (~rembo10@main.remulis.com) |
2022-10-28 05:21:02 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 250 seconds) |
2022-10-28 05:23:09 +0200 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-10-28 05:23:24 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2022-10-28 05:23:24 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2022-10-28 05:23:24 +0200 | wroathe | (~wroathe@user/wroathe) |
2022-10-28 05:24:11 +0200 | AlexNoo | (~AlexNoo@178.34.162.124) (Read error: Connection reset by peer) |
2022-10-28 05:24:12 +0200 | polo | (~polo@user/polo) |
2022-10-28 05:24:34 +0200 | AlexNoo | (~AlexNoo@178.34.162.124) |
2022-10-28 05:28:50 +0200 | polo | (~polo@user/polo) (Client Quit) |
2022-10-28 05:29:24 +0200 | polo | (~polo@user/polo) |
2022-10-28 05:33:26 +0200 | slack4673 | (~slack1256@191.125.99.208) (Read error: Connection reset by peer) |
2022-10-28 05:34:38 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 252 seconds) |
2022-10-28 05:36:30 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
2022-10-28 05:38:30 +0200 | boxscape_1 | (~boxscape@81.191.27.107) (Remote host closed the connection) |
2022-10-28 05:44:37 +0200 | Vajb | (~Vajb@2001:999:504:1841:9e47:1ec7:a52e:1d57) (Read error: Connection reset by peer) |
2022-10-28 05:44:49 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) |
2022-10-28 05:47:18 +0200 | causal | (~user@50.35.83.177) |
2022-10-28 05:49:36 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
2022-10-28 05:53:57 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 240 seconds) |
2022-10-28 05:54:33 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 258 seconds) |
2022-10-28 05:57:39 +0200 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-10-28 06:00:25 +0200 | polo | (~polo@user/polo) |
2022-10-28 06:03:13 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
2022-10-28 06:11:52 +0200 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-10-28 06:12:15 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
2022-10-28 06:14:42 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 255 seconds) |
2022-10-28 06:17:47 +0200 | arahael | (~arahael@14-202-55-135.tpgi.com.au) (Ping timeout: 260 seconds) |
2022-10-28 06:18:16 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Quit: ZNC - https://znc.in) |
2022-10-28 06:20:29 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 06:22:07 +0200 | mbuf | (~Shakthi@49.204.132.19) |
2022-10-28 06:22:42 +0200 | k8yun | (~k8yun@user/k8yun) |
2022-10-28 06:25:55 +0200 | gqplox | (~textual@2a02:c7c:941d:fd00:4102:e413:2c06:9bc1) (Quit: Textual IRC Client: www.textualapp.com) |
2022-10-28 06:30:48 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
2022-10-28 06:31:01 +0200 | arahael | (~arahael@14-200-56-241.tpgi.com.au) |
2022-10-28 06:31:09 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) (Read error: Connection reset by peer) |
2022-10-28 06:31:23 +0200 | Vajb | (~Vajb@85-76-71-213-nat.elisa-mobile.fi) |
2022-10-28 06:33:18 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 06:33:58 +0200 | k8yun | (~k8yun@user/k8yun) (Quit: Leaving) |
2022-10-28 06:35:39 +0200 | jonathanx | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2022-10-28 06:37:16 +0200 | jonathanx_ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2022-10-28 06:39:43 +0200 | bgs | (~bgs@212-85-160-171.dynamic.telemach.net) |
2022-10-28 06:40:20 +0200 | jonathanx | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 250 seconds) |
2022-10-28 06:40:26 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 06:44:37 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Ping timeout: 240 seconds) |
2022-10-28 06:45:55 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
2022-10-28 06:56:33 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 06:59:50 +0200 | raym | (~ray@user/raym) (Ping timeout: 250 seconds) |
2022-10-28 07:01:21 +0200 | tjakway | (~tjakway@184.170.241.65) |
2022-10-28 07:07:53 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
2022-10-28 07:11:56 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 07:13:10 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 07:14:00 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2022-10-28 07:14:00 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2022-10-28 07:14:00 +0200 | wroathe | (~wroathe@user/wroathe) |
2022-10-28 07:15:55 +0200 | tjakway | (~tjakway@184.170.241.65) (Quit: WeeChat 3.5) |
2022-10-28 07:17:43 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Ping timeout: 255 seconds) |
2022-10-28 07:18:45 +0200 | tjakway | (~tjakway@cpe-107-184-74-161.socal.res.rr.com) |
2022-10-28 07:27:41 +0200 | bgs | (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
2022-10-28 07:28:29 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
2022-10-28 07:28:45 +0200 | polo | (~polo@user/polo) |
2022-10-28 07:29:54 +0200 | polo | (~polo@user/polo) (Client Quit) |
2022-10-28 07:36:11 +0200 | tomku | (~tomku@user/tomku) (Ping timeout: 276 seconds) |
2022-10-28 07:36:46 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 07:40:40 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2022-10-28 07:42:02 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2022-10-28 07:43:16 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
2022-10-28 07:44:22 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
2022-10-28 07:46:31 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 272 seconds) |
2022-10-28 07:47:01 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-10-28 07:54:23 +0200 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Quit: quit) |
2022-10-28 07:54:31 +0200 | nshepperd | (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) |
2022-10-28 07:56:55 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
2022-10-28 07:57:34 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 07:58:30 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
2022-10-28 08:00:57 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-10-28 08:01:19 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Client Quit) |
2022-10-28 08:02:22 +0200 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
2022-10-28 08:02:40 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 250 seconds) |
2022-10-28 08:21:43 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
2022-10-28 08:21:49 +0200 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
2022-10-28 08:27:06 +0200 | mixfix41 | (~sdenynine@user/mixfix41) |
2022-10-28 08:27:48 +0200 | detuneattune | (~detuneatt@user/detuneattune) (Quit: The Lounge - https://thelounge.chat) |
2022-10-28 08:28:04 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 246 seconds) |
2022-10-28 08:28:50 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-10-28 08:29:07 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 08:32:08 +0200 | mixfix41 | (~sdenynine@user/mixfix41) (Ping timeout: 250 seconds) |
2022-10-28 08:33:03 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 08:33:26 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
2022-10-28 08:35:13 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
2022-10-28 08:35:33 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-10-28 08:35:45 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-10-28 08:37:46 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
2022-10-28 08:41:25 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2022-10-28 08:42:06 +0200 | detuneattune | (~detuneatt@user/detuneattune) |
2022-10-28 08:43:08 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2022-10-28 08:43:10 +0200 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
2022-10-28 08:43:19 +0200 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
2022-10-28 08:45:37 +0200 | mixfix41 | (~sdenynine@user/mixfix41) |
2022-10-28 08:48:01 +0200 | raym | (~ray@user/raym) |
2022-10-28 08:52:14 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 276 seconds) |
2022-10-28 08:52:27 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 08:52:59 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 08:55:57 +0200 | echoreply | (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
2022-10-28 08:57:14 +0200 | echoreply | (~echoreply@45.32.163.16) |
2022-10-28 08:57:16 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
2022-10-28 09:01:48 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:e14a:54e1:f555:fbc8) |
2022-10-28 09:04:55 +0200 | michalz | (~michalz@185.246.207.200) |
2022-10-28 09:06:14 +0200 | danza | (~francesco@151.82.113.246) |
2022-10-28 09:06:48 +0200 | gmg | (~user@user/gehmehgeh) |
2022-10-28 09:12:11 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
2022-10-28 09:13:07 +0200 | acidjnk_new | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
2022-10-28 09:13:07 +0200 | acidjnk | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
2022-10-28 09:15:34 +0200 | m5zs7k | (aquares@web10.mydevil.net) (Ping timeout: 244 seconds) |
2022-10-28 09:16:32 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2022-10-28 09:16:38 +0200 | m5zs7k | (aquares@web10.mydevil.net) |
2022-10-28 09:17:22 +0200 | CiaoSen | (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
2022-10-28 09:18:43 +0200 | mncheck | (~mncheck@193.224.205.254) |
2022-10-28 09:20:15 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Ping timeout: 272 seconds) |
2022-10-28 09:22:37 +0200 | mixfix41 | (~sdenynine@user/mixfix41) (Remote host closed the connection) |
2022-10-28 09:25:48 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-10-28 09:25:59 +0200 | ft | (~ft@p508dbd59.dip0.t-ipconnect.de) (Quit: leaving) |
2022-10-28 09:26:14 +0200 | tjakway | (~tjakway@cpe-107-184-74-161.socal.res.rr.com) (Quit: WeeChat 3.5) |
2022-10-28 09:26:41 +0200 | kenran | (~user@user/kenran) |
2022-10-28 09:26:49 +0200 | kenran | (~user@user/kenran) (Remote host closed the connection) |
2022-10-28 09:28:37 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 09:28:58 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
2022-10-28 09:31:06 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 09:31:08 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
2022-10-28 09:31:46 +0200 | mixfix41 | (~sdenynine@user/mixfix41) |
2022-10-28 09:34:44 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 09:36:24 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 09:39:15 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
2022-10-28 09:45:48 +0200 | raym | (~ray@user/raym) (Ping timeout: 250 seconds) |
2022-10-28 09:46:09 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 09:46:21 +0200 | infinity0 | (~infinity0@pwned.gg) (Remote host closed the connection) |
2022-10-28 09:46:26 +0200 | infinity0_ | (~infinity0@pwned.gg) |
2022-10-28 09:46:29 +0200 | infinity0_ | infinity0 |
2022-10-28 09:46:40 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 09:46:40 +0200 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
2022-10-28 09:46:52 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 09:48:07 +0200 | mixfix41 | (~sdenynine@user/mixfix41) (Ping timeout: 272 seconds) |
2022-10-28 09:50:16 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 09:51:32 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2022-10-28 09:52:05 +0200 | fserucas|eod | (~fserucas|@2001:818:e376:a400:fb92:70c1:dd88:c7d7) |
2022-10-28 09:52:36 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 264 seconds) |
2022-10-28 09:56:57 +0200 | redmp | (~redmp@mobile-166-170-43-64.mycingular.net) (Ping timeout: 240 seconds) |
2022-10-28 09:58:09 +0200 | mmhat | (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) |
2022-10-28 10:02:01 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 10:05:19 +0200 | mbuf | (~Shakthi@49.204.132.19) (Quit: Leaving) |
2022-10-28 10:12:15 +0200 | danza | (~francesco@151.82.113.246) (Read error: Connection reset by peer) |
2022-10-28 10:12:28 +0200 | cfricke | (~cfricke@user/cfricke) |
2022-10-28 10:18:10 +0200 | chele | (~chele@user/chele) |
2022-10-28 10:22:40 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
2022-10-28 10:23:35 +0200 | jonathanx_ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 272 seconds) |
2022-10-28 10:24:20 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2022-10-28 10:29:27 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2022-10-28 10:30:05 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 10:30:33 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2022-10-28 10:32:53 +0200 | king_gs1 | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-10-28 10:32:55 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
2022-10-28 10:32:55 +0200 | king_gs1 | king_gs |
2022-10-28 10:33:44 +0200 | shriekingnoise | (~shrieking@186.137.167.202) (Quit: Quit) |
2022-10-28 10:35:37 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 272 seconds) |
2022-10-28 10:38:02 +0200 | chele | (~chele@user/chele) |
2022-10-28 10:43:14 +0200 | erisco_ | (~erisco@d24-141-66-165.home.cgocable.net) |
2022-10-28 10:45:07 +0200 | erisco | (~erisco@d24-141-66-165.home.cgocable.net) (Ping timeout: 272 seconds) |
2022-10-28 10:45:07 +0200 | erisco_ | erisco |
2022-10-28 10:46:02 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 250 seconds) |
2022-10-28 10:47:43 +0200 | Kaipii | (~Kaiepi@108.175.84.104) |
2022-10-28 10:50:45 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 10:51:27 +0200 | Kaipei | (~Kaiepi@108.175.84.104) (Ping timeout: 272 seconds) |
2022-10-28 10:55:08 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 250 seconds) |
2022-10-28 10:57:43 +0200 | __monty__ | (~toonn@user/toonn) |
2022-10-28 11:08:01 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
2022-10-28 11:08:32 +0200 | jonathanx_ | (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
2022-10-28 11:11:59 +0200 | acidjnk | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2022-10-28 11:13:00 +0200 | kenran | (~user@user/kenran) |
2022-10-28 11:13:07 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 11:17:54 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:e14a:54e1:f555:fbc8) (Quit: WeeChat 2.8) |
2022-10-28 11:20:15 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
2022-10-28 11:21:09 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
2022-10-28 11:22:16 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 11:22:36 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
2022-10-28 11:23:49 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2022-10-28 11:27:28 +0200 | Kaipii | Kaiepi |
2022-10-28 11:28:43 +0200 | axeman | (~quassel@212.129.76.63) |
2022-10-28 11:29:27 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2022-10-28 11:31:27 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2022-10-28 11:33:04 +0200 | <probie> | Is there a convenient way to recurse over type-level naturals, or am I stuck defining something like `data N = Z | S N` and `type family ToNat (n :: Nat) :: N where`? |
2022-10-28 11:34:50 +0200 | gmg | (~user@user/gehmehgeh) |
2022-10-28 11:35:12 +0200 | frost24 | (~frost@user/frost) |
2022-10-28 11:35:37 +0200 | <merijn> | There is a convenient way! It's called "writing your code in Idris" :D |
2022-10-28 11:35:42 +0200 | <probie> | I wrote iterated fmap (i.e `fmapn @2 (*2) [[1..4::Int],[2..7]] = [[2,4,6,8],[4,6,8,10,12,14]]`), but to use `Nat` I ended up needing a type like `fmapn :: forall n x y a b . FmapN (ToN n) x y a b => (a -> b) -> x -> y` |
2022-10-28 11:36:27 +0200 | <probie> | s/(*2)/(*2::Int)/ (type inference does not play nicely here) |
2022-10-28 11:38:57 +0200 | <probie> | merijn: and give up my laziness? |
2022-10-28 11:41:09 +0200 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
2022-10-28 11:41:26 +0200 | <tomsmeding> | some of us need to be strict and get some productive work done, once in a while, otherwise nothing would happen ;) |
2022-10-28 11:42:03 +0200 | <merijn> | There's a threshold past which writing type level stuff is more pain than gain, and this seems well past this threshold, unless your name is Oleg :p |
2022-10-28 11:42:59 +0200 | <tomsmeding> | but unless such a way has come into existence in the last two ghc versions or so, there is no way to conveniently recurse over ghc typelevel nats |
2022-10-28 11:43:01 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Read error: Connection reset by peer) |
2022-10-28 11:43:01 +0200 | king_gs1 | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-10-28 11:43:21 +0200 | <tomsmeding> | but iirc there was a package that already had conversions back and forth to an actual inductive natural number type |
2022-10-28 11:45:20 +0200 | king_gs1 | king_gs |
2022-10-28 11:50:30 +0200 | raym | (~ray@user/raym) |
2022-10-28 11:50:50 +0200 | axeman | (~quassel@212.129.76.63) (Ping timeout: 252 seconds) |
2022-10-28 11:51:23 +0200 | axeman | (~quassel@212.129.77.169) |
2022-10-28 11:54:30 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 258 seconds) |
2022-10-28 11:55:52 +0200 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
2022-10-28 11:57:05 +0200 | eaxli | (~eax@user/eaxli) |
2022-10-28 11:58:06 +0200 | eaxli | (~eax@user/eaxli) (Quit: leaving) |
2022-10-28 11:58:09 +0200 | <tomsmeding> | talismanick: hlint not shutting up is easily solved by adding a .hlint.yaml file (if I remember the file name correctly) with some hints to ignore |
2022-10-28 11:58:35 +0200 | <merijn> | I have this one simpel trick for shutting up hlint (Neil Mitchell hates him!) |
2022-10-28 12:04:14 +0200 | <tomsmeding> | settings = { haskell = { plugin = { hlint = { globalOn = false } } } } |
2022-10-28 12:08:10 +0200 | <merijn> | tomsmeding: I was thinking "rm `which hlint`", but sure :p |
2022-10-28 12:08:52 +0200 | <tomsmeding> | merijn: I remember that at some point the path for that HLS setting changed, so I randomly got hlint notices again at some point |
2022-10-28 12:08:53 +0200 | frost24 | (~frost@user/frost) (Quit: Client closed) |
2022-10-28 12:09:07 +0200 | <tomsmeding> | I was like wait what no what changed |
2022-10-28 12:14:23 +0200 | CiaoSen | (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2022-10-28 12:14:57 +0200 | axeman | (~quassel@212.129.77.169) (Ping timeout: 240 seconds) |
2022-10-28 12:15:02 +0200 | <Profpatsch> | newtype RevList a = RevList [a] |
2022-10-28 12:15:04 +0200 | <Profpatsch> | deriving (Semigroup) via (Dual [a]) |
2022-10-28 12:15:07 +0200 | <Profpatsch> | Can I make this work somehow? |
2022-10-28 12:16:43 +0200 | <tomsmeding> | > :set -XDerivingVia -XDerivingStrategies |
2022-10-28 12:16:45 +0200 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
2022-10-28 12:16:52 +0200 | <tomsmeding> | % :set -XDerivingVia -XDerivingStrategies |
2022-10-28 12:16:52 +0200 | <yahb2> | <no output> |
2022-10-28 12:16:54 +0200 | <Profpatsch> | I guess I can add the Dual constructor to the RevList constructor |
2022-10-28 12:16:54 +0200 | <tomsmeding> | % import Data.Monoid |
2022-10-28 12:16:54 +0200 | <yahb2> | <no output> |
2022-10-28 12:17:00 +0200 | <tomsmeding> | % newtype RevList a = RevList [a] deriving (Semigroup) via (Dual [a]) deriving (Show) |
2022-10-28 12:17:00 +0200 | <yahb2> | <no output> |
2022-10-28 12:17:05 +0200 | <tomsmeding> | % RevList [1..4] <> RevList [5..8] |
2022-10-28 12:17:05 +0200 | <yahb2> | RevList [5,6,7,8,1,2,3,4] |
2022-10-28 12:17:09 +0200 | <tomsmeding> | Profpatsch: seems to work |
2022-10-28 12:17:18 +0200 | <Profpatsch> | tomsmeding: huuuh |
2022-10-28 12:17:29 +0200 | <Profpatsch> | maybe I’m missing an extension |
2022-10-28 12:17:54 +0200 | <tomsmeding> | both extensions that you need to enable are clearly indicated in the error you get |
2022-10-28 12:17:56 +0200 | <tomsmeding> | so unlikely |
2022-10-28 12:18:12 +0200 | <Profpatsch> | tomsmeding: one sec |
2022-10-28 12:18:26 +0200 | <Profpatsch> | tomsmeding: https://zerobin.verklagmichdo.ch/paste/oQbaRRFW#pMEIil63xvsyWeAlN1n0kd2MhmNBpfvG6z1bK+Uo2OV |
2022-10-28 12:18:37 +0200 | <Profpatsch> | Oh I should read the error message |
2022-10-28 12:18:41 +0200 | <Profpatsch> | I have to import the Dual constructor |
2022-10-28 12:18:46 +0200 | <tomsmeding> | :) |
2022-10-28 12:18:47 +0200 | <tomsmeding> | yes |
2022-10-28 12:18:55 +0200 | <Profpatsch> | lol |
2022-10-28 12:18:57 +0200 | <Profpatsch> | sorry |
2022-10-28 12:19:07 +0200 | <tomsmeding> | 'coerce' will try to not "use" stuff that you wouldn't be able to use normally |
2022-10-28 12:19:24 +0200 | <Profpatsch> | prime hls potential |
2022-10-28 12:19:36 +0200 | <Profpatsch> | but prob nontrivial to implement a suggestion to import Dual |
2022-10-28 12:19:48 +0200 | td_ | (~td@83.135.9.42) (Ping timeout: 252 seconds) |
2022-10-28 12:19:49 +0200 | <Profpatsch> | I really need to get into hls dev |
2022-10-28 12:20:02 +0200 | <merijn> | Sure, but do you wanna implement custom warnings for every newtype in hls? |
2022-10-28 12:20:27 +0200 | <merijn> | Would be more sensible to work on the machine interface for GHC errors and have that integrated in there |
2022-10-28 12:20:33 +0200 | <tomsmeding> | merijn: I guess it could recognise "The data constructor `bla' of newtype `bla' is not in scope", and suggest import |
2022-10-28 12:20:37 +0200 | <tomsmeding> | yes for sure |
2022-10-28 12:20:43 +0200 | <Profpatsch> | well the GHC error would have to be structured enough |
2022-10-28 12:21:00 +0200 | <Profpatsch> | to turn the part that says “you might not have imported Dual” into a hls suggestion |
2022-10-28 12:21:10 +0200 | <merijn> | Profpatsch: There's a running project for structured GHC errors |
2022-10-28 12:21:21 +0200 | <Profpatsch> | So I guess by extension I’d have to get into GHC development lol |
2022-10-28 12:21:27 +0200 | <Profpatsch> | neverending rabbit holes |
2022-10-28 12:21:44 +0200 | <merijn> | tbh, GHC is pretty easy to work on if you're not touching the scary parts (type checker) |
2022-10-28 12:21:54 +0200 | <Profpatsch> | every nix user is a nix developer |
2022-10-28 12:21:58 +0200 | <Profpatsch> | every haskell user is a ghc developer |
2022-10-28 12:22:01 +0200 | <merijn> | One of my first ever Haskell contributions was a GHC patch |
2022-10-28 12:22:28 +0200 | <merijn> | The problem is that not every Haskell user is a GHC developer :p |
2022-10-28 12:22:29 +0200 | <geekosaur> | I have yet to contrib a patch but I review RTS code |
2022-10-28 12:22:58 +0200 | <Profpatsch> | the structured errors would be exposed via the GHC lib? |
2022-10-28 12:23:22 +0200 | <merijn> | Actually my *two* first Haskell contributiosn where GHC and I'm kinda proud of both, despite being trivial :p |
2022-10-28 12:23:48 +0200 | <Profpatsch> | https://gitlab.haskell.org/ghc/ghc/-/issues/18516 |
2022-10-28 12:24:42 +0200 | beteigeuze | (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) |
2022-10-28 12:26:02 +0200 | <Profpatsch> | I feel like this is too abstract tho |
2022-10-28 12:26:31 +0200 | <Profpatsch> | It would be better to just start with ideas for hls suggestions, and push them upstream by implementing the minimal amount of structure needed for these suggestions in GHC lib |
2022-10-28 12:27:05 +0200 | <Profpatsch> | (keeping that interface unstable between GHC versions until a nice interface is reached by experimentation) |
2022-10-28 12:27:55 +0200 | <tomsmeding> | I think programming against another unstable ghc interface is the absolute last thing that hls developers are looking for |
2022-10-28 12:27:57 +0200 | <Profpatsch> | then hls can add more and more stuff per GHC version without having to resort to dump string parsing |
2022-10-28 12:28:14 +0200 | <Profpatsch> | *dumb |
2022-10-28 12:28:30 +0200 | <Profpatsch> | tomsmeding: anything is more stable than parsing string output |
2022-10-28 12:28:41 +0200 | xff0x | (~xff0x@2405:6580:b080:900:2e5f:ef77:7c98:ca52) |
2022-10-28 12:29:19 +0200 | <Profpatsch> | well, string is the universal interface :P |
2022-10-28 12:29:26 +0200 | td_ | (~td@83.135.9.42) |
2022-10-28 12:29:37 +0200 | <Profpatsch> | as per the unix philosophy |
2022-10-28 12:29:40 +0200 | <merijn> | Profpatsch: hls is already ginormous |
2022-10-28 12:29:48 +0200 | <Profpatsch> | merijn: why? |
2022-10-28 12:29:53 +0200 | <merijn> | Profpatsch: Making it bigger with tons of custom code is undesirable |
2022-10-28 12:30:44 +0200 | axeman | (~quassel@212.129.78.247) |
2022-10-28 12:31:04 +0200 | <Profpatsch> | merijn: by that metric we should just outright delete 3 quarters of the Cabal codebase :) |
2022-10-28 12:31:54 +0200 | <Profpatsch> | which reminds me, I still have to finish the hoogle patches I submitted |
2022-10-28 12:32:20 +0200 | <merijn> | Except deleting that cabal could would break working things, I'm saying we shouldn't *add more* if possible |
2022-10-28 12:32:41 +0200 | <Profpatsch> | merijn: is anybody using backpack? :) |
2022-10-28 12:32:54 +0200 | mmhat | (~mmh@p200300f1c730768bee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.7.1) |
2022-10-28 12:33:01 +0200 | <tomsmeding> | kmett is, I think |
2022-10-28 12:33:12 +0200 | <Franciman> | i am |
2022-10-28 12:33:14 +0200 | <Franciman> | in ocaml |
2022-10-28 12:33:16 +0200 | <Franciman> | way better |
2022-10-28 12:33:18 +0200 | <Profpatsch> | lol |
2022-10-28 12:33:22 +0200 | <Profpatsch> | touche |
2022-10-28 12:33:25 +0200 | <merijn> | backpack is kinda dead due to ezyang getting hired away from Haskell into writing pytorch stuff |
2022-10-28 12:33:26 +0200 | <Profpatsch> | éééé |
2022-10-28 12:33:38 +0200 | <merijn> | As he was the driving force behind its implementation |
2022-10-28 12:33:44 +0200 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) (Ping timeout: 252 seconds) |
2022-10-28 12:34:14 +0200 | <Profpatsch> | Oh you can derive multiple things in the same clause super cool deriving (Semigroup, Monoid) via (Dual [a]) |
2022-10-28 12:41:36 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
2022-10-28 12:42:20 +0200 | acidjnk_new | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2022-10-28 12:42:46 +0200 | kenran | (~user@user/kenran) (Remote host closed the connection) |
2022-10-28 12:47:46 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
2022-10-28 12:59:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
2022-10-28 12:59:44 +0200 | acidjnk_new | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) |
2022-10-28 13:00:20 +0200 | acidjnk_new | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Client Quit) |
2022-10-28 13:00:30 +0200 | axeman | (~quassel@212.129.78.247) (Ping timeout: 252 seconds) |
2022-10-28 13:05:01 +0200 | birdgoose | (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
2022-10-28 13:13:45 +0200 | Kaiepi | (~Kaiepi@108.175.84.104) (Quit: Leaving) |
2022-10-28 13:15:18 +0200 | Kaiepi | (~Kaiepi@108.175.84.104) |
2022-10-28 13:29:13 +0200 | shriekingnoise | (~shrieking@186.137.167.202) |
2022-10-28 13:30:16 +0200 | frost53 | (~frost@user/frost) |
2022-10-28 13:32:21 +0200 | Midjak | (~Midjak@82.66.147.146) |
2022-10-28 13:42:50 +0200 | birdgoose | (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) (Ping timeout: 250 seconds) |
2022-10-28 13:47:33 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
2022-10-28 13:49:25 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
2022-10-28 13:53:05 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2022-10-28 13:56:15 +0200 | frost53 | (~frost@user/frost) (Quit: Client closed) |
2022-10-28 13:57:43 +0200 | frost70 | (~frost@user/frost) |
2022-10-28 14:04:50 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
2022-10-28 14:09:32 +0200 | yuzhao | (~yuzhao@36.112.45.73) |
2022-10-28 14:15:03 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
2022-10-28 14:15:37 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
2022-10-28 14:15:57 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 240 seconds) |
2022-10-28 14:16:36 +0200 | yuzhao | (~yuzhao@36.112.45.73) (Read error: Connection reset by peer) |
2022-10-28 14:17:36 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) |
2022-10-28 14:17:54 +0200 | <MangoIV[m]> | Does anybody here have know a good library to work with formal grammars? I mainly need cf. |
2022-10-28 14:19:48 +0200 | cheater | (~Username@user/cheater) (Quit: BitchX: fit to feel groovy) |
2022-10-28 14:19:53 +0200 | chomwitt | (~chomwitt@2a02:587:dc10:8200:1ac0:4dff:fedb:a3f1) |
2022-10-28 14:20:36 +0200 | cheater | (~Username@user/cheater) |
2022-10-28 14:21:44 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
2022-10-28 14:22:20 +0200 | <MangoIV[m]> | s/have// |
2022-10-28 14:22:39 +0200 | <merijn> | Work in what way? |
2022-10-28 14:23:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a04040206df7d69f9dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2022-10-28 14:23:47 +0200 | <MangoIV[m]> | construct them in an eDSL, do algorithms on them, generate strings from them, stuff like that. |
2022-10-28 14:24:24 +0200 | leagueoflegends | (~leagueofl@user/leagueoflegends) |
2022-10-28 14:24:34 +0200 | raek | (raek@2a01:7e01::f03c:93ff:fedf:bffe) |
2022-10-28 14:24:37 +0200 | <leagueoflegends> | what is a monad and can you give a code example/ |
2022-10-28 14:24:50 +0200 | yuzhao | (~yuzhao@36.112.45.73) |
2022-10-28 14:26:41 +0200 | <geekosaur> | http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html |
2022-10-28 14:27:17 +0200 | <geekosaur> | you don't care about anything beyond that |
2022-10-28 14:27:58 +0200 | frost70 | (~frost@user/frost) (Ping timeout: 244 seconds) |
2022-10-28 14:28:59 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
2022-10-28 14:31:22 +0200 | <leagueoflegends> | wait |
2022-10-28 14:31:22 +0200 | yuzhao | (~yuzhao@36.112.45.73) (Ping timeout: 250 seconds) |
2022-10-28 14:31:36 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 14:31:49 +0200 | <leagueoflegends> | leading up to a monad is a function that returns two separate times |
2022-10-28 14:31:56 +0200 | <leagueoflegends> | or at the same time |
2022-10-28 14:32:53 +0200 | <probie> | What is an iterable and can you give a code example? |
2022-10-28 14:34:10 +0200 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Ping timeout: 246 seconds) |
2022-10-28 14:34:27 +0200 | <leagueoflegends> | in what languge |
2022-10-28 14:34:29 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 14:34:29 +0200 | <leagueoflegends> | language |
2022-10-28 14:35:18 +0200 | <merijn> | leagueoflegends: Trying to understand the idea behind "monad" without first learning Haskell's type system and typeclasses is kinda futile, it won't make much sense. And once you understand how the types and typeclasses work then it's mostly obvious |
2022-10-28 14:36:05 +0200 | <geekosaur> | returning two things at the same time is just a tuple |
2022-10-28 14:36:13 +0200 | <probie> | leagueoflegends: In doesn't matter which language. The "joke" is that it defines an interface and many things satisfy that interface. |
2022-10-28 14:36:13 +0200 | <leagueoflegends> | oh |
2022-10-28 14:36:28 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 255 seconds) |
2022-10-28 14:38:05 +0200 | nilradical | (~nilradica@user/naso) |
2022-10-28 14:39:13 +0200 | <leagueoflegends> | what's the preferred way to install haskell on windows |
2022-10-28 14:39:17 +0200 | <probie> | For an example of a valid, but useless monad `data AMonad a = AMonad`, `instance Functor AMonad where fmap _ _ = AMonad` `instance Applicative AMonad where {pure _ = AMonad; (<*>) _ _ = AMonad}` `instance Monad AMonad where (>>=) _ _ = AMonad` |
2022-10-28 14:39:47 +0200 | <probie> | On all platforms, if you're not using nix, via ghcup |
2022-10-28 14:40:07 +0200 | <leagueoflegends> | why can't I just download an installer |
2022-10-28 14:41:46 +0200 | <geekosaur> | people use installers these days? |
2022-10-28 14:42:34 +0200 | <leagueoflegends> | never mind |
2022-10-28 14:42:37 +0200 | <leagueoflegends> | I'll use ghcip |
2022-10-28 14:42:40 +0200 | <leagueoflegends> | ghcup |
2022-10-28 14:44:11 +0200 | <leagueoflegends> | what is stack? |
2022-10-28 14:44:23 +0200 | CiaoSen | (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
2022-10-28 14:46:39 +0200 | <leagueoflegends> | should I install stack? |
2022-10-28 14:47:00 +0200 | <probie> | A build tool. It used to very popular, but it's less popular these days after many of the good ideas it introduced landed in cabal. Unless you're learning by following a tutorial that explicitly uses it, I wouldn't worry about it |
2022-10-28 14:47:09 +0200 | <probie> | s/used to very/used to be very/ |
2022-10-28 14:47:12 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:16c5:7e8f:5f7a:cef6) |
2022-10-28 14:47:48 +0200 | <leagueoflegends> | I said yes to the haskell language server as I want to use vscode or vim etc with haskell |
2022-10-28 14:48:03 +0200 | <leagueoflegends> | unless I'm doing something very wrong |
2022-10-28 14:48:39 +0200 | <probie> | Installing hls is probably a good idea |
2022-10-28 14:52:34 +0200 | <leagueoflegends> | is there any reason why GHC is so big say compared to a C compiler/ |
2022-10-28 14:52:42 +0200 | <leagueoflegends> | ?* |
2022-10-28 14:52:42 +0200 | <lambdabot> | Maybe you meant: v @ ? . |
2022-10-28 14:55:03 +0200 | <geekosaur> | it's doing a lot more than a C compiler |
2022-10-28 14:55:52 +0200 | <leagueoflegends> | ghc is .5gb while gcc is like .05gb |
2022-10-28 14:58:34 +0200 | <merijn> | leagueoflegends: A lot of gcc's install size is hidden inside your OS :p I have a user install of gcc in my homedir, it's 1.6 GB. Clang is well over 4-5 GB |
2022-10-28 14:58:34 +0200 | <leagueoflegends> | oops I accidentally install stack |
2022-10-28 14:58:43 +0200 | <leagueoflegends> | oh |
2022-10-28 14:58:55 +0200 | <leagueoflegends> | installed* |
2022-10-28 14:59:07 +0200 | <leagueoflegends> | will it conflict with cabal |
2022-10-28 14:59:20 +0200 | <probie> | The source for gcc is larger than the source for GHC thought :p |
2022-10-28 14:59:27 +0200 | <probie> | stack doesn't conflict with cabal |
2022-10-28 14:59:38 +0200 | <probie> | in fact, stack still needs cabal |
2022-10-28 14:59:49 +0200 | littlefinger | (~littlefin@pool-100-15-237-121.washdc.fios.verizon.net) |
2022-10-28 14:59:53 +0200 | <probie> | s/thought/though/ |
2022-10-28 14:59:58 +0200 | constxd | (~brad@47.55.121.233) |
2022-10-28 15:03:02 +0200 | <merijn> | probie: stack still needs Cabal it doesn't need cabal (the executable, aka cabal-install) |
2022-10-28 15:03:52 +0200 | <leagueoflegends> | do you recommend vim or neovim |
2022-10-28 15:04:10 +0200 | <leagueoflegends> | and ghcup installed haskell successfully |
2022-10-28 15:04:15 +0200 | <leagueoflegends> | I guess that's a start |
2022-10-28 15:05:10 +0200 | <probie> | merijn: does ghcup install them separately? I live in a nix world |
2022-10-28 15:06:17 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:16c5:7e8f:5f7a:cef6) (Ping timeout: 240 seconds) |
2022-10-28 15:07:38 +0200 | <geekosaur> | ghcup initially installs just ghc (9.2.4 currently) and HLS. `ghcup tui` lets you install stack and/or cabal |
2022-10-28 15:07:51 +0200 | <geekosaur> | (or `ghcup install stack`/`ghcup install cabal`) |
2022-10-28 15:07:57 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 272 seconds) |
2022-10-28 15:08:08 +0200 | <probie> | leagueoflegends: I think neovim with coc is gaining ground over regular vim, but I'm an emacs user and most of my coworkers use vscode, so take my opinion with a grain of salt |
2022-10-28 15:08:32 +0200 | <merijn> | probie: I dunno, I don't use ghcup, because I'm a grumpy old man |
2022-10-28 15:09:15 +0200 | <geekosaur> | <-- this grumpy old man uses ghcup. and even vscode for some things. but not nvim+coc |
2022-10-28 15:10:25 +0200 | <MangoIV[m]> | <MangoIV[m]> "Does anybody here have know a..." <- bumping this. Ideally it would also have an efficient representation for the grammars. |
2022-10-28 15:11:16 +0200 | <geekosaur> | might work better to ask on reddit or the discourse |
2022-10-28 15:11:24 +0200 | <merijn> | or haskell-cafe, yeah |
2022-10-28 15:11:29 +0200 | lortabac | (~lortabac@37.166.20.4) |
2022-10-28 15:14:30 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2022-10-28 15:16:00 +0200 | lortabac | (~lortabac@37.166.20.4) (Ping timeout: 250 seconds) |
2022-10-28 15:17:41 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:a2d7:73b4:5d4c:1129) |
2022-10-28 15:20:54 +0200 | <leagueoflegends> | what is coc |
2022-10-28 15:23:17 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 240 seconds) |
2022-10-28 15:23:56 +0200 | <geekosaur> | language server protocol plugin for nvim |
2022-10-28 15:24:15 +0200 | <geekosaur> | lets it speak to HLS and other LSP engines (for C, JS, etc.) |
2022-10-28 15:24:24 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
2022-10-28 15:26:09 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 15:26:13 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2022-10-28 15:27:56 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2022-10-28 15:32:57 +0200 | ft | (~ft@p508dbd59.dip0.t-ipconnect.de) |
2022-10-28 15:34:59 +0200 | littlefinger | (~littlefin@pool-100-15-237-121.washdc.fios.verizon.net) (Quit: Client closed) |
2022-10-28 15:36:06 +0200 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-10-28 15:37:05 +0200 | nilradical | (~nilradica@user/naso) |
2022-10-28 15:38:56 +0200 | <leagueoflegends> | what's the preferred way to install haskell in ubuntu? |
2022-10-28 15:39:23 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 3.7.1) |
2022-10-28 15:40:13 +0200 | vpan | (~0@212.117.1.172) |
2022-10-28 15:40:44 +0200 | jonathanx__ | (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
2022-10-28 15:43:31 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Ping timeout: 255 seconds) |
2022-10-28 15:45:19 +0200 | jonathanx_ | (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
2022-10-28 15:45:26 +0200 | <geekosaur> | same way. most OS distros have very old versions of GHC |
2022-10-28 15:45:57 +0200 | jonathanx__ | (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
2022-10-28 15:52:04 +0200 | <leagueoflegends> | ok, thanks |
2022-10-28 15:55:02 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2022-10-28 15:55:02 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2022-10-28 15:55:02 +0200 | wroathe | (~wroathe@user/wroathe) |
2022-10-28 15:55:22 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 15:56:22 +0200 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-10-28 15:57:34 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) |
2022-10-28 15:58:59 +0200 | slack1256 | (~slack1256@186.11.47.202) |
2022-10-28 15:59:48 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Ping timeout: 252 seconds) |
2022-10-28 16:00:39 +0200 | slac95907 | (~slack1256@191.125.99.208) |
2022-10-28 16:00:44 +0200 | nilradical | (~nilradica@user/naso) |
2022-10-28 16:02:17 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 240 seconds) |
2022-10-28 16:02:51 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
2022-10-28 16:03:28 +0200 | slack1256 | (~slack1256@186.11.47.202) (Ping timeout: 252 seconds) |
2022-10-28 16:04:15 +0200 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-10-28 16:04:31 +0200 | nilradical | (~nilradica@user/naso) |
2022-10-28 16:05:07 +0200 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2022-10-28 16:07:03 +0200 | mncheck | (~mncheck@193.224.205.254) (Quit: Leaving) |
2022-10-28 16:07:09 +0200 | mncheckm | (~mncheck@193.224.205.254) |
2022-10-28 16:07:22 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2022-10-28 16:13:06 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 16:13:37 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2022-10-28 16:15:37 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2022-10-28 16:16:44 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2022-10-28 16:18:15 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Ping timeout: 272 seconds) |
2022-10-28 16:27:16 +0200 | jonathanx | (~jonathan@94.234.119.48) |
2022-10-28 16:28:39 +0200 | mastarija | (~mastarija@188.252.199.190) |
2022-10-28 16:30:21 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2022-10-28 16:30:39 +0200 | <mastarija> | If I have this function in a file `foo = id :: Ord a => a -> a`, and load it into ghci and say `:t x = foo []` I get `[] :: Ord a => [a]`. |
2022-10-28 16:31:38 +0200 | <mastarija> | However, if I write `x = foo []` alongside the `foo` in that same file I get an error saying "ambiguous type variable a0 prevents constraint Ord a0 from being solved" |
2022-10-28 16:31:44 +0200 | <mastarija> | If I don't add the type signature. |
2022-10-28 16:32:32 +0200 | king_gs | (~Thunderbi@187.201.83.115) |
2022-10-28 16:34:07 +0200 | king_gs | (~Thunderbi@187.201.83.115) (Client Quit) |
2022-10-28 16:36:42 +0200 | <dolio> | That's the monomorphism restriction. |
2022-10-28 16:37:14 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2022-10-28 16:38:46 +0200 | <mastarija> | Ah.. I thought that too, and have added the MonomorphismRestriction extension instead of NoMonomorphismRestriction |
2022-10-28 16:38:49 +0200 | <mastarija> | x/ |
2022-10-28 16:39:54 +0200 | <mastarija> | thanks dolio |
2022-10-28 16:40:00 +0200 | <dolio> | No problem. |
2022-10-28 16:42:15 +0200 | tomku | (~tomku@user/tomku) |
2022-10-28 16:44:01 +0200 | burakcank | (burakcank@has.arrived.and.is.ready-to.party) (Killed (NickServ (GHOST command used by burakcank_!B438@free.znc.bg))) |
2022-10-28 16:44:15 +0200 | burakcank | (bnc4free@has.arrived.and.is.ready-to.party) |
2022-10-28 16:44:44 +0200 | mastarija | (~mastarija@188.252.199.190) (Quit: Leaving) |
2022-10-28 16:46:24 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 17:04:02 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
2022-10-28 17:04:35 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-10-28 17:04:37 +0200 | CiaoSen | (~Jura@p200300c95724d3002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2022-10-28 17:05:38 +0200 | jonathanx | (~jonathan@94.234.119.48) (Ping timeout: 250 seconds) |
2022-10-28 17:06:14 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:a2d7:73b4:5d4c:1129) (Ping timeout: 276 seconds) |
2022-10-28 17:09:02 +0200 | boxscape | (~boxscape@81.191.27.107) |
2022-10-28 17:09:16 +0200 | econo | (uid147250@user/econo) |
2022-10-28 17:10:02 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2022-10-28 17:12:22 +0200 | jonathanx | (~jonathan@c-5eea7730-74736162.cust.telenor.se) |
2022-10-28 17:13:10 +0200 | leagueoflegends | (~leagueofl@user/leagueoflegends) (Remote host closed the connection) |
2022-10-28 17:24:09 +0200 | jakalx | (~jakalx@base.jakalx.net) () |
2022-10-28 17:25:41 +0200 | jakalx | (~jakalx@base.jakalx.net) |
2022-10-28 17:26:07 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 255 seconds) |
2022-10-28 17:28:22 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
2022-10-28 17:31:10 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2022-10-28 17:32:28 +0200 | mrvdb | (~mrvdb@185.92.221.186) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-10-28 17:34:34 +0200 | jonathanx | (~jonathan@c-5eea7730-74736162.cust.telenor.se) (Remote host closed the connection) |
2022-10-28 17:34:55 +0200 | mrvdb | (~mrvdb@185.92.221.186) |
2022-10-28 17:34:56 +0200 | jonathanx | (~jonathan@94.234.119.48) |
2022-10-28 17:36:36 +0200 | boxscape | boxscape_ |
2022-10-28 17:40:10 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 17:46:06 +0200 | jonathanx | (~jonathan@94.234.119.48) (Ping timeout: 260 seconds) |
2022-10-28 17:49:58 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) |
2022-10-28 17:56:18 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 17:56:37 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 17:56:53 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 17:57:25 +0200 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-10-28 18:00:04 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 18:00:22 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 18:04:22 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
2022-10-28 18:06:19 +0200 | <monochrom> | EvanR: I now wonder if wikiepedia had a typo. If it said instead "here T |
2022-10-28 18:06:21 +0200 | <monochrom> | err |
2022-10-28 18:06:53 +0200 | <monochrom> | EvanR: I now wonder if wikiepedia had a typo. If it said instead "here Tµ and µT are formed by whiskering", that would be perfect. |
2022-10-28 18:08:34 +0200 | mrvdb | (~mrvdb@185.92.221.186) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-10-28 18:08:50 +0200 | mrvdb | (~mrvdb@2001:19f0:5000:8582:5400:ff:fe07:3df5) |
2022-10-28 18:08:56 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2022-10-28 18:10:20 +0200 | jonathanx | (~jonathan@c-5eea738b-74736162.cust.telenor.se) |
2022-10-28 18:16:49 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 18:18:25 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
2022-10-28 18:20:37 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Remote host closed the connection) |
2022-10-28 18:20:57 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
2022-10-28 18:21:07 +0200 | jonathanx | (~jonathan@c-5eea738b-74736162.cust.telenor.se) (Ping timeout: 272 seconds) |
2022-10-28 18:21:54 +0200 | Kaiepi | (~Kaiepi@108.175.84.104) (Ping timeout: 255 seconds) |
2022-10-28 18:24:07 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Read error: Connection reset by peer) |
2022-10-28 18:25:00 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
2022-10-28 18:26:34 +0200 | phma | (~phma@host-67-44-208-88.hnremote.net) (Read error: Connection reset by peer) |
2022-10-28 18:27:21 +0200 | phma | (~phma@2001:5b0:212a:cc58:94b0:45f6:bc48:ff7d) |
2022-10-28 18:27:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-10-28 18:28:43 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 272 seconds) |
2022-10-28 18:31:15 +0200 | fserucas|eod | (~fserucas|@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Quit: Leaving) |
2022-10-28 18:31:29 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2022-10-28 18:31:50 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-10-28 18:33:06 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 18:33:46 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 18:35:05 +0200 | titibandit | (~titibandi@xdsl-87-78-36-34.nc.de) |
2022-10-28 18:37:37 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
2022-10-28 18:40:15 +0200 | jonathanx | (~jonathan@94.234.102.75) |
2022-10-28 18:40:18 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Remote host closed the connection) |
2022-10-28 18:43:45 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2022-10-28 18:43:45 +0200 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2022-10-28 18:43:45 +0200 | wroathe | (~wroathe@user/wroathe) |
2022-10-28 18:44:58 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 18:47:48 +0200 | mixfix41 | (~sdeny9ee@user/mixfix41) |
2022-10-28 18:50:32 +0200 | nilradical | (~nilradica@user/naso) () |
2022-10-28 18:51:23 +0200 | redmp | (~redmp@eduroam-169-233-187-108.ucsc.edu) |
2022-10-28 18:51:55 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 18:54:06 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-10-28 18:55:57 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 272 seconds) |
2022-10-28 18:56:10 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
2022-10-28 18:56:48 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
2022-10-28 18:57:36 +0200 | vpan | (~0@212.117.1.172) (Quit: Leaving.) |
2022-10-28 18:58:09 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) |
2022-10-28 18:58:43 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 18:58:53 +0200 | Guest2776 | (~Guest27@2001:448a:7028:49a2:c005:3fe8:2bc0:33bd) |
2022-10-28 18:59:25 +0200 | Guest2776 | (~Guest27@2001:448a:7028:49a2:c005:3fe8:2bc0:33bd) (Client Quit) |
2022-10-28 19:00:56 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-10-28 19:01:57 +0200 | jonathanx | (~jonathan@94.234.102.75) (Ping timeout: 240 seconds) |
2022-10-28 19:02:42 +0200 | boxscape_ | (~boxscape@81.191.27.107) (Remote host closed the connection) |
2022-10-28 19:02:59 +0200 | boxscape | (~boxscape@81.191.27.107) |
2022-10-28 19:03:08 +0200 | boxscape | boxscape_ |
2022-10-28 19:03:24 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 19:05:09 +0200 | cross | (~cross@spitfire.i.gajendra.net) (Quit: leaving) |
2022-10-28 19:07:20 +0200 | johnw | (~johnw@2600:1700:cf00:db0:24dd:7cba:243c:c819) |
2022-10-28 19:10:09 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-10-28 19:11:14 +0200 | <EvanR> | monochrom, ah. Feel free to change it xD |
2022-10-28 19:13:57 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 19:14:06 +0200 | <EvanR> | but also by a leap of logic, whiskering is horizontal composition where one of the natural transformations is identity |
2022-10-28 19:15:08 +0200 | <EvanR> | Tµ =desugar=> id_T * µ |
2022-10-28 19:15:14 +0200 | Kaiepi | (~Kaiepi@108.175.84.104) |
2022-10-28 19:15:31 +0200 | <EvanR> | µT =desugar=> µ * id_T |
2022-10-28 19:21:26 +0200 | slack1256 | (~slack1256@186.11.44.138) |
2022-10-28 19:23:31 +0200 | slac95907 | (~slack1256@191.125.99.208) (Ping timeout: 260 seconds) |
2022-10-28 19:28:06 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-10-28 19:29:30 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 250 seconds) |
2022-10-28 19:30:16 +0200 | beteigeuze | (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) (Ping timeout: 252 seconds) |
2022-10-28 19:31:25 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
2022-10-28 19:31:26 +0200 | jakalx | (~jakalx@base.jakalx.net) () |
2022-10-28 19:31:48 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
2022-10-28 19:32:38 +0200 | sadmax2 | (~user@cpe-76-186-137-164.tx.res.rr.com) |
2022-10-28 19:33:24 +0200 | jakalx | (~jakalx@base.jakalx.net) |
2022-10-28 19:34:50 +0200 | sadmax2 | (~user@cpe-76-186-137-164.tx.res.rr.com) (Remote host closed the connection) |
2022-10-28 19:39:44 +0200 | jonathanx | (~jonathan@c-5eea74d9-74736162.cust.telenor.se) |
2022-10-28 19:40:31 +0200 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
2022-10-28 19:41:29 +0200 | sadmax | (~user@cpe-76-186-137-164.tx.res.rr.com) |
2022-10-28 19:42:11 +0200 | jonathanx_ | (~jonathan@c-5eea664b-74736162.cust.telenor.se) (Ping timeout: 260 seconds) |
2022-10-28 19:44:28 +0200 | titibandit | (~titibandi@xdsl-87-78-36-34.nc.de) (Quit: Leaving.) |
2022-10-28 19:46:18 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
2022-10-28 19:51:52 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 19:52:39 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 19:54:07 +0200 | <monochrom> | EvanR: Ah, thanks. |
2022-10-28 19:55:07 +0200 | slack3102 | (~slack1256@191.126.99.208) |
2022-10-28 19:57:18 +0200 | slack1256 | (~slack1256@186.11.44.138) (Ping timeout: 255 seconds) |
2022-10-28 19:58:00 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
2022-10-28 19:58:06 +0200 | berberman | (~berberman@user/berberman) (Ping timeout: 250 seconds) |
2022-10-28 19:58:44 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
2022-10-28 20:03:11 +0200 | <monochrom> | EvanR: Riehl's textbook (Category Theory in Context) section 1.7 has a brief intro to 2-catgories. It may help you decode that blog. Her homepage has the book in PDF for free: https://math.jhu.edu/~eriehl/ |
2022-10-28 20:04:38 +0200 | <monochrom> | Actually https://emilyriehl.github.io/ may be a more active page, heh. |
2022-10-28 20:10:19 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 20:10:54 +0200 | jonathanx_ | (~jonathan@c-5eea63bf-74736162.cust.telenor.se) |
2022-10-28 20:12:24 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
2022-10-28 20:13:36 +0200 | jonathanx | (~jonathan@c-5eea74d9-74736162.cust.telenor.se) (Ping timeout: 264 seconds) |
2022-10-28 20:15:34 +0200 | birdgoose | (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
2022-10-28 20:18:17 +0200 | sadmax | (~user@cpe-76-186-137-164.tx.res.rr.com) (Ping timeout: 272 seconds) |
2022-10-28 20:18:47 +0200 | <EvanR> | cool |
2022-10-28 20:19:29 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 20:21:14 +0200 | jonathanx_ | (~jonathan@c-5eea63bf-74736162.cust.telenor.se) (Ping timeout: 276 seconds) |
2022-10-28 20:24:06 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 250 seconds) |
2022-10-28 20:25:24 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 250 seconds) |
2022-10-28 20:26:53 +0200 | <jean-paul[m]> | `CString` is just an alias for `Ptr CChar` so any function, like `newCString` or `withCString` that gives you a `CString` might be giving you null, right? |
2022-10-28 20:28:16 +0200 | <monochrom> | Actually I doubt it. |
2022-10-28 20:29:09 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
2022-10-28 20:30:37 +0200 | <jean-paul[m]> | That would be great. But do I have to read GHC source or something to know for sure? |
2022-10-28 20:30:58 +0200 | <jean-paul[m]> | (if so, easier to just assume they could give me NULL, I think) |
2022-10-28 20:31:13 +0200 | <monochrom> | The source code rabbit hole seems to go through a "failWhenNULL" so you get an exception or you get a non-null pointer. |
2022-10-28 20:34:04 +0200 | birdgoose | (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) (Ping timeout: 250 seconds) |
2022-10-28 20:36:28 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2022-10-28 20:37:27 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e7137a26d59898e5c9870d6b.dip0.t-ipconnect.de) |
2022-10-28 20:37:36 +0200 | birdgoose | (~jesse@151.210.175.160) |
2022-10-28 20:41:11 +0200 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
2022-10-28 20:43:03 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 20:43:35 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-10-28 20:44:15 +0200 | birdgoose | (~jesse@151.210.175.160) (Ping timeout: 272 seconds) |
2022-10-28 20:45:14 +0200 | jakalx | (~jakalx@base.jakalx.net) |
2022-10-28 20:48:03 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
2022-10-28 20:50:24 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
2022-10-28 20:51:49 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 20:55:14 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
2022-10-28 20:56:17 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 240 seconds) |
2022-10-28 21:05:48 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 21:12:49 +0200 | danza | (~francesco@151.68.150.173) |
2022-10-28 21:13:28 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
2022-10-28 21:18:01 +0200 | <gurkenglas> | Let Phi be some set of functions Reals->Reals. Their pointwise infimum is at each point their greatest lower bound. This acts like an optic that can turn "all f in Phi satisfy foo(f) <= bar(f)" into "their pointwise infimum g satisfies foo(g) <= bar(f)" whenever foo and bar are monotonic. Thus it can turn "all Phi are monotonic/1-lipschitz/concave" into "their pointwise infimum is |
2022-10-28 21:18:07 +0200 | <gurkenglas> | monotonic/1-lipschitz/concave". I thought I would mention that here since I was surprised to be reminded of optics. |
2022-10-28 21:19:16 +0200 | <gurkenglas> | s/foo(g) <= bar(f)/foo(g) <= bar(g)/ :( |
2022-10-28 21:23:18 +0200 | thyriaen | (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) |
2022-10-28 21:24:48 +0200 | gqplox | (~textual@2a02:c7c:941d:fd00:40a0:1c9d:7a12:f334) |
2022-10-28 21:25:33 +0200 | slack1256 | (~slack1256@181.42.52.169) |
2022-10-28 21:26:25 +0200 | jinsun__ | (~jinsun@user/jinsun) |
2022-10-28 21:26:25 +0200 | jinsun | Guest7738 |
2022-10-28 21:26:25 +0200 | Guest7738 | (~jinsun@user/jinsun) (Killed (iridium.libera.chat (Nickname regained by services))) |
2022-10-28 21:26:25 +0200 | jinsun__ | jinsun |
2022-10-28 21:26:37 +0200 | slack3102 | (~slack1256@191.126.99.208) (Ping timeout: 240 seconds) |
2022-10-28 21:28:17 +0200 | <gqplox> | Hello guys |
2022-10-28 21:28:37 +0200 | <gqplox> | I have made a project in pytohn I want to convert it to haskell to learn haskell |
2022-10-28 21:28:58 +0200 | <gqplox> | However, for it i need to read toml and csv files |
2022-10-28 21:29:05 +0200 | <gqplox> | what is the easiest way to do it |
2022-10-28 21:29:29 +0200 | <energizer> | <EvanR: so a transpose of a 0 x inf matrix> but why is the empty arglist in zip() a 0 x inf matrix instead of, say, a 0 x 0 matrix? |
2022-10-28 21:29:44 +0200 | <gqplox> | Basically i want to focus on actually transforming the data for now and later on i can learn the io and monad stuff |
2022-10-28 21:29:59 +0200 | <gqplox> | but for now i just want a simple way to get the data in so i can do haskell stuff on it |
2022-10-28 21:30:12 +0200 | <jean-paul[m]> | gqplox: Maybe set aside the idea of "easiest" and just learn some stuff. |
2022-10-28 21:30:29 +0200 | <EvanR> | jean-paul[m], withCString uses allocaArray, which uses ... ... allocaBytesAlignedAndUnchecked which newAlignedPinnedByteArray# which can't fail |
2022-10-28 21:30:47 +0200 | <geekosaur> | we generally use cassava to read csv. dunno about toml |
2022-10-28 21:30:48 +0200 | <EvanR> | except that it is IO so anything can fail if you try hard enough |
2022-10-28 21:31:04 +0200 | <monochrom> | Perhaps choose a project that doesn't read toml. |
2022-10-28 21:31:05 +0200 | <jean-paul[m]> | gqplox: You can type things like "toml" and "yaml" into the search box on https://hoogle.haskell.org/ if you want to use libraries for this. |
2022-10-28 21:31:12 +0200 | <EvanR> | energizer, it isn't |
2022-10-28 21:31:29 +0200 | <EvanR> | there's no way to know using only list rep |
2022-10-28 21:31:56 +0200 | <energizer> | EvanR: so why would zip() be an inf x 0 matrix? |
2022-10-28 21:32:02 +0200 | <EvanR> | my observations just highlight all the important missing information in a ill typed variadic zip |
2022-10-28 21:32:16 +0200 | <EvanR> | energizer, repeat () would represent inf x 0 matrix |
2022-10-28 21:32:53 +0200 | <EvanR> | someone else suggested that is what zip() should return |
2022-10-28 21:33:12 +0200 | <EvanR> | more like, zip( a 0 x inf matrix ) should return repeat () |
2022-10-28 21:33:12 +0200 | <energizer> | EvanR: but you think it's ambiguous? |
2022-10-28 21:33:29 +0200 | <energizer> | EvanR: *but you think zip() is ambiguous? |
2022-10-28 21:33:31 +0200 | <EvanR> | and zip ( 0 x 17 matrix ) should return 17 ()s |
2022-10-28 21:33:57 +0200 | <gqplox> | yeah okay fair enough |
2022-10-28 21:34:07 +0200 | <gqplox> | thx for the website btw, looks helpful |
2022-10-28 21:34:33 +0200 | <EvanR> | zip() with no other information is ambiguous, such as what size you want |
2022-10-28 21:34:50 +0200 | <jean-paul[m]> | monochrom, EvanR : thanks |
2022-10-28 21:35:11 +0200 | <monochrom> | I did nothing :) |
2022-10-28 21:35:22 +0200 | <jean-paul[m]> | gqplox: Personally I found https://www.cis.upenn.edu/~cis1940/fall16/ to be a good resource to work though. |
2022-10-28 21:35:32 +0200 | <EvanR> | if your name is on the paper you're good |
2022-10-28 21:35:35 +0200 | <jean-paul[m]> | Hmmm nope, that's not the right link at all (maybe it is good but I haven't done it yet) |
2022-10-28 21:35:43 +0200 | <gqplox> | oh haha |
2022-10-28 21:35:53 +0200 | <gqplox> | right now i am doing programming in haskell by Graham Hutton |
2022-10-28 21:35:56 +0200 | <geekosaur> | @where cis194 |
2022-10-28 21:35:57 +0200 | <lambdabot> | https://www.seas.upenn.edu/~cis194/spring13/lectures.html |
2022-10-28 21:36:06 +0200 | <geekosaur> | is the usually recommended one hereabouts |
2022-10-28 21:36:07 +0200 | <energizer> | EvanR: i am sorta persuaded that zip is fairly tho not exactly monoidal, in which case repeat () is right |
2022-10-28 21:36:11 +0200 | <geekosaur> | but hutton's good too |
2022-10-28 21:36:16 +0200 | <gqplox> | im not far through but im eager to build stuff now that's why i was asking |
2022-10-28 21:36:19 +0200 | <jean-paul[m]> | Yes, thanks, that's the one. |
2022-10-28 21:36:40 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::f30b) |
2022-10-28 21:36:48 +0200 | <gqplox> | i understand your point, best to just learn properly |
2022-10-28 21:37:02 +0200 | <monochrom> | Dive-in projects are more haste less speed. |
2022-10-28 21:37:33 +0200 | <monochrom> | (Oh it "worked" when you switched from python to javascript because the difference was too small.) |
2022-10-28 21:38:23 +0200 | <gqplox> | haha :) i understand your point |
2022-10-28 21:38:29 +0200 | <gqplox> | oh this website looks cool |
2022-10-28 21:38:40 +0200 | <gqplox> | the seas.upenn |
2022-10-28 21:38:52 +0200 | <monochrom> | "I already speak American English. I want to learn Australian English by the dive-in project of writing a review for an Australian-accent movie." This works. |
2022-10-28 21:39:17 +0200 | <monochrom> | "I already speak American English. I want to learn Japanese by the dive-in project of writing a review for a Japanese movie." This breaks. |
2022-10-28 21:39:28 +0200 | <c_wraith> | I learned Haskell starting with making changes to a production system. It's not impossible, but you do need to be motivated by things like "This is hard and I want to learn it all" |
2022-10-28 21:39:52 +0200 | <c_wraith> | That was 14 years ago and I have not yet learned it all |
2022-10-28 21:40:14 +0200 | <gqplox> | yep i understand |
2022-10-28 21:40:23 +0200 | <c_wraith> | But I have learned a whole lot! |
2022-10-28 21:40:47 +0200 | <gqplox> | in this case it was a very minor thing, if i can get the toml and csv files into variables i can do it |
2022-10-28 21:40:55 +0200 | <gqplox> | anyway ill look at the upenn |
2022-10-28 21:42:13 +0200 | <monochrom> | There is also the prospect of not porting a python code base to haskell, instead write in haskell from scratch and implement the same features. |
2022-10-28 21:42:39 +0200 | <monochrom> | Indeed you wouldn't even try to translate C++ to C. |
2022-10-28 21:43:49 +0200 | <gqplox> | Yep that's what I meant sorry |
2022-10-28 21:43:58 +0200 | <gqplox> | and its like a 200 lines script haha |
2022-10-28 21:44:03 +0200 | <gqplox> | woah the .lhs is so cool |
2022-10-28 21:44:24 +0200 | <monochrom> | OK that works better. |
2022-10-28 21:46:38 +0200 | <monochrom> | Alternatively, dive-in projects can work (even for arbitrarily large gaps) if you manage your expectations. (Tautology: All frustrations can be solved by managing expectations.) |
2022-10-28 21:48:06 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
2022-10-28 21:48:19 +0200 | <monochrom> | The first dive-in project alerts you to a million things you need to learn first. Learning them can take a long time. If you don't have a conflicting expectation, you will persevere. |
2022-10-28 21:48:46 +0200 | <monochrom> | This initial investment amortizes. The 2nd, 3rd, ... projects will be much faster. |
2022-10-28 21:50:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-10-28 21:50:34 +0200 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
2022-10-28 21:52:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-10-28 21:52:44 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-10-28 21:58:44 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Quit: leaving) |
2022-10-28 21:59:56 +0200 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2022-10-28 22:02:11 +0200 | redmp | (~redmp@eduroam-169-233-187-108.ucsc.edu) (Ping timeout: 260 seconds) |
2022-10-28 22:02:28 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
2022-10-28 22:07:01 +0200 | <gurkenglas> | yeah i gave up on my 2nd and 3rd project much faster than on my 1st |
2022-10-28 22:07:21 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 22:10:23 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 272 seconds) |
2022-10-28 22:11:10 +0200 | birdgoose | (~jesse@2406:e003:1d87:6601:e725:b6b4:ace8:4ebe) |
2022-10-28 22:11:12 +0200 | hpc | (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 264 seconds) |
2022-10-28 22:11:49 +0200 | <c_wraith> | see how much faster you reached the natural conclusion? |
2022-10-28 22:12:36 +0200 | hpc | (~juzz@ip98-169-32-242.dc.dc.cox.net) |
2022-10-28 22:13:46 +0200 | <darkling> | If only I'd learned to give up programming 40 years ago. :) |
2022-10-28 22:15:09 +0200 | <gurkenglas> | noticing that training giving up allocates my skill ranks to Giving Up put such a pin into trying :D |
2022-10-28 22:16:46 +0200 | hpc | (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 250 seconds) |
2022-10-28 22:23:28 +0200 | hpc | (~juzz@ip98-169-32-242.dc.dc.cox.net) |
2022-10-28 22:23:55 +0200 | kjak | (~kjak@pool-108-31-114-135.washdc.fios.verizon.net) (Quit: leaving) |
2022-10-28 22:24:19 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 22:26:57 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 22:28:25 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 246 seconds) |
2022-10-28 22:30:57 +0200 | irrgit__ | (~irrgit@176.113.74.74) |
2022-10-28 22:31:31 +0200 | iteratee | (~kyle@162.218.222.107) |
2022-10-28 22:33:49 +0200 | irrgit_ | (~irrgit@176.113.74.130) (Ping timeout: 244 seconds) |
2022-10-28 22:34:21 +0200 | slack1256 | (~slack1256@181.42.52.169) (Ping timeout: 255 seconds) |
2022-10-28 22:34:35 +0200 | nate3 | (~nate@98.45.169.16) |
2022-10-28 22:35:36 +0200 | irrgit_ | (~irrgit@176.113.74.74) |
2022-10-28 22:38:02 +0200 | gqplox | (~textual@2a02:c7c:941d:fd00:40a0:1c9d:7a12:f334) (Quit: Textual IRC Client: www.textualapp.com) |
2022-10-28 22:38:56 +0200 | irrgit__ | (~irrgit@176.113.74.74) (Ping timeout: 260 seconds) |
2022-10-28 22:39:17 +0200 | nate3 | (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
2022-10-28 22:45:51 +0200 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 272 seconds) |
2022-10-28 22:46:15 +0200 | titibandit | (~titibandi@xdsl-87-78-36-34.nc.de) |
2022-10-28 22:47:24 +0200 | irrgit_ | (~irrgit@176.113.74.74) (Read error: Connection reset by peer) |
2022-10-28 22:48:29 +0200 | titibandit | (~titibandi@xdsl-87-78-36-34.nc.de) (Remote host closed the connection) |
2022-10-28 22:51:39 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
2022-10-28 22:52:10 +0200 | polo | (~polo@user/polo) |
2022-10-28 22:52:25 +0200 | polo | (~polo@user/polo) (Client Quit) |
2022-10-28 22:52:31 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2022-10-28 22:52:44 +0200 | polo | (~polo@user/polo) |
2022-10-28 22:53:36 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-10-28 22:54:37 +0200 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-10-28 22:56:27 +0200 | nek0 | (~nek0@2a01:4f8:222:2b41::12) (Quit: The Lounge - https://thelounge.chat) |
2022-10-28 23:01:47 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 23:03:13 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) |
2022-10-28 23:03:14 +0200 | bilegeek | (~bilegeek@2600:1008:b027:7f32:a99b:c297:feda:8531) |
2022-10-28 23:03:16 +0200 | <cpli> | are there async `Chan`s? |
2022-10-28 23:03:26 +0200 | <cpli> | i.e. where one may await `readChan`? |
2022-10-28 23:03:35 +0200 | <monochrom> | You can just use TChan. |
2022-10-28 23:04:16 +0200 | <monochrom> | Or Chan, too. |
2022-10-28 23:04:49 +0200 | <EvanR> | isn't await readChan already what readChan does |
2022-10-28 23:06:07 +0200 | mncheckm | (~mncheck@193.224.205.254) (Ping timeout: 272 seconds) |
2022-10-28 23:10:01 +0200 | <cpli> | so if i race between readChan and anything else, it's cancel safe? |
2022-10-28 23:13:43 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2022-10-28 23:15:03 +0200 | <dsal> | cpli: Not super clear what you mean. If you're waiting for a channel value in a transaction and get killed, it should be safe, but if you completed the transaction and were killed, it's not going to magically fix stuff. |
2022-10-28 23:19:05 +0200 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
2022-10-28 23:26:46 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
2022-10-28 23:30:03 +0200 | raek | (raek@2a01:7e01::f03c:93ff:fedf:bffe) (WeeChat 3.0) |
2022-10-28 23:35:12 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::f30b) (Ping timeout: 250 seconds) |
2022-10-28 23:38:53 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2022-10-28 23:38:58 +0200 | <EvanR> | if you're thinking of cancelling something doing a readChan then it does sound like you're at least going to need TChan |
2022-10-28 23:39:29 +0200 | <EvanR> | either the entire atomically containing readTChan happens or it doesn't |
2022-10-28 23:39:50 +0200 | <EvanR> | (STM) |
2022-10-28 23:46:55 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) (Remote host closed the connection) |
2022-10-28 23:51:07 +0200 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f81b:3b92:bbe7:93b6) |
2022-10-28 23:51:12 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 23:52:35 +0200 | <cpli> | perfect thank |
2022-10-28 23:54:25 +0200 | redmp | (~redmp@eduroam-169-233-187-108.ucsc.edu) |
2022-10-28 23:56:59 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::f30b) |
2022-10-28 23:57:03 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-10-28 23:59:21 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-10-28 23:59:33 +0200 | talismanick | (~talismani@76.133.152.122) (Remote host closed the connection) |