Newest at the top
2024-11-08 20:17:50 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2024-11-08 20:15:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
2024-11-08 20:14:19 +0100 | <tomsmeding> | is what I meant |
2024-11-08 20:14:17 +0100 | <kaol> | Are you sure you didn't do it with megaparsec the last time? It has more knobs including type variable for the error type. |
2024-11-08 20:14:16 +0100 | <tomsmeding> | sure, but the Parser monad doesn't support anything more general than String |
2024-11-08 20:14:09 +0100 | <geekosaur> | `fail :: String -> m a` |
2024-11-08 20:13:57 +0100 | <geekosaur> | https://downloads.haskell.org/ghc/latest/docs/libraries/base-4.20.0.0-1f57/Control-Monad-Fail.html… |
2024-11-08 20:13:43 +0100 | <tomsmeding> | "requires"? |
2024-11-08 20:13:19 +0100 | <geekosaur> | afaik `fail` itself requires it? |
2024-11-08 20:12:57 +0100 | <tomsmeding> | and the type that `fail` uses in the parser monad looks pretty monomorphically String |
2024-11-08 20:11:50 +0100 | <tomsmeding> | it has `fail` if you're okay with strings |
2024-11-08 20:11:41 +0100 | <kqr> | Hm. I'd hoped I could hook into the parser monad itself, but maybe it doesn't support failure in the way I think of it? |
2024-11-08 20:11:15 +0100 | <kaol> | ExceptT is one option. |
2024-11-08 20:07:43 +0100 | <kqr> | Hm. I'm looking at doing some validation in an Attoparsec parser and I want to fail the parse if the validation fails – ideally with a value of some custom error type. I feel like I have done this before but I cannot for the life of me figure out how I did it now. |
2024-11-08 20:07:03 +0100 | longlongdouble | (~longlongd@169.150.196.101) (Ping timeout: 245 seconds) |
2024-11-08 20:06:06 +0100 | <ncf> | ah, https://en.wikipedia.org/wiki/Natural_transformation#Whiskering |
2024-11-08 20:06:05 +0100 | <famubu> | Okay, looks like I got a few terms to look up. Thanks. Had seen horizonatal composition mentioned in the wikipedia article. Reading nlab now. |
2024-11-08 20:05:10 +0100 | <ncf> | or pure @T @(T a) |
2024-11-08 20:04:40 +0100 | shapr | (~user@2601:19c:417e:5434:6d2c:aeb2:81b3:3df4) shapr |
2024-11-08 20:04:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-11-08 20:04:06 +0100 | <ncf> | in haskell, Tη is fmap @T pure, while ηT is pure @(T a) |
2024-11-08 20:03:29 +0100 | <ncf> | also called horizontal compositions: https://en.wikipedia.org/wiki/Natural_transformation#Operations_with_natural_transformations |
2024-11-08 20:03:09 +0100 | <ncf> | famubu: those are whiskerings |
2024-11-08 20:00:18 +0100 | <tomsmeding> | perhaps wait until someone like ncf comes along lol |
2024-11-08 20:00:09 +0100 | <tomsmeding> | I'm not sure what I just said is correct |
2024-11-08 19:59:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
2024-11-08 19:58:51 +0100 | <tomsmeding> | the difference is that the source and target of T(mu_X) have an additional T() around them |
2024-11-08 19:58:37 +0100 | <tomsmeding> | see e.g. the third commutative diagram: you have mu_X on the bottom arrow, and T(mu_X) on the top arrow |
2024-11-08 19:58:10 +0100 | <tomsmeding> | they denote that by applying T to the natural transformation |
2024-11-08 19:57:56 +0100 | <tomsmeding> | if you have a natural transformation between two functors T1 and T2, and a functor T, then you can build a natural transformation from T . T1 to T . T2 |
2024-11-08 19:57:09 +0100 | longlongdouble | (~longlongd@169.150.196.101) |
2024-11-08 19:56:51 +0100 | <tomsmeding> | famubu: a functor from C to C' consists of a mapping from Ob C to Ob C' and a mapping from the arrows in C to the arrows in C' |
2024-11-08 19:51:56 +0100 | <famubu> | I am not that familiar with category theory. |
2024-11-08 19:51:49 +0100 | <famubu> | * `T` is a functor. |
2024-11-08 19:51:35 +0100 | <famubu> | is a functor. That means it's like a function whose 'argument' is a category, right? And `η` is a natural transformation, not a category. |
2024-11-08 19:51:31 +0100 | <famubu> | I could understand `η T` part. It does the 'opposite' of flattening. |
2024-11-08 19:51:19 +0100 | <famubu> | What is the difference between the two? |
2024-11-08 19:51:16 +0100 | <famubu> | The commutative diagram and properties mention both `T ηand `η T`. |
2024-11-08 19:51:13 +0100 | <famubu> | I was looking at the wikipedia page for monad in category theory: https://en.wikipedia.org/wiki/Monad_(category_theory)#Formal_definition |
2024-11-08 19:51:12 +0100 | user363627 | (~user@user/user363627) (Quit: Konversation terminated!) |
2024-11-08 19:50:41 +0100 | longlongdouble | (~longlongd@169.150.196.101) (Remote host closed the connection) |
2024-11-08 19:47:01 +0100 | longlongdouble | (~longlongd@169.150.196.101) |
2024-11-08 19:46:41 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Read error: Connection reset by peer) |
2024-11-08 19:46:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-11-08 19:45:53 +0100 | <kqr> | merijn, Numeric looks good for what I need. Thanks! |
2024-11-08 19:42:58 +0100 | noctux | (~noctux@user/noctux) noctux |
2024-11-08 19:42:33 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
2024-11-08 19:42:27 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2024-11-08 19:41:49 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
2024-11-08 19:41:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |