Newest at the top
| 2024-10-06 20:46:08 +0200 | <tomsmeding> | this _can_ be implemented for Set by setting FConstr Set = Ord |
| 2024-10-06 20:45:56 +0200 | <tomsmeding> | let me pull up my Functor' suggestion again for reference: class Functor' f where { type FConstr f ; fmap' :: (FConstr a, FConstr b) => (a -> b) -> f a -> f b } |
| 2024-10-06 20:45:16 +0200 | <tomsmeding> | monochrom: Set is not a Functor, for sure, but there is a Functor-like class (that does not correspond to what CT calls a "functor") that Set can implement; it's the Functor' that I gave before |
| 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) |