Newest at the top
2024-10-03 06:29:58 +0200 | <amano> | I need `a` to be a typeclass instance. |
2024-10-03 06:29:31 +0200 | <Lears> | `DataType` |
2024-10-03 06:29:21 +0200 | <amano> | What is f? |
2024-10-03 06:29:20 +0200 | <dmj`> | * uses existential to solve problem, now has two problems * |
2024-10-03 06:28:48 +0200 | <Lears> | I don't know why there's a class involved here at all? All you need is `data Some f = forall a. Some (f a)`. |
2024-10-03 06:28:11 +0200 | <amano> | But, I prefer existential typeclass... |
2024-10-03 06:28:03 +0200 | <amano> | I know it can be represented as a record of functions.... |
2024-10-03 06:27:44 +0200 | <c_wraith> | it's no different from just passing around a function, or a record of them. |
2024-10-03 06:27:41 +0200 | <amano> | This is the only way I know to use multiple typeclass instances in StateT. |
2024-10-03 06:27:16 +0200 | <amano> | Why? |
2024-10-03 06:27:11 +0200 | <c_wraith> | and it's kinda useless. |
2024-10-03 06:26:33 +0200 | <amano> | This is existential typeclass |
2024-10-03 06:26:29 +0200 | <amano> | I mean data SomeType = forall a. TypeClass a => SomeType a |
2024-10-03 06:25:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
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 |