Newest at the top
| 2024-12-29 04:11:00 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. any work that can done by a type, as an indexing type, will be the same as can be done by either "Finite n" or the type of natural numbers |
| 2024-12-29 04:10:30 +0100 | prasad | (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) (Ping timeout: 260 seconds) |
| 2024-12-29 04:08:43 +0100 | <haskellbridge> | <thirdofmay18081814goya> there is no type that can carry more information as an indexing type*** |
| 2024-12-29 04:08:25 +0100 | <haskellbridge> | <thirdofmay18081814goya> there is no type that can carry more information that either "Finite n" or "Nat", so I think it is a good starting point |
| 2024-12-29 04:07:49 +0100 | <haskellbridge> | <thirdofmay18081814goya> well |
| 2024-12-29 04:07:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> thinking about specifically the case where the indexes are given by "Finite n" |
| 2024-12-29 04:07:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 04:05:34 +0100 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2024-12-29 04:05:03 +0100 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2024-12-29 04:02:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:00:27 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2024-12-29 04:00:07 +0100 | <haskellbridge> | <thirdofmay18081814goya> we want there to be a strict ordering in the indexing type/sort right? |
| 2024-12-29 03:59:50 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm |
| 2024-12-29 03:52:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 03:45:04 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 265 seconds) |
| 2024-12-29 03:44:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:32:16 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 03:27:53 +0100 | <Leary> | This is clearer when looking at a corresponding indexed applicative: `unit :: f i i (); fuse :: f i j a -> f j k b -> f i k (a, b)` |
| 2024-12-29 03:27:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:24:00 +0100 | <Leary> | thirdofmay: The Atkey indexed monad has two indices for the same reason `Category` arrows do; its bind performs a kind of composition. Simple examples include the indexed writer monad, which writes category arrows rather than monoids, and the indexed state monad which has distinct types for the initial and final state. |
| 2024-12-29 03:16:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-29 03:12:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 03:11:41 +0100 | <lambdabot> | Consider it noted. |
| 2024-12-29 03:11:40 +0100 | <Leary> | @tell prsteele https://play.haskell.org/saved/J7bdQ5zn |
| 2024-12-29 03:06:24 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-29 03:04:56 +0100 | thatonelutenist | (8216c46202@2a03:6000:1812:100::fb3) thatonelutenist |
| 2024-12-29 03:03:11 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 03:00:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 02:55:47 +0100 | comonad | (~comonad@p200300d027182d00bcfd40be9d94d2dc.dip0.t-ipconnect.de) |
| 2024-12-29 02:54:07 +0100 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-12-29 02:54:03 +0100 | comonad | (~comonad@p200300d0270bcb00d2bd35ff80c069c9.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2024-12-29 02:53:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:52:22 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-12-29 02:47:33 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 2024-12-29 02:44:58 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-29 02:39:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-29 02:37:53 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f42bc4ebb891d7561a4.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2024-12-29 02:36:55 +0100 | <hololeap> | ok I think I see what you mean |
| 2024-12-29 02:35:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 02:32:11 +0100 | <ncf> | i.e. applicative functors are monoids in the category of endofunctors *with Day convolution as the monoidal product* |
| 2024-12-29 02:31:34 +0100 | <ncf> | well that doesn't tell you which monoidal structure you put on it |
| 2024-12-29 02:31:29 +0100 | <hololeap> | (I barely understand this stuff so don't take me too seriously) |
| 2024-12-29 02:30:10 +0100 | <hololeap> | isn't that usually just referred to as "the category of endofunctors" |
| 2024-12-29 02:28:29 +0100 | <ncf> | i.e. the endomorphism monoidal category on Set in the bicategory of categories |
| 2024-12-29 02:27:24 +0100 | <ncf> | composition of endofunctors |
| 2024-12-29 02:27:14 +0100 | <ncf> | with composition as the monoidal product |
| 2024-12-29 02:26:37 +0100 | <hololeap> | "with composition" seems like it would be redundant. isn't that implied by it being a category? |
| 2024-12-29 02:25:55 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-12-29 02:23:42 +0100 | <ncf> | (the one that monads are just monoids in) |
| 2024-12-29 02:23:31 +0100 | <ncf> | i guess the one-sentence definition of an indexed monad is "category enriched in the monoidal category of endofunctors with composition" |