Logs on 2023-06-18 (liberachat/#haskell)
| 00:09:10 | × | Dykam quits (Dykam@dykam.nl) (Server closed connection) |
| 00:09:19 | → | Dykam joins (Dykam@dykam.nl) |
| 00:22:01 | × | pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-56-65-92-162-12.dsl.bell.ca) (Quit: ZNC 1.8.2 - https://znc.in) |
| 00:22:21 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-56-65-92-162-12.dsl.bell.ca) |
| 00:25:15 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 00:25:52 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 00:29:52 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 00:31:38 | <ijqq> | Hi I'm struggling to come up with a way to parse escapes in strings using applicative parsing. The issue is that my function to check an escape needs to take a look at multiple characters, so it works on strings. But I don't know how to make a parser that will parse everything between quotes, but also check for any amount of escapes. Well, I know that I could do it with a few case ofs but I don't know how to do it using the parsing |
| 00:31:38 | <ijqq> | functions that I've defined. Here is the file, it's quite messy but the string parsing function is on line 93 http://sprunge.us/jfTxfg. |
| 00:33:26 | <[Leary]> | Nosrep: I had to go read up on demand signatures to remind myself how to interpret them. My next best guess is that, with the function using 3 out of 5 fields from the outer product, GHC chooses not to unpack it. And without unpacking it, nothing further can be done. |
| 00:34:27 | <Nosrep> | hm maybe |
| 00:37:53 | <EvanR> | ijqq, with monadic parsing you could use manyTill to parse elements of the string until you encounter a (bare) quote. Escaped quote would be consumed by the inner parser |
| 00:41:13 | <ijqq> | EvanR ah interesting. I am trying to do it with just applicative ( I don't really know or understand monads yet xd) but thank you. I'll keep trying. |
| 00:43:31 | <EvanR> | I don't see a way to do it with *just* applicative and nothing else |
| 00:44:10 | <ijqq> | Oh right |
| 00:44:40 | → | extor joins (~extor@ns3018124.ip-149-202-82.eu) |
| 00:45:23 | <ijqq> | Did you look at the code I put? It has alternative too by the way, I forgot to say. |
| 00:45:28 | <EvanR> | the <*> operation lets you combine two parsers sequentially |
| 00:45:45 | <EvanR> | :t manyTill |
| 00:45:46 | <lambdabot> | error: Variable not in scope: manyTill |
| 00:46:12 | <EvanR> | manyTill :: Alternative m => m a -> m end -> m [a] |
| 00:47:01 | <EvanR> | Alternative adds the ability to repeat a parser |
| 00:47:20 | <EvanR> | so looks like you don't need monads |
| 00:47:44 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 00:49:18 | <ijqq> | In my code i have Parser a = Parser {parse :: String -> Maybe (String, a)} so I think I can definitely write a function which will be like Parser $\ case ('\\':xs) | x `elem` escapeChars ... .But I was wondering how to write something similar to how my other functions are |
| 00:49:51 | <EvanR> | if you write explicit code that's another story |
| 00:50:35 | <EvanR> | if you implemented Alternative you can use manyTill from Text.Parser.Combinators |
| 00:50:35 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 00:51:54 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 00:53:33 | <ijqq> | Hmm, I don't seem to have that library; I can't import it. But thanks for the help, maybe I'll try write something similar. |
| 00:54:13 | <EvanR> | you could read the docs if you don't want to add the package https://hackage.haskell.org/package/parsers-0.12.11/docs/Text-Parser-Combinators.html#v:manyTill |
| 00:55:07 | <EvanR> | the implementation is 1 line |
| 00:56:09 | × | fweht quits (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 01:04:25 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 01:04:25 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 01:05:20 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 01:05:45 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 260 seconds) |
| 01:09:24 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
| 01:09:38 | <ijqq> | manyTill :: Alternative m => m a -> m end -> m [a] I still don't really understand how I can use it. So end would be a parser that inspects two chars and if the first is not a backslash and second is a quote, then it succeeds? And the m a I think would be a Parser String as I need to look at two chars at a time. So then It'd give me Parser [String]? |
| 01:09:48 | → | tomku joins (~tomku@user/tomku) |
| 01:10:12 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:13:15 | × | Ranhir quits (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 01:16:20 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:16:52 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 01:17:06 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 01:22:14 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 01:22:55 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 01:26:26 | → | chromoblob joins (~user@37.113.180.121) |
| 01:27:09 | → | tomku joins (~tomku@user/tomku) |
| 01:33:39 | <EvanR> | ijqq, end would inspect 1 char, to see if it's a " |
| 01:34:34 | <EvanR> | the a in m a is what type the parser produces, not what it inspects |
| 01:35:18 | <EvanR> | so if you are parsing a string literal to get character by character (interpreting escapes in the process), a = Char and [a] is String |
| 01:36:59 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 01:38:30 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 240 seconds) |
| 01:39:44 | <monochrom> | manyTill is unlikely to help if you need lookahead/backtrack of 2 or more characters. |
| 01:39:59 | → | trev joins (~trev@user/trev) |
| 01:40:41 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 01:41:45 | <monochrom> | Err, no, I was wrong. |
| 01:42:11 | <EvanR> | the inner parser here could consume 1 or 2 characters to generate the next literal character |
| 01:42:58 | <monochrom> | Yeah, I just realized that "foo :: Parser Char" does not mean that it cannot consume 2 characters. |
| 01:45:29 | → | Angelz joins (~Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) |
| 01:46:34 | <monochrom> | foo = satisfy (/= '\\') <|> (char '\\' *> fmap translate_escape_code anyChar) |
| 01:48:49 | <EvanR> | that lines of code makes me hate /= |
| 01:49:14 | <monochrom> | > let (!=) = (/=) in 1 != 2 |
| 01:49:15 | <lambdabot> | True |
| 01:49:28 | <monochrom> | I think you can do that if you hate /= :) |
| 01:49:33 | <monochrom> | In fact, =) |
| 01:49:52 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 240 seconds) |
| 01:50:42 | <monochrom> | I think you can also do this: |
| 01:50:49 | <monochrom> | > let (\=) = (/=) in 1 \= 2 |
| 01:50:51 | <lambdabot> | True |
| 01:51:00 | <monochrom> | foo = satisfy (\= '\\') <|> (char '\\' *> fmap translate_escape_code anyChar) |
| 01:51:50 | <monochrom> | "monochrom received a backlash for proposing backslash-intensive code" :) |
| 01:51:50 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 01:52:16 | → | tomku joins (~tomku@user/tomku) |
| 01:52:46 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 01:52:59 | × | parseval quits (sid239098@id-239098.helmsley.irccloud.com) (Server closed connection) |
| 01:53:13 | → | parseval joins (sid239098@id-239098.helmsley.irccloud.com) |
| 02:04:58 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 02:04:58 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 02:04:58 | → | wroathe joins (~wroathe@user/wroathe) |
| 02:04:58 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 02:06:20 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 02:07:02 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Remote host closed the connection) |
| 02:07:50 | → | gurkenglas joins (~user@dynamic-046-114-176-022.46.114.pool.telefonica.de) |
| 02:14:33 | × | bilegeek quits (~bilegeek@2600:1008:b085:8180:1da1:2103:9ba6:bd4d) (Quit: Leaving) |
| 02:15:25 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 02:16:16 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:16:16 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:16:16 | finn_elija | is now known as FinnElija |
| 02:22:19 | <[Leary]> | ijqq: You can do what you want with what you've already written. Consider something of the form: `char '"' *> (fmap _ . many) (isMany _ <|> escape) <* char '"'`. I'd venture it's faster too, though you may need to rewrite `isMany` as a primitive. |
| 02:29:27 | × | mud quits (~mud@user/kadoban) (Remote host closed the connection) |
| 02:29:52 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 240 seconds) |
| 02:29:52 | → | mud joins (~mud@user/kadoban) |
| 02:30:20 | × | hpc quits (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 240 seconds) |
| 02:30:33 | → | hpc joins (~juzz@ip98-169-35-163.dc.dc.cox.net) |
| 02:31:16 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 02:32:01 | → | tomku joins (~tomku@user/tomku) |
| 02:32:01 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 02:32:46 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 02:38:40 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 02:38:40 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 02:39:14 | × | td_ quits (~td@i5387091A.versanet.de) (Ping timeout: 252 seconds) |
| 02:39:16 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 02:41:13 | → | td_ joins (~td@i5387092E.versanet.de) |
| 02:41:21 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 02:43:23 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 02:44:16 | → | tomku joins (~tomku@user/tomku) |
| 02:52:11 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 246 seconds) |
| 02:54:00 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 02:57:04 | → | jinsun joins (~jinsun@user/jinsun) |
| 03:02:20 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 03:03:32 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 240 seconds) |
| 03:14:32 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 240 seconds) |
| 03:18:39 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 258 seconds) |
| 03:19:55 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 03:21:03 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 03:22:01 | → | chromoblob joins (~user@37.113.180.121) |
| 03:27:32 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 03:32:49 | × | ijqq quits (uid603979@id-603979.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 03:38:23 | <mauke> | > let (≠) = (/=) in 1 ≠ 2 |
| 03:38:24 | <lambdabot> | True |
| 03:39:43 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 03:39:43 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 03:40:10 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 03:40:35 | → | arrowhead joins (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) |
| 03:42:50 | <EvanR> | \o/ |
| 03:42:52 | <EvanR> | ⦻ |
| 03:43:04 | → | falafel joins (~falafel@2607:fb91:86c:d890:3d8c:5948:319b:d394) |
| 03:43:32 | <EvanR> | who needs unicode, just =<backspace>/ |
| 03:50:16 | → | Inst joins (~Inst@2601:6c4:4081:2fc0:4f54:13aa:bf33:bb41) |
| 03:50:17 | <Inst> | wait |
| 03:50:32 | <Inst> | well, i guess voidf still isn't a monad because free monads are cheating |
| 03:50:35 | <Inst> | but it's giggly |
| 03:52:34 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 03:53:09 | × | gurkenglas quits (~user@dynamic-046-114-176-022.46.114.pool.telefonica.de) (Ping timeout: 258 seconds) |
| 03:59:09 | → | meeks joins (~meeks@2600:6c5e:1300:28:4756:6a12:671:5a0d) |
| 04:01:16 | × | falafel quits (~falafel@2607:fb91:86c:d890:3d8c:5948:319b:d394) (Remote host closed the connection) |
| 04:02:07 | × | meeks quits (~meeks@2600:6c5e:1300:28:4756:6a12:671:5a0d) (Quit: WeeChat 3.5) |
| 04:11:45 | <Nosrep> | after further experimentation on the worker-wrapper thing i have discovered on a flat datatype of Words ghc refuses to do the worker-wrapper trick when there are >10 Words in the type |
| 04:12:09 | <Nosrep> | this also happens when i put the Words in another datatype like a tuple with 2 elements, the maximum is 5 of those wrapper datatypes so still 10 words total |
| 04:12:25 | <Nosrep> | whats ghc's rationale for limiting it at 10 |
| 04:15:42 | → | tomku joins (~tomku@user/tomku) |
| 04:16:33 | <Nosrep> | hm -fmax-worker-args |
| 04:25:20 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 04:44:08 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds) |
| 04:44:38 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 04:45:21 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 04:48:16 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 04:50:27 | → | tomku joins (~tomku@user/tomku) |
| 04:52:20 | × | bontaq quits (~user@ool-45779b84.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 05:08:14 | × | nadja quits (~dequbed@banana-new.kilobyte22.de) (Server closed connection) |
| 05:08:52 | → | nadja joins (~dequbed@2a01:4f8:201:34c7::1) |
| 05:09:00 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 05:20:25 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 05:21:24 | → | coot joins (~coot@89.69.206.216) |
| 05:21:25 | × | arrowhead quits (~arrowhead@2603-7000-9b3f-6934-a88a-36a7-e0af-5d4c.res6.spectrum.com) (Read error: Connection reset by peer) |
| 05:22:12 | → | arrowhead joins (~arrowhead@cpe-74-66-76-151.nyc.res.rr.com) |
| 05:22:55 | → | smoge joins (~smoge@2603-7000-4b42-1100-9dab-c33e-5e93-2285.res6.spectrum.com) |
| 05:25:05 | → | tomku joins (~tomku@user/tomku) |
| 05:28:46 | <smoge> | can someone help a beginner to define a type? |
| 05:32:18 | <smoge> | http://recherche.ircam.fr/equipes/repmus/OpenMusic/user-doc/DocFiles/Documentation/Rhythm.html |
| 05:32:34 | <smoge> | It isn't quite right: |
| 05:32:34 | <smoge> | data RTMNode = RTMInt Int | RTMList [RTMNode] deriving (Show) |
| 05:33:28 | <pavonia> | What's wrong with it? |
| 05:34:40 | <smoge> | A Rhythm Tree is a list of lists, it can be a list of ints (1 1 1 2), or one of the items can be subdivided, for example, 1 becomes (1 (1 1 1)). the list would become ((1 (1 1 1)) 1 1 2) |
| 05:34:53 | <smoge> | I can't translate that into a type |
| 05:36:00 | <smoge> | It's a way to represent music rhythms |
| 05:36:26 | <davean> | Do you mean you want data RTMNode = RTMInt Int | RTMList Int [RTMNode] deriving (Show)? |
| 05:36:40 | <davean> | I'm a little confused as to what you mean is off |
| 05:36:45 | <chromoblob> | why doesn't your definition work? |
| 05:37:16 | <davean> | can it not nest further? You say tree so I assume it can |
| 05:37:19 | <smoge> | because my original definition is too general, thatnks davean, maybe it will work, I'll test it |
| 05:37:37 | <smoge> | it should be recursive, yes |
| 05:37:57 | <smoge> | http://recherche.ircam.fr/equipes/repmus/OpenMusic/user-doc/DocFiles/Documentation/Rhythm.html |
| 05:37:58 | <chromoblob> | RTMList [RTMList [RTMInt 1, RTMList [RTMInt 1, RTMInt 1, RTMInt 1]], RTMInt 1, RTMInt 1, RTMInt 2] |
| 05:38:00 | <davean> | you might also want to see NonEmpty |
| 05:38:16 | <probie> | I'd be inclined to go with `data RTMNode = RTMNode Int [RTMNode]` |
| 05:38:33 | <smoge> | why NonEmpty? |
| 05:39:28 | <smoge> | Is it problematic to use |
| 05:39:28 | <smoge> | showRTM :: RTMNode -> String |
| 05:39:29 | <smoge> | showRTM (RTMInt i) = show i |
| 05:39:29 | <smoge> | showRTM (RTMList l) = "(" ++ unwords (map showRTM l) ++ ")" |
| 05:39:42 | <smoge> | so it would show a more readable output |
| 05:40:56 | <chromoblob> | showRTM seems fine |
| 05:41:14 | <smoge> | @probie why? in addiction to RTMNode = RTMInt Int | RTMList Int [RTMNode] ? |
| 05:41:14 | <lambdabot> | Unknown command, try @list |
| 05:41:24 | <smoge> | probie why? in addiction to RTMNode = RTMInt Int | RTMList Int [RTMNode] ? |
| 05:43:07 | <probie> | smoge: You can't have an empty list. I'm just being lazy and folding `data RTMNode = RTMInt Int | RTMList Int (NonEmpty RTMNode)` into a single constructor |
| 05:44:44 | <smoge> | makes sense, thanks |
| 05:44:44 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 05:44:59 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Quit: Leaving) |
| 05:45:14 | <probie> | but on re-reading I don't think this is sufficient, since according to the spec, I need to support fractions, and at the measure level, genuinely need pairs (at least if I want to distinguish between things like 4/4 and 2/2) |
| 05:46:45 | <smoge> | Yes, that's just part of the syntax. Those are the time signatures. I'll need a type for that I think |
| 05:48:04 | × | hpc quits (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 252 seconds) |
| 05:48:38 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 05:49:56 | → | tomku joins (~tomku@user/tomku) |
| 05:50:20 | → | hpc joins (~juzz@98.169.35.163) |
| 05:51:30 | × | phileasfogg quits (~phileasfo@user/phileasfogg) (Server closed connection) |
| 05:51:53 | → | phileasfogg joins (~phileasfo@user/phileasfogg) |
| 05:52:30 | <smoge> | Where should I start to write a little parser for this? Any tips? |
| 05:53:56 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 05:55:40 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 05:56:08 | <smoge> | beatParser :: Parser RTMNode |
| 05:56:09 | <smoge> | beatParser = RTMInt . read <$> many1 digit |
| 05:56:09 | <smoge> | rtmParser :: Parser RTMNode |
| 05:56:10 | <smoge> | rtmParser = try beatParser <|> listParser |
| 05:56:10 | <smoge> | listParser :: Parser RTMNode |
| 05:56:11 | <smoge> | listParser = do |
| 05:56:11 | <smoge> | _ <- char '(' |
| 05:56:12 | <smoge> | nodes <- sepBy rtmParser (many1 space) |
| 05:56:12 | <smoge> | _ <- char ')' |
| 05:56:13 | <smoge> | return $ RTMList nodes |
| 05:56:13 | <smoge> | parseRTM :: String -> Either ParseError RTMNode |
| 05:56:14 | <smoge> | parseRTM = parse rtmParser "" |
| 05:59:29 | <mauke> | listParser = RTMList <$> (char '(' *> sepBy rtmParser (many1 space) <* char ')') -- using Applicative |
| 05:59:37 | <probie> | Does that handle rests? (which are represented with negative numbers) |
| 05:59:48 | × | dy quits (sid3438@user/dy) (Server closed connection) |
| 06:00:25 | → | dy joins (sid3438@user/dy) |
| 06:03:31 | <probie> | I also think it fails when there are spaces where you don't expect, for example, try it on `(2( (1(1 1 1 1))(1(1 1 1 1)))` |
| 06:08:39 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 06:08:56 | <smoge> | Yes, it's not very good. But I'm just starting with Haskell. I'd appreciate some tips |
| 06:10:30 | <probie> | I'm not sure what parsing library you're using, but it probably has some sort of `lexeme` combinator that you probably want to look into using for handling whitespace |
| 06:11:56 | <smoge> | thanks probie. yes, I haven't thought about rests yet.... |
| 06:13:48 | → | tomku joins (~tomku@user/tomku) |
| 06:15:05 | <smoge> | probie, Parsec. I think you're suggesting this? https://hackage.haskell.org/package/parsec-3.1.3/docs/Text-Parsec-Token.html#v:lexeme |
| 06:15:30 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 240 seconds) |
| 06:16:03 | → | jinsun joins (~jinsun@user/jinsun) |
| 06:16:58 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 06:25:16 | → | Pickchea joins (~private@user/pickchea) |
| 06:26:32 | → | acidjnk joins (~acidjnk@p5dd870a3.dip0.t-ipconnect.de) |
| 06:33:53 | → | jonathan_ joins (~jonathan@83.252.3.92) |
| 06:39:17 | → | lottaquestions_ joins (~nick@2607:fa49:503f:6d00:ed09:2f19:74f7:7b05) |
| 06:41:26 | × | lottaquestions quits (~nick@2607:fa49:503f:6d00:a5bc:3af4:48cc:9dd6) (Ping timeout: 265 seconds) |
| 06:41:43 | → | puke joins (~puke@user/puke) |
| 06:41:58 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 06:43:24 | × | monochrom quits (trebla@216.138.220.146) (Quit: NO CARRIER) |
| 06:44:08 | × | lottaquestions_ quits (~nick@2607:fa49:503f:6d00:ed09:2f19:74f7:7b05) (Client Quit) |
| 06:44:32 | → | lottaquestions_ joins (~nick@2607:fa49:503f:6d00:ed09:2f19:74f7:7b05) |
| 06:48:56 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 06:51:13 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 07:01:00 | × | shapr quits (~user@2600:1700:c640:3100:11cd:d5ec:6209:48bd) (Ping timeout: 260 seconds) |
| 07:01:11 | → | takuan joins (~takuan@178.116.218.225) |
| 07:01:32 | → | monochrom joins (trebla@216.138.220.146) |
| 07:10:12 | × | jargon quits (~jargon@184.101.75.235) (Ping timeout: 252 seconds) |
| 07:13:15 | → | gmg joins (~user@user/gehmehgeh) |
| 07:13:36 | × | gmg quits (~user@user/gehmehgeh) (Client Quit) |
| 07:13:39 | × | conjunctive quits (sid433686@id-433686.helmsley.irccloud.com) (Server closed connection) |
| 07:14:15 | → | conjunctive joins (sid433686@2a03:5180:f:1::6:9e16) |
| 07:16:25 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 07:17:00 | × | lambdabot quits (~lambdabot@haskell/bot/lambdabot) (Server closed connection) |
| 07:18:03 | × | zxrom quits (~zxrom@mm-196-2-212-37.vitebsk.dynamic.pppoe.byfly.by) (Quit: Leaving) |
| 07:19:03 | → | gmg joins (~user@user/gehmehgeh) |
| 07:19:08 | → | lambdabot joins (~lambdabot@silicon.int-e.eu) |
| 07:19:08 | × | lambdabot quits (~lambdabot@silicon.int-e.eu) (Changing host) |
| 07:19:08 | → | lambdabot joins (~lambdabot@haskell/bot/lambdabot) |
| 07:20:48 | → | merijn joins (~merijn@86.86.29.250) |
| 07:26:53 | → | dtman34 joins (~dtman34@2601:447:d000:93c9:2c61:433f:e0a9:a7c4) |
| 07:36:00 | × | dtman34 quits (~dtman34@2601:447:d000:93c9:2c61:433f:e0a9:a7c4) (Ping timeout: 260 seconds) |
| 07:36:01 | → | dtman34_ joins (~dtman34@2601:447:d000:93c9:b581:a620:d736:2367) |
| 07:36:58 | → | zxrom joins (~zxrom@mm-196-2-212-37.vitebsk.dynamic.pppoe.byfly.by) |
| 07:40:49 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 07:44:42 | → | dtman34 joins (~dtman34@2601:447:d000:93c9:626c:6ed7:c046:4c00) |
| 07:44:44 | × | dtman34_ quits (~dtman34@2601:447:d000:93c9:b581:a620:d736:2367) (Ping timeout: 240 seconds) |
| 07:49:15 | × | ubert quits (~Thunderbi@p200300ecdf0da912f884ed912556b966.dip0.t-ipconnect.de) (Quit: ubert) |
| 07:49:33 | → | Guest44 joins (~Guest39@1.145.147.142) |
| 07:54:12 | × | merijn quits (~merijn@86.86.29.250) (Ping timeout: 240 seconds) |
| 07:59:23 | <Guest44> | trouble getting started with this command: |
| 07:59:23 | <Guest44> | ghci part18.lhs |
| 07:59:24 | <Guest44> | where part18.lhs comes from https://www.haskell.org/tutorial/code/ |
| 07:59:24 | <Guest44> | error reported: part18.lhs:46:12: error: |
| 07:59:25 | <Guest44> | • No instance for (Applicative SM) |
| 07:59:25 | <Guest44> | arising from the superclasses of an instance declaration |
| 07:59:26 | <Guest44> | • In the instance declaration for ‘Monad SM’ |
| 07:59:26 | <Guest44> | line 46 starts with > instance Monad in the following: |
| 07:59:45 | <Guest44> | Section 9.3 |
| 07:59:46 | <Guest44> | > type S = Int |
| 07:59:46 | <Guest44> | > data SM a = SM (S -> (a,S)) -- The monadic type |
| 07:59:47 | <Guest44> | > instance Monad SM where |
| 07:59:47 | <Guest44> | > -- defines state propagation |
| 07:59:48 | <lambdabot> | <hint>:1:1: error: parse error on input ‘type’ |
| 07:59:48 | <Guest44> | > SM c1 >>= fc2 = SM (\s0 -> let (r,s1) = c1 s0 |
| 07:59:48 | <lambdabot> | <hint>:1:1: error: parse error on input ‘data’ |
| 07:59:48 | <Guest44> | > SM c2 = fc2 r in |
| 07:59:49 | <Guest44> | > c2 s1) |
| 07:59:49 | <lambdabot> | <hint>:1:1: error: parse error on input ‘instance’ |
| 07:59:49 | <Guest44> | > return k = SM (\s -> (k,s)) |
| 08:08:40 | <probie> | Guest44: That tutorial might be outdated. You now also need to define an `Applicative` instance. |
| 08:10:27 | <probie> | Since you've already defined a monad instance, you should be able to do something like `instance Applicative SM where { pure = return; f <*> x = do { f' <- f; x' <- x; pure (f' x') }}` |
| 08:13:25 | <probie> | also, in future if it's more than about 3 lines, use something like https://paste.tomsmeding.com and share the link |
| 08:21:50 | <Guest44> | ok thanks probie |
| 08:22:32 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 08:23:14 | × | hammond quits (proscan@user/hammond2) (Server closed connection) |
| 08:23:22 | → | hammond joins (proscan@gateway02.insomnia247.nl) |
| 08:30:25 | × | Philonous quits (~Philonous@user/philonous) (Quit: ZNC - https://znc.in) |
| 08:30:51 | → | Philonous joins (~Philonous@user/philonous) |
| 08:31:50 | × | davean quits (~davean@davean.sciesnet.net) (Server closed connection) |
| 08:32:36 | → | davean joins (~davean@67.205.182.208) |
| 08:44:54 | × | hueso_ quits (~root@user/hueso) (Server closed connection) |
| 08:45:06 | → | hueso joins (~root@user/hueso) |
| 08:49:14 | → | alexherbo2 joins (~alexherbo@2a02-842a-8180-4601-e9ea-f8a5-e557-b41f.rev.sfr.net) |
| 08:51:11 | × | mcglk quits (~mcglk@131.191.19.145) (Remote host closed the connection) |
| 08:55:49 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Ping timeout: 268 seconds) |
| 08:57:48 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 08:58:50 | × | dtman34 quits (~dtman34@2601:447:d000:93c9:626c:6ed7:c046:4c00) (Ping timeout: 260 seconds) |
| 08:58:50 | → | dtman34_ joins (~dtman34@2601:447:d000:93c9:49a3:2ee1:9e07:c081) |
| 09:01:37 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 09:01:40 | → | aforemny_ joins (~aforemny@2001:9e8:6ce0:8f00:7cf4:9859:63d6:96a8) |
| 09:02:30 | × | aforemny_ quits (~aforemny@2001:9e8:6ce0:8f00:7cf4:9859:63d6:96a8) (Quit: ZNC 1.8.2 - https://znc.in) |
| 09:03:34 | → | aforemny joins (~aforemny@2001:9e8:6ce0:8f00:7cf4:9859:63d6:96a8) |
| 09:08:42 | × | aforemny quits (~aforemny@2001:9e8:6ce0:8f00:7cf4:9859:63d6:96a8) (Quit: ZNC 1.8.2 - https://znc.in) |
| 09:09:40 | → | fendor joins (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) |
| 09:10:16 | → | aforemny joins (~aforemny@2001:9e8:6ce0:8f00:7cf4:9859:63d6:96a8) |
| 09:12:20 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 09:13:17 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 09:15:52 | → | gurkenglas joins (~user@dynamic-046-114-182-229.46.114.pool.telefonica.de) |
| 09:22:41 | × | Guest44 quits (~Guest39@1.145.147.142) (Quit: Client closed) |
| 09:25:25 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 09:43:14 | <tomsmeding> | :t Control.Monad.ap -- probie |
| 09:43:16 | <lambdabot> | Monad m => m (a -> b) -> m a -> m b |
| 09:43:38 | <tomsmeding> | {pure = return; (<*>) = ap} is a sufficient definition for Applicative once you have Monad |
| 09:45:18 | → | titibandit joins (~titibandi@user/titibandit) |
| 09:48:57 | <probie> | tomsmeding: but that requires importing `Control.Monad` |
| 09:52:26 | × | tubogram44711 quits (~tubogram@user/tubogram) (Quit: See ya later!) |
| 09:55:22 | <tomsmeding> | it does yeah |
| 09:55:41 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 09:55:54 | ← | zxrom parts (~zxrom@mm-196-2-212-37.vitebsk.dynamic.pppoe.byfly.by) (Leaving) |
| 09:59:20 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Read error: Connection reset by peer) |
| 09:59:36 | → | kritzefitz joins (~kritzefit@debian/kritzefitz) |
| 10:01:34 | → | tubogram44711 joins (~tubogram@user/tubogram) |
| 10:03:13 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 10:07:28 | → | p3n joins (~p3n@217.198.124.246) |
| 10:08:59 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 10:09:42 | → | Pickchea joins (~private@user/pickchea) |
| 10:11:25 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
| 10:13:30 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 260 seconds) |
| 10:13:32 | → | titibandit joins (~titibandi@user/titibandit) |
| 10:20:10 | × | vgtw quits (~vgtw@user/vgtw) (Server closed connection) |
| 10:20:33 | → | vgtw joins (~vgtw@user/vgtw) |
| 10:20:50 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Remote host closed the connection) |
| 10:25:59 | × | Inst quits (~Inst@2601:6c4:4081:2fc0:4f54:13aa:bf33:bb41) (Ping timeout: 240 seconds) |
| 10:26:07 | → | chromoblob joins (~user@37.113.180.121) |
| 10:27:55 | → | Inst joins (~Inst@c-76-101-10-131.hsd1.fl.comcast.net) |
| 10:31:48 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Remote host closed the connection) |
| 10:35:46 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 10:36:03 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 10:37:48 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 10:44:02 | <jackdk> | What name would you give this function? `Functor e => (forall x. f x -> e (g x)) -> Coyoneda f a -> e (Coyoneda g a)` |
| 10:44:22 | <jackdk> | It's like a `traversish` analogue of `hoist` |
| 10:48:57 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 10:49:54 | → | ubert joins (~Thunderbi@p200300ecdf0da912f884ed912556b966.dip0.t-ipconnect.de) |
| 10:50:30 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (Server closed connection) |
| 10:50:31 | → | michalz joins (~michalz@185.246.207.217) |
| 10:50:49 | × | michalz quits (~michalz@185.246.207.217) (Remote host closed the connection) |
| 10:54:33 | <ncf> | hoistFCoyoneda? |
| 10:56:43 | <probie> | Can we directly go `Functor e => Coyoneda (e g) a -> e (Coyoneda g a)`? |
| 10:57:00 | <probie> | s/(e g)/(Compose e g)/ |
| 10:59:14 | <probie> | `\(Coyenda f (Compose x)) -> fmap (Coyoneda f) x` |
| 11:00:20 | <probie> | I think that function should get a name, and then it's really just `thatFunction . hoist` |
| 11:00:59 | <ncf> | still have to insert Compose and getCompose in the middle |
| 11:01:02 | × | AlexNoo quits (~AlexNoo@178.34.163.88) (Read error: Connection reset by peer) |
| 11:01:25 | → | AlexNoo joins (~AlexNoo@178.34.163.88) |
| 11:01:43 | <ncf> | well, hoist (Compose . f) or something |
| 11:03:33 | <probie> | To match `Functor e => (forall x. f x -> e (g x)) -> Coyoneda f a -> e (Coyoneda g a)`, sure. But this is conceptually just a regular hoist, followed by lowering the coyoneda one layer |
| 11:10:12 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:10:22 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 11:10:31 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 11:13:44 | → | __monty__ joins (~toonn@user/toonn) |
| 11:17:17 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 11:21:19 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 11:21:25 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
| 11:21:35 | → | titibandit joins (~titibandi@user/titibandit) |
| 11:23:25 | → | Techcable joins (~Techcable@user/Techcable) |
| 11:25:32 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Ping timeout: 240 seconds) |
| 11:25:32 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 11:26:46 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 11:29:19 | → | titibandit joins (~titibandi@user/titibandit) |
| 11:33:39 | × | astra quits (sid289983@id-289983.hampstead.irccloud.com) (Server closed connection) |
| 11:34:20 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 240 seconds) |
| 11:34:27 | → | astra joins (sid289983@2a03:5180:f:4::4:6cbf) |
| 11:34:29 | → | titibandit joins (~titibandi@user/titibandit) |
| 11:36:10 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 11:38:40 | × | acidjnk quits (~acidjnk@p5dd870a3.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 11:40:29 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 11:41:22 | → | bontaq joins (~user@ool-45779b84.dyn.optonline.net) |
| 11:56:43 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 11:58:59 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 11:59:55 | × | takuan quits (~takuan@178.116.218.225) (Remote host closed the connection) |
| 12:02:56 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds) |
| 12:03:34 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 12:04:39 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 12:12:39 | × | sa1 quits (sid7690@id-7690.ilkley.irccloud.com) (Server closed connection) |
| 12:12:52 | → | sa1 joins (sid7690@id-7690.ilkley.irccloud.com) |
| 12:12:53 | × | alexherbo2 quits (~alexherbo@2a02-842a-8180-4601-e9ea-f8a5-e557-b41f.rev.sfr.net) (Remote host closed the connection) |
| 12:13:52 | × | jonathan_ quits (~jonathan@83.252.3.92) (Ping timeout: 240 seconds) |
| 12:17:10 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 12:20:17 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 265 seconds) |
| 12:22:03 | → | titibandit joins (~titibandi@user/titibandit) |
| 12:30:40 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 12:35:27 | × | thaumavorio quits (~thaumavor@thaumavor.io) (Server closed connection) |
| 12:37:44 | → | thaumavorio joins (~thaumavor@162.243.123.105) |
| 12:40:25 | × | gurkenglas quits (~user@dynamic-046-114-182-229.46.114.pool.telefonica.de) (Ping timeout: 240 seconds) |
| 12:40:59 | <ddrone[m]> | Is there a way to print out parse tree of a Haskell module as parsed by GHC to see its internal AST structure? |
| 12:41:10 | <ddrone[m]> | I have ParsedModule as returned by this function https://hackage.haskell.org/package/ghc-exactprint-1.7.0.1/docs/Language-Haskell-GHC-ExactPrint-Parsers.html#v:parseModule |
| 12:41:47 | <ddrone[m]> | But the problem there's no Show instance, and using ppr prints out rendered syntax |
| 12:43:50 | × | coot quits (~coot@89.69.206.216) (Quit: coot) |
| 12:44:58 | → | coot joins (~coot@89.69.206.216) |
| 12:45:18 | <[exa]> | ddrone[m]: is there no --ddump-... option ? |
| 12:45:48 | <[exa]> | ah so it's hiding it via ppr |
| 12:46:42 | <[exa]> | if there's a Generic instance on the stuff, you might have luck with the generic printing libs around |
| 12:47:52 | → | gurkenglas joins (~user@46.114.182.229) |
| 12:49:44 | <jackdk> | probie: like `lowerCoyonedaC :: Functor f => Coyoneda (Compose f g) a -> f (Coyoneda g a)`? |
| 12:50:40 | <geekosaur> | ddrone[m], check for an Outputtable instance iirc |
| 12:51:21 | <ddrone[m]> | <[exa]> "ddrone: is there no --ddump..." <- Oh didn't think, turns out `-ddump-parsed-ast` works, thanks! |
| 12:51:38 | → | ijqq joins (uid603979@id-603979.helmsley.irccloud.com) |
| 12:51:56 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 12:53:20 | <ddrone[m]> | FTR https://hackage.haskell.org/package/ghc-9.6.1/docs/GHC-Hs-Dump.html#v:showAstData that's the function -ddump-parsed-ast uses |
| 12:55:43 | × | fendor quits (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) (Remote host closed the connection) |
| 12:58:16 | <[exa]> | ah ok good nice. :D |
| 13:02:26 | <ddrone[m]> | Unfortunately looking at parse trees is not as enlightening as I thought it would be |
| 13:02:49 | <ddrone[m]> | Any chance someone can point me to usages of ghc-exactprint source transformations? |
| 13:03:25 | <ddrone[m]> | The only codebase I've looked so far to get the sense of it is HLS, looking for more examples |
| 13:06:48 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 13:11:17 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 258 seconds) |
| 13:14:03 | → | mcglk joins (~mcglk@131.191.19.145) |
| 13:16:07 | → | jonathan_ joins (~jonathan@c83-252-3-92.bredband.tele2.se) |
| 13:23:03 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 13:23:12 | <ijqq> | hi [Leary], I just saw your message. I'm sorry I don't exactly follow what you mean by `char '"' *> (fmap _ . many) (isMany _ <|> escape) <* char '"'`. I tried the first _ as concat and the second _ as (/= '\\'). So I thought it would be parse many times either something that isn't an escape or an escape char, and then concat those all together to form a string. But now it just hangs on the input. Would you be able to explain a bit |
| 13:23:12 | <ijqq> | more please? |
| 13:23:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:27:08 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Ping timeout: 240 seconds) |
| 13:35:00 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 13:35:44 | → | tomku joins (~tomku@user/tomku) |
| 13:37:10 | <ncf> | i think many (many x) will always hang, since the inner parser can succeed with an empty list indefinitely? |
| 13:37:20 | <ncf> | you probably want the inner parser to be non-nullable |
| 13:37:58 | <ncf> | (i'm not sure what isMany is) |
| 13:44:42 | <ijqq> | ah okay. http://sprunge.us/aPE1T6 this is the code. yep I changed isMany to isSome and it now doesn't hang, the code is now `str = char '"' *> (fmap concat . many) (isSome (\x -> x /= '\\' && x /= '"') <|> escape) <* char '"'` (though it still doesn't parse escapes correctly) . i think i'm on the right track now, thank you. So the second bracketed expression is the inner parser right? And the fmap is just getting as many of those as |
| 13:44:42 | <ijqq> | possible. |
| 13:46:11 | <ijqq> | I think the <* char '"' at the end needs to be replaced with something that checks for a preceding backslash maybe |
| 13:47:03 | <ncf> | escape should handle that |
| 13:47:21 | <ncf> | on the other hand you probably want isSome to also reject " |
| 13:47:53 | <ncf> | otherwise "a"b" might be accepted |
| 13:49:46 | <ijqq> | i thought that isSome (\x -> x /= '\\' && x /= '"') handles that? |
| 13:49:55 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 13:50:04 | → | Midjak joins (~Midjak@82.66.147.146) |
| 13:50:26 | <ncf> | well yes, but that's not what's in your last paste |
| 13:50:43 | <ncf> | oh, next line |
| 13:51:51 | <ijqq> | oh yep sorry my bad. although it still doesn't work haha |
| 13:52:15 | <ncf> | how so? |
| 13:53:30 | → | acidjnk joins (~acidjnk@2003:d6:e707:2f24:4af:8cce:d4f:7715) |
| 13:53:50 | × | jonathan_ quits (~jonathan@c83-252-3-92.bredband.tele2.se) (Ping timeout: 258 seconds) |
| 13:55:00 | <ijqq> | here are some examples http://sprunge.us/EP24JM |
| 13:55:18 | <ijqq> | so escape works but escaping a quote doesn't work |
| 14:00:08 | <ijqq> | oh I get it because of (\x -> x /= '\\' && x /= '"') |
| 14:00:16 | <ncf> | i don't see what's wrong here |
| 14:00:34 | <ncf> | remember you have to escape twice: once for ghci and once for your parser |
| 14:00:43 | <ncf> | so if you want to test whether \" is parsed correctly you need to use \\\" |
| 14:01:01 | <ijqq> | oh |
| 14:01:04 | <ijqq> | i see |
| 14:01:07 | <ijqq> | so it does work correctly |
| 14:01:22 | <ijqq> | oops |
| 14:02:00 | <ijqq> | well thank you very much for the help :) |
| 14:02:43 | <ncf> | (and, to test \n, you need \\n) |
| 14:03:13 | <ijqq> | ah cool |
| 14:03:31 | <ijqq> | now I need to just fix the case of empty string, as I changed the isMany to isSome to prevent it from hanging |
| 14:03:54 | <ncf> | you still have an outer many, so the empty string is still accepted |
| 14:04:10 | → | jonathan_ joins (~jonathan@83.252.3.92) |
| 14:04:29 | <ijqq> | oh oops, my bad with the escapes again |
| 14:05:22 | <ijqq> | it's actually quite cool this way. i didn't think to have an inner and outer parser |
| 14:05:43 | <ijqq> | you guys are smart haha |
| 14:16:33 | × | gurkenglas quits (~user@46.114.182.229) (Read error: Connection reset by peer) |
| 14:18:08 | × | TMA quits (tma@twin.jikos.cz) (Ping timeout: 248 seconds) |
| 14:18:08 | → | acidjnk_new joins (~acidjnk@p200300d6e7072f24519cabbd94a7f195.dip0.t-ipconnect.de) |
| 14:21:32 | × | acidjnk quits (~acidjnk@2003:d6:e707:2f24:4af:8cce:d4f:7715) (Ping timeout: 240 seconds) |
| 14:25:08 | → | rburkholder joins (~blurb@96.45.2.121) |
| 14:27:16 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 14:28:08 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:35:50 | × | acarrico quits (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net) (Server closed connection) |
| 14:36:13 | → | acarrico joins (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net) |
| 14:36:18 | → | dorin joins (~dorin@79.115.55.108) |
| 14:38:31 | → | ub joins (~Thunderbi@p200300ecdf0da9ac5cdf960cafa3cfa2.dip0.t-ipconnect.de) |
| 14:39:12 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 240 seconds) |
| 14:39:50 | × | ubert quits (~Thunderbi@p200300ecdf0da912f884ed912556b966.dip0.t-ipconnect.de) (Ping timeout: 258 seconds) |
| 14:39:50 | ub | is now known as ubert |
| 14:40:00 | → | o-90 joins (~o-90@gateway/tor-sasl/o-90) |
| 14:40:05 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 14:42:04 | <segfaultfizzbuzz> | so i think if i understand correctly, the mathematician's instruction set architecture is called a cartesian closed category? |
| 14:49:52 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 14:50:33 | × | T_S__ quits (sid501726@id-501726.uxbridge.irccloud.com) (Server closed connection) |
| 14:50:47 | → | T_S__ joins (sid501726@id-501726.uxbridge.irccloud.com) |
| 14:51:36 | <leah2> | if you dare call lambda calculus an isa, maybe |
| 14:51:57 | <segfaultfizzbuzz> | a mathematician's abstract computer, if you like |
| 14:52:09 | <segfaultfizzbuzz> | in other words, turing machines are not really useful imo |
| 14:55:19 | <leah2> | it depends what you wanna proof |
| 14:55:22 | <leah2> | prove* |
| 14:57:46 | × | o-90 quits (~o-90@gateway/tor-sasl/o-90) (Remote host closed the connection) |
| 14:58:33 | <segfaultfizzbuzz> | i am looking at the definition of the CCC on wikipedia and it requires a product and exponential... intuitively i have difficulty seeing the distinction between product and exponential as they are both binary operators |
| 15:00:12 | × | agander_m quits (sid407952@id-407952.tinside.irccloud.com) (Server closed connection) |
| 15:00:17 | × | tomku quits (~tomku@user/tomku) (Read error: Connection reset by peer) |
| 15:00:21 | → | agander_m joins (sid407952@id-407952.tinside.irccloud.com) |
| 15:00:52 | <ncf> | product is (,), exponential is (->) |
| 15:01:20 | <segfaultfizzbuzz> | sure but what distinguishes (,) from (->) |
| 15:02:37 | <ncf> | well surely you agree that (a, b) and a -> b are different types (and that they ought to be) |
| 15:02:57 | <ncf> | (in general; they might happen to be isomorphic in a few cases) |
| 15:03:06 | <segfaultfizzbuzz> | my best intuition here would be to focus on the cardinality, and to say that the cardinaility of (X,Y) translates to "count the pair X and Y", the cardinality of (->) translates to "count all functions from X to Y" |
| 15:03:29 | <segfaultfizzbuzz> | and so (,) refers to the "endpoints" whereas (->) refers to the all paths between the endpoints |
| 15:03:43 | <segfaultfizzbuzz> | and then the function implementation would be a specific path between endpoints |
| 15:05:55 | → | tomku joins (~tomku@user/tomku) |
| 15:07:08 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 15:10:30 | × | Teacup quits (~teacup@user/teacup) (Server closed connection) |
| 15:11:09 | → | Teacup joins (~teacup@user/teacup) |
| 15:12:40 | → | zer0bitz_ joins (~zer0bitz@user/zer0bitz) |
| 15:13:31 | × | zer0bitz quits (~zer0bitz@user/zer0bitz) (Ping timeout: 240 seconds) |
| 15:20:45 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 240 seconds) |
| 15:22:29 | → | josias joins (~mottmatri@2001:470:69fc:105::b6c) |
| 15:23:19 | × | tired quits (~tired@user/tired) (Server closed connection) |
| 15:23:41 | → | tired joins (~tired@user/tired) |
| 15:24:09 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 15:24:23 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 15:28:29 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Ping timeout: 240 seconds) |
| 15:33:33 | → | TMA joins (tma@91.219.245.39) |
| 15:39:29 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 15:39:42 | <tomsmeding> | when do we have a * b == b^a ? :p |
| 15:40:17 | <tomsmeding> | e.g. if a == b == 2, i.e. (Bool, Bool) ~= (Bool -> Bool) |
| 15:40:36 | <tomsmeding> | at least as sets -- same cardinality. Isomorphism as objects in the CCC, perhaps not |
| 15:41:32 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 240 seconds) |
| 15:41:56 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 258 seconds) |
| 15:42:11 | × | nehsou^ quits (~nehsou@c-71-204-38-59.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 15:42:48 | × | Inst quits (~Inst@c-76-101-10-131.hsd1.fl.comcast.net) (Ping timeout: 252 seconds) |
| 15:43:11 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:47:59 | → | user__ joins (~user@dynamic-046-114-182-229.46.114.pool.telefonica.de) |
| 15:50:01 | <ncf> | i think it works in a CCC, if by Bool you mean the coproduct of two terminal objects |
| 15:50:13 | <ncf> | haven't checked too carefully |
| 15:51:05 | × | dorin quits (~dorin@79.115.55.108) (Ping timeout: 246 seconds) |
| 15:51:44 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds) |
| 15:52:10 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 15:53:41 | → | tomku joins (~tomku@user/tomku) |
| 15:58:29 | → | ddellacosta joins (~ddellacos@143.244.47.89) |
| 16:01:08 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 252 seconds) |
| 16:01:18 | × | tom_ quits (~tom@2a00:23c8:970c:4801:5b6a:e81b:79dc:f684) (Read error: Connection reset by peer) |
| 16:01:47 | → | dsrt^ joins (~dsrt@c-71-204-38-59.hsd1.ga.comcast.net) |
| 16:01:57 | → | tom_ joins (~tom@2a00:23c8:970c:4801:5b6a:e81b:79dc:f684) |
| 16:03:22 | → | tomku joins (~tomku@user/tomku) |
| 16:04:20 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 240 seconds) |
| 16:10:23 | × | driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 16:10:39 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 16:11:07 | → | driib joins (~driib@176.57.184.141) |
| 16:13:10 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 16:16:45 | × | driib quits (~driib@176.57.184.141) (Read error: Connection reset by peer) |
| 16:17:06 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:19:50 | × | bontaq quits (~user@ool-45779b84.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 16:21:22 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 16:23:23 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 16:23:40 | → | chromoblob joins (~user@37.113.180.121) |
| 16:25:09 | <segfaultfizzbuzz> | but wait, b^a, which if i understand correctly is b -> a, which translates to "all functions from b to a" includes all noninvertible functions from b to a |
| 16:25:22 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 16:25:27 | <segfaultfizzbuzz> | but if a and b are Bool then a*b is always invertible |
| 16:26:30 | <segfaultfizzbuzz> | and furthermore b^a does not in general include the same functions as a^b due to the inclusion of noninvertible functions |
| 16:26:49 | <ncf> | b^a is a -> b |
| 16:27:08 | <segfaultfizzbuzz> | ok then apply that patch to the last few lines ;) |
| 16:27:39 | <ncf> | what does it mean for a*b to be invertible? |
| 16:27:54 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 16:28:48 | <segfaultfizzbuzz> | like in the sense of a group, so there would be an inverse b^-1 |
| 16:29:00 | <segfaultfizzbuzz> | so that a*b*b^-1 = a*(b*b^-1) = a |
| 16:29:00 | <ncf> | but a*b is not a type of functions... |
| 16:29:09 | <[exa]> | segfaultfizzbuzz: how come bool functions are all invertible? |
| 16:29:17 | <ncf> | the noninvertible functions Bool -> Bool correspond to the pairs (a, b) : (Bool, Bool) with a /= b (at least if you're using the "obvious" isomorphism) |
| 16:29:23 | <segfaultfizzbuzz> | ah wait they aren't, i can have 0 lol |
| 16:29:29 | <segfaultfizzbuzz> | b = 0, nvm lol |
| 16:30:08 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 16:30:25 | <ncf> | er sorry, with a == b |
| 16:30:35 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:30:47 | <segfaultfizzbuzz> | but if a and b were nonzero rationals you could have the inclusion of the multiplicative inverses |
| 16:43:09 | <segfaultfizzbuzz> | that is to say, if the type of a and b is nonzero rationals, then a*b always has an inverse for any b, but a -> b can include noninvertible functions,... |
| 16:43:39 | → | toastloop joins (~toastloop@user/toastloop) |
| 16:43:47 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 16:43:47 | <segfaultfizzbuzz> | but perhaps that is boring |
| 16:44:08 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:44:32 | <ncf> | this does not make any sense |
| 16:44:50 | <ncf> | what is a -> b, if a and b are rational numbers? |
| 16:44:56 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 16:45:26 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 16:45:40 | <segfaultfizzbuzz> | that would be a function from a to b, where a and b are nonzero rational numbers |
| 16:46:34 | <segfaultfizzbuzz> | for example if f : a -> b then f x = (-1) * x would qualify, as would g x = (1/3) * x |
| 16:46:49 | <segfaultfizzbuzz> | excuse me, g : a -> b there as well |
| 16:48:02 | <ncf> | do you mean a function f : ℚ* → ℚ* such that f(a) = b? why would those qualify, if we know nothing about a and b? |
| 16:48:17 | <segfaultfizzbuzz> | those would happen to be invertible functions ... but h x = 1 where h : a -> b also is a function h mapping rationals to rationals, and h in this case is noninvertible |
| 16:48:49 | <segfaultfizzbuzz> | correct f : ℚ* → ℚ* |
| 16:49:22 | <ncf> | and your point is? |
| 16:49:23 | <segfaultfizzbuzz> | ah here a and b were both ℚ* |
| 16:49:40 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:49:57 | <segfaultfizzbuzz> | my point is that multiplication can sometimes mandate invertibility depending on what it acts on, whereas functions never mandate invertibility |
| 16:52:30 | <ncf> | but we were talking about products of types (in the categorical sense), not multiplication of rational numbers |
| 16:53:37 | <segfaultfizzbuzz> | yes and the distinction between product and exponentiation |
| 16:55:32 | <ncf> | you might as well ask about the distinction between apples and cars |
| 16:55:41 | <segfaultfizzbuzz> | and so i am saying that one distinction is that depending on the underlying type, products can require invertibility whereas exponentiation always includes noninvertible |
| 16:56:02 | <segfaultfizzbuzz> | well product and exponentiation are both binary operators so the distinction is not obvious |
| 16:57:23 | <ncf> | you might as well say that apples and cars are both physical objects so the distinction is not obvious |
| 16:57:39 | <ncf> | still no idea what "products can require invertibility" is supposed to mean |
| 16:58:10 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 16:58:32 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 16:58:46 | <segfaultfizzbuzz> | ncf: i mean sure if you are talking about massive point particles from very far away, there is really only the mass to worry about |
| 16:59:37 | <segfaultfizzbuzz> | let p : ℚ* → ℚ* and let e : ℚ* → ℚ* where p is a product and e is an exponentiation |
| 16:59:46 | <segfaultfizzbuzz> | p must be invertible whereas e may be noninvertible |
| 16:59:59 | <segfaultfizzbuzz> | therefore p and e are not the same |
| 17:01:04 | <tomsmeding> | products are not functions |
| 17:01:43 | <segfaultfizzbuzz> | oh wow really? |
| 17:01:51 | <tomsmeding> | a product a * b can be modelled in type theory as a dependent function (b : Bool) -> (case b of false -> a ; true -> b) |
| 17:01:51 | <tomsmeding> | :p |
| 17:01:55 | <tomsmeding> | in _that_ sense it might be a function |
| 17:02:22 | <tomsmeding> | your saying "let p : ℚ* → ℚ* where p is a product" makes little sense to me |
| 17:02:46 | <segfaultfizzbuzz> | well... i suppose p is uniquely defined in that case? |
| 17:02:57 | <tomsmeding> | like, p is a product -- of which two things? |
| 17:03:10 | <tomsmeding> | (or of which collection of things, if you want n-ary products) |
| 17:03:14 | × | ysh____ quits (sid6017@id-6017.ilkley.irccloud.com) (Server closed connection) |
| 17:03:22 | <tomsmeding> | product of ℚ* and ℚ*? Or something else? |
| 17:03:25 | → | ysh____ joins (sid6017@id-6017.ilkley.irccloud.com) |
| 17:03:34 | <segfaultfizzbuzz> | ah right let me fix the definitions: p : ℚ* → ℚ* → ℚ* and e : ℚ* → ℚ* → ℚ* |
| 17:04:05 | <tomsmeding> | okay so p is multiplication in ℚ* and e is exponentiation in ℚ* |
| 17:04:34 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 17:04:48 | <segfaultfizzbuzz> | p is probably unique (?) but e may not be, although p might be nonunique up to something like inversion 1/x and negation -x |
| 17:05:14 | <tomsmeding> | in what sense is ℚ* a category? |
| 17:05:26 | <tomsmeding> | because if it isn't, we're not talking about the same kind of product in the first place |
| 17:05:35 | <segfaultfizzbuzz> | ℚ* is a ... type? |
| 17:05:38 | <tomsmeding> | yeah |
| 17:05:45 | <segfaultfizzbuzz> | or maybe a set? if you want? |
| 17:05:54 | <segfaultfizzbuzz> | a type is a category? probably? |
| 17:05:55 | <tomsmeding> | a product operation is a thing that a _category_ might have |
| 17:06:07 | <tomsmeding> | if you want a product on ℚ*, ℚ* first has to be a category |
| 17:06:27 | <tomsmeding> | and I believe it isn't a category in a relevant way |
| 17:07:17 | <tomsmeding> | Haskell types form a category (kind of... details), where the types are the objects and functions are the morphisms |
| 17:07:29 | <tomsmeding> | and the haskell pair type is the product in that category |
| 17:07:53 | <tomsmeding> | in Set, the product is the cartesian product of sets |
| 17:08:15 | × | dtman34_ quits (~dtman34@2601:447:d000:93c9:49a3:2ee1:9e07:c081) (Ping timeout: 260 seconds) |
| 17:08:32 | <tomsmeding> | the only link with multiplication of numbers that I know (though I know very little of CT, so YMMV) is that in Set, the cardinalities multiply |
| 17:08:44 | <tomsmeding> | and this cardinality situation is quite common; same holds in Hask |
| 17:09:13 | <tomsmeding> | segfaultfizzbuzz: "a type is a category?" -- a category has objects and morphisms, what are the objects and the morphisms of ℚ*? ;) |
| 17:09:23 | <dolio> | It has related algebraic properties, too. |
| 17:09:34 | <segfaultfizzbuzz> | well ℚ* does define objects. ... so perhaps product is a method of counting morphisms where the value of b is the index, ... |
| 17:09:46 | <tomsmeding> | dolio: commutativity, associativity, distribution over sums/coproducts? |
| 17:09:57 | <dolio> | Yeah, stuff like that. |
| 17:10:14 | <tomsmeding> | segfaultfizzbuzz: sure, we could call the numbers of ℚ* its objects. But then what is the collection of morphisms from 4 to 7.6? |
| 17:10:28 | tomsmeding | has no clue |
| 17:10:49 | <tomsmeding> | only once you have a definition of a "morphism" in the category, can you even formulate what a categorical product _is_ |
| 17:11:03 | <segfaultfizzbuzz> | well there are at least two classes of morphisms of interest, the product and the exponentiation |
| 17:11:12 | <tomsmeding> | those are not of the right type |
| 17:11:16 | <ncf> | there are a couple choices you can make, but i'm not sure any of them give rise to a CCC |
| 17:11:38 | <tomsmeding> | segfaultfizzbuzz: the morphisms go from one object to another |
| 17:11:48 | <segfaultfizzbuzz> | both endpoints must be specified? |
| 17:12:01 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:12:36 | <tomsmeding> | like in Set, a morphism from A to B is a function from A to B; in Hask, similarly; in Rel (binary relations), objects are sets and a morphism from A to B is a subset of A x B (their cartesian product) |
| 17:12:37 | <segfaultfizzbuzz> | so the morphism cannot be a "nice" description of a function ... like if the morphism was SHA256 |
| 17:12:46 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:13:03 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 17:13:06 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:13:10 | <segfaultfizzbuzz> | you cannot describe morphisms in many useful cases because it is unrealistic to enumerate both endpoints |
| 17:13:11 | <tomsmeding> | in other words, in Set, Hom(A, B) = {functions from A to B}, and similarly for the others -- Hom(A, B) is notation for the set of morphisms from A to B in a category |
| 17:13:16 | <tomsmeding> | what is Hom(4, 7.6)? |
| 17:13:21 | <segfaultfizzbuzz> | whereas it is substantially always realistic to enumerate the "inputs" to the function |
| 17:13:28 | <tomsmeding> | it's gotta be a set of _things_ |
| 17:13:31 | <tomsmeding> | not necessarily functions |
| 17:13:41 | <monochrom> | To muddle the discussion, recall that the standard way to cast a group as a category is that the category has only one object of no content itself, the content is that group elements are endomorphisms over that object of no content. |
| 17:13:56 | <tomsmeding> | and there has to be some sense of combination of an element of Hom(A, B) and an element of Hom(B, C) to an element of Hom(A, C) |
| 17:14:32 | <tomsmeding> | monochrom: does the resulting single-object category have a product? (honest question) |
| 17:14:42 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:14:57 | tomsmeding | guesses no |
| 17:15:28 | <tomsmeding> | but anyway it would be a category that looks completely different from what segfaultfizzbuzz is, I think, envisioning |
| 17:15:32 | <monochrom> | But let's muddle the discussion even more! The standard way to cast a partially-ordered set as a category is that elements are objects, morphisms happen (uniquely) iff x<=y using the partial order. |
| 17:15:45 | <monochrom> | I don't know. Haven't thought of that. |
| 17:15:53 | <tomsmeding> | hm that'd be closer |
| 17:16:16 | <dolio> | Product in a partial order is max, though. |
| 17:16:29 | <monochrom> | Using the partial order idea, Hom(4, 7.6) is a singleton set of no content other than the fact that it is a singleton set. :) |
| 17:16:41 | <tomsmeding> | dolio: min, right? |
| 17:16:53 | <ncf> | for a group G to have categorical products, you'd need the single object to be the product of itself and itself, which means that a map * → * is equivalent to two maps * → * |
| 17:17:11 | <ncf> | so, you need an iso G ≃ G × G i guess |
| 17:17:42 | <ncf> | (does it have to be a group isomorphism, or merely sets?) |
| 17:18:07 | <dolio> | Oh, yeah. |
| 17:18:31 | × | bradparker quits (sid262931@id-262931.uxbridge.irccloud.com) (Server closed connection) |
| 17:18:40 | → | bradparker joins (sid262931@id-262931.uxbridge.irccloud.com) |
| 17:21:20 | <tomsmeding> | ncf: reading the universal property of a product on nlab, it sounds to me like * is the product of * and * if there are two morphisms p1,p2 : * -> *, such that for any two morphisms f1,f2 : * -> *, there is a unique morphism h : * -> * such that pi ∘ h = fi |
| 17:22:31 | → | danza joins (~francesco@151.44.185.43) |
| 17:23:08 | <monochrom> | Choose p1 = p2 = the identity element of the group. >:) |
| 17:23:17 | <tomsmeding> | i.e. in the group: ∃p1,p2. ∀f1,f2. ∃h. (p1 h = f1) & (p2 h = f2); thus p2^{-1} f2 = h = p1^{-1} f1, thus f2 = p2 p1^{-1} f1 |
| 17:23:18 | → | wroathe joins (~wroathe@50.205.197.50) |
| 17:23:18 | × | wroathe quits (~wroathe@50.205.197.50) (Changing host) |
| 17:23:18 | → | wroathe joins (~wroathe@user/wroathe) |
| 17:23:34 | <tomsmeding> | so f2 is determined by f1, so there can only be one element in the group? |
| 17:23:52 | <tomsmeding> | surely if there is more than one element, one can choose f2 so that it doesn't satisfy the relation |
| 17:24:02 | <tomsmeding> | making * not the product of * and * |
| 17:24:04 | <monochrom> | Err right oops. |
| 17:24:13 | <tomsmeding> | have I gotten this right? |
| 17:24:19 | <tomsmeding> | that would be surprising |
| 17:24:21 | × | danza quits (~francesco@151.44.185.43) (Client Quit) |
| 17:24:23 | <ncf> | yeah sounds like it |
| 17:24:23 | <monochrom> | Yeah you're right. |
| 17:24:31 | tomsmeding | is bludgeoning through stuff I kinda understand |
| 17:25:02 | <monochrom> | Letting the symbols do the work is the best kind of understanding. >:D |
| 17:25:11 | <tomsmeding> | so does it have a product? Well only if the group is the trivial group :p |
| 17:25:11 | <tomsmeding> | yes |
| 17:25:17 | <monochrom> | SYMBOLS DON'T LIE |
| 17:25:32 | <tomsmeding> | not when the number of symbols and laws to check is this low |
| 17:26:00 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:26:18 | <tomsmeding> | this was good practice for me |
| 17:26:19 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:26:27 | <monochrom> | OK that was an exaggeration. I have seen philosopher-wannabes use symbols to lie. |
| 17:26:36 | monochrom | is looking at Euler |
| 17:27:01 | <int-e> | that's not the symbols' fault |
| 17:27:06 | <segfaultfizzbuzz> | so then does this connect to my original question: what is the difference between product and exponential ? |
| 17:27:30 | <segfaultfizzbuzz> | in light of the fact that both are binary operators |
| 17:27:50 | <int-e> | are we really doing syntax and semantics |
| 17:27:59 | <ncf> | i have no idea what we're doing |
| 17:28:15 | <ncf> | looking for a difference between two things that is not covered by "they are not the same thing, clearly" |
| 17:28:17 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:28:25 | <geekosaur> | wasn't that question like the first thing answered? |
| 17:28:39 | <monochrom> | Oh that reminds me of on Friday at school we had a discussion on being anal and pedantic about the definition of "binary operator". |
| 17:28:44 | <geekosaur> | if that answer didn't satisfy you then you're doing philosophy, not math |
| 17:28:44 | × | smoge quits (~smoge@2603-7000-4b42-1100-9dab-c33e-5e93-2285.res6.spectrum.com) (Ping timeout: 246 seconds) |
| 17:29:04 | <dolio> | Why would all binary operators be the same? |
| 17:29:08 | <ncf> | that must be why i can't make sense of this conversation 🙃 |
| 17:29:29 | <monochrom> | As it turns out, if you are to be pedantic, foo::AxB->C qualifies as a binary operator iff A=C or B=C. |
| 17:29:31 | <segfaultfizzbuzz> | well only the input values can index the output of the binary operator... |
| 17:29:39 | <tomsmeding> | segfaultfizzbuzz: they are both binary operators, but they have to satisfy different laws |
| 17:29:51 | <monochrom> | And to some people, even more strongly A=B=C. |
| 17:30:16 | <dolio> | I mean, people have been talking a lot about numbers. Do you have this confusion with numbers? |
| 17:30:24 | <dolio> | 2*3 = 6, 2^3 = 8. |
| 17:30:27 | <int-e> | monochrom: scalar products have A = B != C. |
| 17:30:29 | × | cheater quits (~Username@user/cheater) (Ping timeout: 240 seconds) |
| 17:30:34 | <monochrom> | We had that discussion because in standard linear algebra definitions it's said "blah blah binary operator blah blah" and the student decided to really ask what does "binary operator" mean. |
| 17:30:49 | <dolio> | 2+3 = 5 |
| 17:31:33 | <int-e> | And I guess if you are detailed about matrix products, that'll give you an example where all three sets are usually distinct... oh and the operator is heavily overloaded. |
| 17:31:48 | <dolio> | 2|3 = 3, 2&3 = 2 |
| 17:32:37 | <tomsmeding> | all binary operators, but all have different properties |
| 17:32:41 | <monochrom> | Eventually I said "forget it, if it's infix it's a binary operator, yes it's just syntax" |
| 17:32:57 | <tomsmeding> | monochrom: that's what programming languages do :p |
| 17:33:05 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 240 seconds) |
| 17:33:51 | <monochrom> | But the student did look for "binary operator/ion" on Wikipedia and it's a whole rabbit hole. |
| 17:34:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:37:23 | monochrom | prefers 2+2=4, 2*2=4, 2^2=4 >:D |
| 17:37:49 | × | nshepperd2 quits (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) (Server closed connection) |
| 17:38:05 | → | nshepperd2 joins (nshepperd@2600:3c03::f03c:92ff:fe28:92c9) |
| 17:39:25 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:39:48 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 17:40:08 | × | user__ quits (~user@dynamic-046-114-182-229.46.114.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 17:41:38 | <int-e> | monochrom: tune in for the next episode when we learn about monads |
| 17:42:07 | <monochrom> | :( |
| 17:42:22 | <monochrom> | OK no worries, :) |
| 17:42:42 | <int-e> | (I'll admit that "monad" is quite a bit more specific than "binary operator") |
| 17:42:56 | <monochrom> | Oh haha |
| 17:43:02 | <tomsmeding> | similarly, in the ring {0}, where (+), (*), (|) and (&) are all the same thing! |
| 17:43:07 | monochrom | hugs his monadic second-order logic |
| 17:43:11 | <tomsmeding> | (not sure what to do with (^)) |
| 17:43:22 | <ncf> | laser eyes Leibniz |
| 17:43:31 | <monochrom> | I think 0^0 = 1 = 0 still works. |
| 17:43:45 | <tomsmeding> | surely there is some law that breaks |
| 17:43:49 | <tomsmeding> | what laws does ^ even have |
| 17:43:59 | <tomsmeding> | or is this the lawless wild west |
| 17:44:07 | <segfaultfizzbuzz> | i'm not sure whether i'm being mocked here,... my difficulty understanding the distinctions between binary operators stems from the fact that the outputs of the binary operator functions can be indexed by the inputs (specifically the cartesian product of the inputs) |
| 17:44:30 | <tomsmeding> | segfaultfizzbuzz: you are not being mocked, but we're having trouble formulating the answer in a way that makes sense to you |
| 17:44:36 | <monochrom> | x^0 = 1, x^(n+1)= x * x^n. But recall 1=0. "This is fine." |
| 17:45:05 | <int-e> | x^(a+b) = x^a * x^b |
| 17:45:28 | <segfaultfizzbuzz> | put another way: "my binary operator LUT is better than your binary LUT" |
| 17:45:37 | <int-e> | (preconditions omitted) |
| 17:45:44 | <tomsmeding> | segfaultfizzbuzz: did you one of my later messages? (+) and (*) are both binary operators, but we expect them to behave differently (i.e. they have different laws), and some of those laws explicitly involve both. For example, a*(b+c) = a*b + a*c |
| 17:45:48 | <tomsmeding> | similarly for (,) and (->) |
| 17:46:07 | → | user__ joins (~user@46.114.182.229) |
| 17:46:19 | → | Inst joins (~Inst@2601:6c4:4081:2fc0:add4:91ad:5330:1cfd) |
| 17:46:31 | <segfaultfizzbuzz> | oh is there a distribution law for (,) and (->) ? |
| 17:46:32 | <tomsmeding> | we expect the product to be associative, i.e. (a x b) x c should be isomorphic to a x (b x c) |
| 17:46:48 | <tomsmeding> | but we don't expect (a -> b) -> c ~= a -> (b -> c) |
| 17:46:56 | <segfaultfizzbuzz> | ah hmm |
| 17:47:15 | <tomsmeding> | on the other hand, we do expect a -> (b -> c) ~= (a, b) -> c |
| 17:47:24 | <tomsmeding> | err, (a x b) -> c; I need to be consistent with notation |
| 17:47:28 | <tomsmeding> | that's called currying |
| 17:47:38 | <tomsmeding> | and it's the eta-law of categorical exponentials |
| 17:47:43 | <tomsmeding> | there are more laws |
| 17:47:49 | × | pat67 quits (~pat67@145.14.135.137) (Quit: Leaving) |
| 17:48:06 | <tomsmeding> | not quite distribution, but it _is_ a law that connects both |
| 17:48:11 | <tomsmeding> | in a cartesian closed category, that is |
| 17:49:54 | <tomsmeding> | hm, perhaps this is even the only law (outside from (x) being a categorical product, that is) |
| 17:50:30 | <tomsmeding> | meh, no, some naturality conditions |
| 17:50:32 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 17:50:44 | <tomsmeding> | anyway segfaultfizzbuzz does this perspective from the laws make more sense to you? |
| 17:51:00 | <dolio> | It's a defining characteristic, but usually it satisfies other laws in specific scenarios. |
| 17:51:14 | → | driib joins (~driib@176.57.184.141) |
| 17:51:15 | <dolio> | Analogous to arithmetic. |
| 17:51:25 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 17:51:56 | tomsmeding | has to leave, thanks for the CT practice all |
| 17:52:33 | <monochrom> | :) |
| 17:53:32 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 240 seconds) |
| 17:55:27 | <dolio> | In categories, it's even easier to tell apart than in arithmetic, in some ways, because exponentials have a type like: C^op × C -> C. |
| 17:55:43 | <dolio> | Which means it flips the direction of arrows for one of its positions. |
| 17:55:43 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Ping timeout: 265 seconds) |
| 17:56:43 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 17:58:51 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:58:58 | <dolio> | So I suppose exponentials might not even fit a strict definition of "binary operator" on categories. |
| 17:59:37 | <dolio> | That's why reflexive graphs are so much better than categories. :þ |
| 18:01:04 | segfaultfizzbuzz | reads the logs btw |
| 18:02:03 | × | driib quits (~driib@176.57.184.141) (Read error: Connection reset by peer) |
| 18:02:25 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:02:27 | <ncf> | dolio: don't they also have a notion of opposite? |
| 18:02:43 | <dolio> | Who's "they"? |
| 18:03:01 | <dolio> | Oh, reflexive graphs? |
| 18:03:26 | <ncf> | yes |
| 18:03:56 | <ncf> | just flip all the edges |
| 18:04:22 | <segfaultfizzbuzz> | tomsmeding: regarding whether this makes sense, thanks for the effort here... i am trying to understand... |
| 18:04:23 | <dolio> | Yeah, you can take the opposite. But you don't need to to have a well defined exponential 'relator,' I think. |
| 18:07:18 | <segfaultfizzbuzz> | so another way to look at this is that you have n "arguments" to a function like so: f : a -> b -> c -> d -> ... -> z |
| 18:08:41 | <segfaultfizzbuzz> | and you can have constraints (or symmetries) on such functions |
| 18:08:44 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 18:08:56 | <segfaultfizzbuzz> | categories care about associativity for instance |
| 18:09:05 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:10:28 | <segfaultfizzbuzz> | umm i am having some difficulty articulating this in a nicely precise way |
| 18:10:38 | <segfaultfizzbuzz> | let me try again: |
| 18:11:09 | <segfaultfizzbuzz> | associativity, commutativity, invertability, etc might all be seen as enumerating some form of symmetry or identity on functions |
| 18:11:24 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 18:11:24 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 18:11:24 | finn_elija | is now known as FinnElija |
| 18:11:49 | × | gentauro quits (~gentauro@user/gentauro) (Ping timeout: 258 seconds) |
| 18:11:56 | <segfaultfizzbuzz> | is there a sensible completion of the set (associativity, commutativity, invertability, ...) |
| 18:12:18 | <Cale> | There's like... universal algebra |
| 18:12:43 | × | bjobjo quits (~bjobjo@user/bjobjo) (Quit: leaving) |
| 18:12:56 | <monochrom> | I'm a conservative, and I'll say no. |
| 18:14:27 | <Cale> | The result you get depends on how you abstract over those things |
| 18:15:35 | <Cale> | But they're all equational constraints with first order quantifiers, so you could say the set of all sentences in the first order language having a single binary operator |
| 18:16:15 | <Cale> | That's maybe more than you wanted |
| 18:16:23 | <segfaultfizzbuzz> | interesting, but you could go beyond binary...? |
| 18:16:45 | → | cheater joins (~Username@user/cheater) |
| 18:16:48 | → | dtman34 joins (~dtman34@c-76-156-89-180.hsd1.mn.comcast.net) |
| 18:16:51 | <segfaultfizzbuzz> | i failed to construct something but i was thinking one could maybe say something about a rotation or other permutation on n arguments |
| 18:17:14 | <Cale> | https://en.wikipedia.org/wiki/Model_theory |
| 18:17:30 | <Cale> | Would be a further generalization of that. |
| 18:18:23 | <segfaultfizzbuzz> | interesting |
| 18:18:36 | <Cale> | You can have arbitrary collections of n-ary relation and function symbols and then axioms written in terms of those and equality and logical connectives that need to be satisfied, and then interpret those as applying to some set together with suitable relations and functions on it |
| 18:18:57 | → | bjobjo joins (~bjobjo@user/bjobjo) |
| 18:19:33 | <Cale> | https://en.wikipedia.org/wiki/Universal_algebra also is perhaps a bit closer to what you were originally asking about |
| 18:19:55 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 18:20:30 | <Cale> | Universal algebra is a little more constrained, in that the axioms being discussed in that setting don't involve arbitrary logic, they're universally quantified equations. |
| 18:23:24 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 18:23:46 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:23:49 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 18:24:26 | <Cale> | and then you can go even further with generalizing these pictures, to many-sorted logics, or categorical semantics, where you don't just have one set that your quantifiers are ranging over |
| 18:28:39 | → | gentauro joins (~gentauro@user/gentauro) |
| 18:31:29 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 265 seconds) |
| 18:34:38 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 18:35:00 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:35:32 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 240 seconds) |
| 18:36:12 | → | cyphase joins (~cyphase@user/cyphase) |
| 18:36:29 | <segfaultfizzbuzz> | 🤯 |
| 18:39:04 | → | rf joins (~rf@2605:59c8:179c:f610:381a:41b2:b045:204d) |
| 18:42:39 | × | Ekho quits (~Ekho@user/ekho) (Server closed connection) |
| 18:42:40 | <segfaultfizzbuzz> | the jacobi identity might be something useful as an example of something nonobvious to include in the set (assoc, commut, invert, etc) |
| 18:44:03 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Quit: Lost terminal) |
| 18:47:14 | × | hamishmack quits (sid389057@id-389057.hampstead.irccloud.com) (Server closed connection) |
| 18:47:24 | → | hamishmack joins (sid389057@id-389057.hampstead.irccloud.com) |
| 18:48:38 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 18:48:39 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 18:48:58 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 18:51:10 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 18:54:23 | → | Ekho joins (~Ekho@user/ekho) |
| 18:55:54 | → | Pickchea joins (~private@user/pickchea) |
| 18:55:54 | × | dmj` quits (sid72307@id-72307.hampstead.irccloud.com) (Server closed connection) |
| 18:56:23 | → | dmj` joins (sid72307@id-72307.hampstead.irccloud.com) |
| 18:58:36 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 18:59:39 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Remote host closed the connection) |
| 19:00:27 | <segfaultfizzbuzz> | thx for the math bbl |
| 19:00:28 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
| 19:02:30 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 19:04:42 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:05:02 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:07:24 | × | dtman34 quits (~dtman34@c-76-156-89-180.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 19:12:37 | → | dtman34 joins (~dtman34@2601:447:d000:93c9:49a3:2ee1:9e07:c081) |
| 19:14:17 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:14:50 | × | Inst quits (~Inst@2601:6c4:4081:2fc0:add4:91ad:5330:1cfd) (Ping timeout: 260 seconds) |
| 19:18:23 | → | Inst joins (~Inst@2601:6c4:4081:2fc0:c22:b297:94d:820e) |
| 19:18:41 | × | Inst quits (~Inst@2601:6c4:4081:2fc0:c22:b297:94d:820e) (Read error: Connection reset by peer) |
| 19:18:44 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:19:05 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:28:06 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 19:28:26 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:34:09 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 19:34:51 | → | driib joins (~driib@176.57.184.141) |
| 19:35:14 | × | Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Remote host closed the connection) |
| 19:37:58 | → | Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 19:43:30 | → | fendor joins (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) |
| 19:46:40 | × | driib quits (~driib@176.57.184.141) (Remote host closed the connection) |
| 19:47:00 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 19:50:03 | → | mechap joins (~mechap@user/mechap) |
| 19:51:28 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 19:53:22 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:54:27 | → | bontaq joins (~user@ool-45779b84.dyn.optonline.net) |
| 19:59:41 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 19:59:49 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 20:00:12 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:02:51 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 20:05:14 | → | biberu joins (~biberu@user/biberu) |
| 20:06:05 | → | michalz joins (~michalz@185.246.207.201) |
| 20:08:21 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 258 seconds) |
| 20:11:16 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:11:36 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:22:12 | × | jero98772 quits (~jero98772@2800:484:1d7f:5d36::2) (Ping timeout: 240 seconds) |
| 20:23:17 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 20:23:32 | → | pavonia joins (~user@user/siracusa) |
| 20:24:00 | → | driib joins (~driib@176.57.184.141) |
| 20:24:47 | → | chromoblob joins (~user@37.113.180.121) |
| 20:26:16 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 20:27:48 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:28:49 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:33:34 | × | merijn quits (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 20:34:25 | → | jero98772 joins (~jero98772@2800:484:1d7f:5d36::2) |
| 20:36:13 | → | Zamyatins_Sky joins (~Zamyatins@broadband-188-255-84-143.ip.moscow.rt.ru) |
| 20:36:50 | × | driib quits (~driib@176.57.184.141) (Remote host closed the connection) |
| 20:37:13 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:37:46 | <Zamyatins_Sky> | Hi! Has anyone here tried the `beam` package (specifically, with SQLite backend)? For some reason, I can't even build the docs, because the build-docs.sh script complains about `TypeError: load() missing 1 required positional argument: 'Loader' |
| 20:37:47 | → | jaror[m] joins (~jaror@2001:470:69fc:105::265) |
| 20:43:27 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 20:46:06 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:47:12 | × | jonathan_ quits (~jonathan@83.252.3.92) (Ping timeout: 240 seconds) |
| 20:47:51 | × | Wojciech_K quits (~Wojciech_@2a01:4f9:6a:18a8::239) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 20:48:29 | → | Wojciech_K joins (~Wojciech_@2a01:4f9:6a:18a8::239) |
| 20:49:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:50:04 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Remote host closed the connection) |
| 20:50:41 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 20:50:53 | × | brettgilio quits (~brettgili@2001:19f0:5c00:27fc:5400:4ff:fe7a:1f8e) (Quit: The Lounge - https://thelounge.chat) |
| 20:51:01 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 20:51:39 | → | brettgilio joins (~brettgili@2001:19f0:5c00:27fc:5400:4ff:fe7a:1f8e) |
| 20:51:41 | × | brettgilio quits (~brettgili@2001:19f0:5c00:27fc:5400:4ff:fe7a:1f8e) (Client Quit) |
| 20:52:20 | → | brettgilio joins (~brettgili@2001:19f0:5c00:27fc:5400:4ff:fe7a:1f8e) |
| 21:00:40 | → | merijn joins (~merijn@145.90.225.2) |
| 21:01:30 | × | rembo10 quits (~rembo10@main.remulis.com) (Server closed connection) |
| 21:02:09 | → | rembo10 joins (~rembo10@2a01:4f9:c010:b5b9::1) |
| 21:02:58 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:03:18 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:06:28 | <Cale> | Zamyatins_Sky: We use beam where I work, but with the postgres backend, and we're using nix to build things, so I haven't had to mess with build-docs.sh |
| 21:07:05 | → | tromp joins (~textual@92.110.219.57) |
| 21:07:51 | <Cale> | I also usually just read the docs online, they're on hackage https://hackage.haskell.org/package/beam-core and here https://haskell-beam.github.io/beam/ |
| 21:08:21 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:09:05 | → | driib joins (~driib@176.57.184.141) |
| 21:09:50 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 21:13:25 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 21:14:39 | <Zamyatins_Sky> | Actually I do not need to build docs specifically, I want to use beam in my side project, and I am trying to figure out why the basic thing (conversion of custom types, which is explicitly described in docs) does not work |
| 21:16:05 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 21:17:18 | <ijqq> | So if I have a parser called char which is Char - Parser Char, I can make a string parser as stringParser = traverse char. But how can I define this parser using <*> and char? |
| 21:17:37 | <ijqq> | char -> Parser Char * |
| 21:18:50 | × | maerwald quits (~maerwald@mail.hasufell.de) (Server closed connection) |
| 21:19:09 | → | maerwald joins (~maerwald@mail.hasufell.de) |
| 21:20:21 | × | driib quits (~driib@176.57.184.141) (Remote host closed the connection) |
| 21:20:42 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:22:57 | × | tromp quits (~textual@92.110.219.57) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:24:18 | <monochrom> | No, not traverse. Perhaps many or some. |
| 21:24:55 | <monochrom> | err actually, |
| 21:24:58 | <monochrom> | @type traverse |
| 21:24:58 | → | glguy joins (~glguy@libera/staff-emeritus/glguy) |
| 21:24:59 | <lambdabot> | (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) |
| 21:25:19 | <monochrom> | Ah yeah traverse is right, you're going for [Char] -> Parser Char. |
| 21:25:30 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 21:25:57 | <monochrom> | traverse is implemented in the standard library by <*> pure and recursion in the "obvious" way. |
| 21:27:19 | × | S11001001 quits (sid42510@id-42510.ilkley.irccloud.com) (Server closed connection) |
| 21:27:30 | → | S11001001 joins (sid42510@id-42510.ilkley.irccloud.com) |
| 21:27:35 | <monochrom> | err [Char] -> Parser [Char] |
| 21:27:43 | <ijqq> | oh okay |
| 21:27:49 | <ijqq> | I mean, I understand that it must be |
| 21:28:01 | <ijqq> | But I guess the obvious way is not so obvious to me :/ |
| 21:28:07 | <ijqq> | Maybe I'll keep thikning about it |
| 21:28:11 | <glguy> | I've been revisiting my previous alex/happy generated TOML parser that I'd previously abandoned because the TOML specification is 1) a disaster to lex, 2) is a mess when it comes to what you're allowed to define or not with super/subtables/dottedkey-defined-tables, etc. but I think I've got it all worked out now :) https://glguy.net/gitea/glguy/toml |
| 21:28:15 | <monochrom> | Perhaps liftA2 (:) makes it more obvious than <*> |
| 21:28:46 | <glguy> | Other than those two complaints, I still rather like toml as a config language option |
| 21:29:06 | × | michalz quits (~michalz@185.246.207.201) (Remote host closed the connection) |
| 21:30:02 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 21:30:30 | <monochrom> | accept ['a', 'b', 'c'] = accept 'a', then accept ['b', 'c'], use (:) to combine their respective answers. |
| 21:30:46 | → | driib joins (~driib@176.57.184.141) |
| 21:30:52 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 240 seconds) |
| 21:32:08 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Ping timeout: 240 seconds) |
| 21:32:12 | × | jero98772 quits (~jero98772@2800:484:1d7f:5d36::2) (Ping timeout: 240 seconds) |
| 21:32:35 | × | fendor quits (~fendor@2a02:8388:1640:be00:7aca:a77a:4a28:631a) (Remote host closed the connection) |
| 21:34:12 | × | merijn quits (~merijn@145.90.225.2) (Ping timeout: 240 seconds) |
| 21:34:37 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 21:34:39 | → | bilegeek joins (~bilegeek@2600:1008:b0a2:c545:7bfb:76e2:41bb:db48) |
| 21:35:19 | × | driib quits (~driib@176.57.184.141) (Remote host closed the connection) |
| 21:35:39 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:36:56 | <ijqq> | I think it got it |
| 21:36:57 | <ijqq> | http://sprunge.us/XDEmJR |
| 21:37:17 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 21:37:26 | <ijqq> | the char'' |
| 21:37:39 | <ijqq> | oh it should be called chars oops |
| 21:38:07 | <monochrom> | Yeah :) |
| 21:38:22 | <ijqq> | cool, thank you for the help :) |
| 21:39:20 | <monochrom> | For the <*> version you just recall liftA2 (:) foo bar = (:) <$> foo <*> bar |
| 21:40:43 | <ijqq> | was just doing that |
| 21:40:45 | <ijqq> | nice |
| 21:40:54 | <ijqq> | thank you :) |
| 21:41:01 | <ijqq> | now I can go back to using traverse haha |
| 21:41:08 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 21:41:49 | → | driib joins (~driib@176.57.184.141) |
| 21:42:16 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 21:43:32 | <ijqq> | oh cool glguy, i am trying to write one now |
| 21:44:19 | <glguy> | ijqq: Sure, if you're doing parser exercises, this could be a good project |
| 21:44:30 | → | jero98772 joins (~jero98772@2800:484:1d7f:5d36::2) |
| 21:45:19 | <ijqq> | Yeah it's been interesting so far |
| 21:45:57 | <glguy> | https://toml.io/en/v1.0.0 |
| 21:47:18 | × | driib quits (~driib@176.57.184.141) (Read error: Connection reset by peer) |
| 21:47:39 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:48:10 | <ijqq> | Yep i've been going through that. I have only a few bits working, I can parse arrays and strings and numbers so far. But I still have lots left to do like figuring out how to actually assign all the correct stuff and then implementing more detailed stuff, like all the types of strings and the escapes and so on. |
| 21:48:12 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 21:49:31 | × | coot quits (~coot@89.69.206.216) (Quit: coot) |
| 21:49:52 | <Zamyatins_Sky> | Cale: I have composed a minimal reproductable example. I would really appreciate if you could look at that: https://bpa.st/FHQVG. |
| 21:53:00 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 258 seconds) |
| 21:53:29 | <Zamyatins_Sky> | It is basically what tutorial says, but with other wording.. yet I get a type mismatch: Couldn't match expected type ‘HaskellLiteralForQExpr StatsFormat’ with actual type ‘StatsFormat’ |
| 21:53:32 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 21:53:53 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:55:10 | <Zamyatins_Sky> | Moreover, if I add `default_` instead of `val_ 0` as the first argument to `StatsSingle` (to exploit the autoincrement), I get another error: Couldn't match type ‘QGenExpr ctxt0 be0 s0 a0’ with ‘Int’, Expected: Columnar Identity Int, Actual: QGenExpr ctxt0 be0 s0 a0 |
| 21:59:04 | <Cale> | on which line? |
| 21:59:17 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 21:59:47 | <Zamyatins_Sky> | Cale: Main.hs:93:44 |
| 22:03:08 | <Cale> | Maybe you'll get a better error message if you tell it what type you're expecting, so something like stat :: StatsSingleT (QGenExpr ctxt be s) |
| 22:05:10 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:05:54 | → | driib joins (~driib@176.57.184.141) |
| 22:07:08 | × | acidjnk_new quits (~acidjnk@p200300d6e7072f24519cabbd94a7f195.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 22:08:08 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 22:11:07 | × | driib quits (~driib@176.57.184.141) (Read error: Connection reset by peer) |
| 22:11:26 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:14:43 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) (Remote host closed the connection) |
| 22:15:06 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:20:10 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 22:20:45 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 22:23:00 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 22:23:20 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:24:51 | <Zamyatins_Sky> | Cale: wow, this was a rather useful advice. Adding `:: StatsSingleT ( QGenExpr ctxt Sqlite s )` to the binding of stat lead me to the solution. Thank you! By any chance, could you explain how `ctxt` and `s` are described by a type system? Link to the docs would be great too. I understand that they behave somewhat similar to `be`, which stands for any backend, but I do not understand where those type-vars are bound |
| 22:25:45 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:25:59 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 22:26:27 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 22:26:34 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 22:27:31 | → | wroathe joins (~wroathe@207.153.38.140) |
| 22:27:31 | × | wroathe quits (~wroathe@207.153.38.140) (Changing host) |
| 22:27:31 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:27:54 | <EvanR> | they're universally quantified by an understood forall ctxt s . in front of the type |
| 22:29:20 | <Zamyatins_Sky> | Oh, I see, it is implicit. Thank you |
| 22:29:39 | <EvanR> | there's an option to always show the forall in ghci... somewhere |
| 22:30:37 | <EvanR> | you can also use it in your type signatures, and there's situation where you have to use it for reasons |
| 22:34:16 | ← | Zamyatins_Sky parts (~Zamyatins@broadband-188-255-84-143.ip.moscow.rt.ru) () |
| 22:34:37 | <geekosaur> | :set -fprint-explicit-foralls |
| 22:36:27 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:36:47 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:42:32 | × | chromoblob quits (~user@37.113.180.121) (Ping timeout: 240 seconds) |
| 22:47:49 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:2847:13c1:54f7:ebbc) |
| 22:50:46 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 22:51:07 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 22:52:10 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 23:04:13 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:04:33 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:05:30 | <[Leary]> | ijqq: Yeah, that `isMany` ought to've been an `isSome`, my bad. Looks like you got it figured out, though. :) |
| 23:10:27 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 23:13:08 | → | cheater_ joins (~Username@user/cheater) |
| 23:14:54 | × | cheater quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 23:15:04 | cheater_ | is now known as cheater |
| 23:19:34 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:19:54 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:26:57 | × | user__ quits (~user@46.114.182.229) (Read error: Connection reset by peer) |
| 23:30:37 | → | merijn joins (~merijn@c-001-001-001.client.esciencecenter.eduvpn.nl) |
| 23:31:39 | × | Adeon quits (sid418992@id-418992.lymington.irccloud.com) (Server closed connection) |
| 23:32:10 | × | cafkafk quits (~cafkafk@fsf/member/cafkafk) (Remote host closed the connection) |
| 23:32:16 | → | Adeon joins (sid418992@2a03:5180:f:2::6:64b0) |
| 23:34:16 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:34:37 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:37:38 | → | cafkafk joins (~cafkafk@fsf/member/cafkafk) |
| 23:41:39 | × | lally quits (sid388228@id-388228.uxbridge.irccloud.com) (Server closed connection) |
| 23:41:47 | → | lally joins (sid388228@id-388228.uxbridge.irccloud.com) |
| 23:48:45 | × | driib quits (~driib@vmi931078.contaboserver.net) (Remote host closed the connection) |
| 23:49:08 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 23:55:23 | → | mauke_ joins (~mauke@user/mauke) |
| 23:56:42 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 252 seconds) |
| 23:56:42 | mauke_ | is now known as mauke |
| 23:56:57 | × | driib quits (~driib@vmi931078.contaboserver.net) (Read error: Connection reset by peer) |
| 23:57:18 | → | driib joins (~driib@vmi931078.contaboserver.net) |
All times are in UTC on 2023-06-18.