Newest at the top
| 2024-10-03 06:23:42 +0200 | <c_wraith> | Lens is all about bidirectional mapping, so it handles that case relatively easily. |
| 2024-10-03 06:23:23 +0200 | <c_wraith> | I just mean that in (s -> m (a, s)), s appears in both positive and negative position. This means it's not covariant or contravariant - you can't map it simply. |
| 2024-10-03 06:23:01 +0200 | <Lears> | If the type parameter to `DataType` is recoverable, then yes, it's simplest just to hide it with `Some DataType`. |
| 2024-10-03 06:22:32 +0200 | <Lears> | StateT uses the same type for the input state as the output state; so not unless you change both. If you lift this restriction with your own StateT', then you cannot make it a Monad, though you can make it an indexed monad. |
| 2024-10-03 06:22:19 +0200 | <c_wraith> | uh, not sure what you mean by that. |
| 2024-10-03 06:21:51 +0200 | <amano> | Then, I have to use existential typeclass in a data type? |
| 2024-10-03 06:21:20 +0200 | <c_wraith> | the trick, and why it appears in lens, is that the transformation needs to be bidirectional |
| 2024-10-03 06:20:41 +0200 | <c_wraith> | nothing in mtl/transformers provides that. mmorph doesn't seem to provide that. lens *does*, as part of the Zoom interface. |
| 2024-10-03 06:20:38 +0200 | <lambdabot> | (s -> m (a, s)) -> StateT s m a |
| 2024-10-03 06:20:37 +0200 | <Lears> | :t StateT |
| 2024-10-03 06:17:10 +0200 | <amano> | I mean StateT (DataType a) m () |
| 2024-10-03 06:16:36 +0200 | <amano> | Let's assume StateT (DataType a) m a. Can StateT replace DataType a with DataType b? |
| 2024-10-03 06:15:59 +0200 | amano | (amano@gateway/vpn/airvpn/amano) amano |
| 2024-10-03 06:14:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-10-03 06:12:45 +0200 | Tisoxin | (~Ikosit@user/ikosit) Ikosit |
| 2024-10-03 06:10:25 +0200 | mud | (~mud@user/kadoban) kadoban |
| 2024-10-03 06:10:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-03 06:08:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-10-03 06:06:56 +0200 | mud | (~mud@user/kadoban) (Client Quit) |
| 2024-10-03 06:03:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-03 06:02:30 +0200 | mud | (~mud@user/kadoban) kadoban |
| 2024-10-03 06:01:10 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-10-03 06:00:48 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 246 seconds) |
| 2024-10-03 05:59:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-03 05:58:50 +0200 | mud | (~mud@user/kadoban) (Quit: quit) |
| 2024-10-03 05:58:30 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty for ref |
| 2024-10-03 05:57:12 +0200 | <EvanR> | haskell maths |
| 2024-10-03 05:56:48 +0200 | <EvanR> | and use a convention that "computing the bottom" means the algorithm provably freezes up xD |
| 2024-10-03 05:56:07 +0200 | <EvanR> | but I figured that'd be weird |
| 2024-10-03 05:55:54 +0200 | <EvanR> | you could posit a mathematical function into a space that includes an additional bottom value |
| 2024-10-03 05:55:50 +0200 | <Lears> | "reduced to a logic program" is also unclear. |
| 2024-10-03 05:54:34 +0200 | <Lears> | You probably want the "general recursive functions". |
| 2024-10-03 05:54:21 +0200 | <Lears> | thirdofmay: Computable functions are mathematical functions; they have no inherent notion of implementation or termination; they're defined at every argument. |
| 2024-10-03 05:53:42 +0200 | <EvanR> | any* non-termination |
| 2024-10-03 05:53:16 +0200 | <EvanR> | these functions wouldn't be missing any answers, and so an non-termination would be a failure to implement |
| 2024-10-03 05:52:56 +0200 | <EvanR> | a mathematical function from integers to integers is computable if there's an algorithm which can implement this function, so non-termination wouldn't come up here because of the codomain in the premise |
| 2024-10-03 05:51:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> i mean i think they are independent from one another, and termination or non-termination is a property of computable functions |
| 2024-10-03 05:51:54 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2024-10-03 05:50:13 +0200 | <EvanR> | not saying they are the same |
| 2024-10-03 05:50:00 +0200 | <EvanR> | :thonk: |
| 2024-10-03 05:49:49 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: yeah I think termination and computability are distinct things |
| 2024-10-03 05:48:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-10-03 05:47:39 +0200 | <EvanR> | if not, that makes some undecidable problems computable |
| 2024-10-03 05:47:09 +0200 | <EvanR> | for some inputs |
| 2024-10-03 05:47:00 +0200 | <EvanR> | is it even a computable function if it doesn't terminate |
| 2024-10-03 05:45:47 +0200 | <haskellbridge> | <thirdofmay18081814goya> can all problems regarding whether or not a computable function terminates be reduced to a logic program? |
| 2024-10-03 05:44:18 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-03 05:43:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-03 05:43:18 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2024-10-03 05:41:39 +0200 | billchenchina- | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) billchenchina |