Newest at the top
| 2024-10-06 20:45:02 +0200 | <monochrom> | To be sure, I don't know how to argue why it's a problem. :) |
| 2024-10-06 20:45:01 +0200 | <geekosaur> | because when it comes down to it, Haskell isn't good at CT |
| 2024-10-06 20:44:46 +0200 | <geekosaur> | right, the only thing I'm coming up with is that Haskell can't express it properly given the constraint, so you need to pass in the types for some reason |
| 2024-10-06 20:44:34 +0200 | <tomsmeding> | hm, I guess that still doesn't really help, because b is fully polymorphic |
| 2024-10-06 20:44:20 +0200 | <monochrom> | Is it related to this? size :: Set a -> Int (with or without Ord a) fails to be a natural transformation: size . fmap_Set (const ()) ≠ size |
| 2024-10-06 20:44:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-06 20:44:03 +0200 | <tomsmeding> | now I guess you could encode the Ord requirement by putting it in the element types: something like: data WithOrd a = Ord a => WithOrd a |
| 2024-10-06 20:43:18 +0200 | <tomsmeding> | under that assumption: the only additional information IxFunctor has about f over Functor, is that f apparently has two additional type arguments, called j and k here. IxFunctor's imap keeps j and k constant, and doesn't use them in some other way, so even if j and k encode some info about Ord somehow, it's unused |
| 2024-10-06 20:42:45 +0200 | glguy | ghoulguy |
| 2024-10-06 20:42:06 +0200 | glguy | (glguy@libera/staff/glguy) glguy |
| 2024-10-06 20:41:05 +0200 | ghoulguy | (glguy@libera/staff/glguy) (Quit: Quit) |
| 2024-10-06 20:41:04 +0200 | <tomsmeding> | i/j/k, I guess |
| 2024-10-06 20:40:51 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-06 20:40:36 +0200 | <tomsmeding> | especially when comparing this indexed FAM hierarchy with the normal hierarchy, and noting that they are equivalent if you forget the j/k type indices everywhere |
| 2024-10-06 20:39:55 +0200 | <tomsmeding> | but I guess that's a reasonable one |
| 2024-10-06 20:39:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-06 20:39:35 +0200 | <tomsmeding> | oh, I realise that I am making one assumption about the "intended meaning" of this IxFunctor class: that 'a' and 'b' are element types of the container thing |
| 2024-10-06 20:38:54 +0200 | <tomsmeding> | and there is none :p |
| 2024-10-06 20:38:52 +0200 | <tomsmeding> | regardless of where that constraint comes from |
| 2024-10-06 20:38:51 +0200 | <geekosaur> | I'm not quite sure how, but that's usually true when CT is involved 😛 |
| 2024-10-06 20:38:44 +0200 | <tomsmeding> | but then there should be a constraint somewhere in the type, right? A constraint on a and/or b, at the very least |
| 2024-10-06 20:38:22 +0200 | <geekosaur> | but as I said, I think it enables you to replace "must preserve order" to "must preserve `Ord` constraint" |
| 2024-10-06 20:38:03 +0200 | <tomsmeding> | it's not like I understand the CT |
| 2024-10-06 20:37:55 +0200 | <tomsmeding> | of course :p |
| 2024-10-06 20:37:48 +0200 | <geekosaur> | remembering that what I wrote may be not merely out in left field, but somewhere in the parking lot, because I barely understand half the stuff involved |
| 2024-10-06 20:37:32 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-06 20:35:48 +0200 | <tomsmeding> | (i.e. I'm not trying to prove geekosaur wrong, I'm trying to make sure that I'm not wrong by investigating the incompatibility between my mental model and what geekosaur writes) |
| 2024-10-06 20:35:13 +0200 | <tomsmeding> | and geekosaur was claiming that it does, hedged in uncertainty that I fully respect |
| 2024-10-06 20:34:49 +0200 | <tomsmeding> | I was trying to argue that this IxFunctor extends Functor in an orthogonal way that doesn't solve the "Set can't be an instance of this class" 'problem' |
| 2024-10-06 20:34:43 +0200 | <davean> | Set specificly violates what a functor is |
| 2024-10-06 20:34:24 +0200 | <davean> | Set *can't* be a member of functor, and thats the proof why |
| 2024-10-06 20:34:22 +0200 | <tomsmeding> | which is what I was trying to argue to geekosaur? |
| 2024-10-06 20:34:11 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-06 20:34:11 +0200 | <davean> | it doesn't it shows why said is impossible. |
| 2024-10-06 20:33:53 +0200 | <tomsmeding> | i.e. the "Set should be an instance of this class somehow" |
| 2024-10-06 20:33:43 +0200 | <tomsmeding> | but how does keeping j and k constant help in implementing my Functor' from above? |
| 2024-10-06 20:33:39 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-06 20:33:32 +0200 | <tomsmeding> | I know, I saw IxMonad |
| 2024-10-06 20:33:27 +0200 | <davean> | Consider vs. Monad |
| 2024-10-06 20:33:16 +0200 | <davean> | tomsmeding: yes, EXACTLY |
| 2024-10-06 20:33:12 +0200 | <tomsmeding> | monochrom: that's just if you want the fmap to be linear time :p |
| 2024-10-06 20:32:50 +0200 | <tomsmeding> | davean: they are kept constant, which is indeed a use I guess |
| 2024-10-06 20:32:43 +0200 | <monochrom> | My perspective is you need a theorem-stating language. fmap_Set :: (Ord a, Ord b) => (a -> b) -> (assurance that that function is monotonic) -> Set a -> Set b should be fine. Alternatively, (Ord a, Ord b) => (MonotonicFunction a b) -> Set a -> Set b |
| 2024-10-06 20:32:38 +0200 | <tomsmeding> | the input and output type _of this fmap-like operation_ are just a and b |
| 2024-10-06 20:32:36 +0200 | <davean> | tomsmeding: They're not unused. |
| 2024-10-06 20:32:16 +0200 | <tomsmeding> | just to be certain we're talking about the same thing: class IxFunctor f where imap :: (a -> b) -> f j k a -> f j k b |
| 2024-10-06 20:31:39 +0200 | <tomsmeding> | (and I do have a vague suspicion of what it's supposed to mean, by looking at IxMonad, but that's beside the point in this case) |
| 2024-10-06 20:31:32 +0200 | <geekosaur> | I think in the case of Set (or Ord constraint) it captures the input and output types so they don't have to obey "doesn't alter structure" except in an abstract sense (hence "pseudonatural transformation"); but you'd need to ask a CT wonk to be certain |
| 2024-10-06 20:31:05 +0200 | <tomsmeding> | because there are no constraints on 'a' and 'b' |
| 2024-10-06 20:30:23 +0200 | <tomsmeding> | well, my point is that whatever it's supposed to mean, it _cannot_ express my Functor' :p |