Restricting and weakening CoRec

[ElvishJerricco]

I'm having trouble figuring out how to write the following functions:

weakenCoRec :: CoRec f ts -> CoRec f (t ': ts)
restrictCoRec :: CoRec f (t ': ts) -> Either (f t) (CoRec f ts)

They seem like they'd be good additions to this library, but I'm not sure if it's possible to implement them with the current CoRec implementation.

[acowley]

Is match1 close to helping? The RDelete type family application is a wrinkle. These functions are good ideas, we should have them.

[ElvishJerricco]

Ah I missed match1... Only works on Identity, but that seems fixable. Main problem is that I think it's linear time, but the constant size data structure makes me think it's possible to do it in constant time, though I have no idea how.

[ElvishJerricco]

Alright, so I did manage to implement restrictCoRec:

class RIndex t ts ~ i => FMatch1 t ts i where
  fmatch1' :: Handler r (f t) -> Rec (Maybe :. f) ts -> Either r (Rec (Maybe :. f) (RDelete t ts))

instance FMatch1 t (t ': ts) 'Z where
  fmatch1' _ (Compose Nothing :& xs) = Right xs
  fmatch1' (H h) (Compose (Just x) :& _) = Left (h x)

instance (FMatch1 t ts i, RIndex t (s ': ts) ~ 'S i,
          RDelete t (s ': ts) ~ (s ': RDelete t ts))
         => FMatch1 t (s ': ts) ('S i) where
  fmatch1' h (x :& xs) = (x :&) <$> fmatch1' h xs

-- | Handle a single variant of a 'CoRec': either the function is
-- applied to the variant or the type of the 'CoRec' is refined to
-- reflect the fact that the variant is /not/ compatible with the type
-- of the would-be handler
fmatch1 :: (FMatch1 t ts (RIndex t ts),
            RecApplicative ts,
            FoldRec (RDelete t ts) (RDelete t ts))
        => Handler r (f t)
        -> CoRec f ts
        -> Either r (CoRec f (RDelete t ts))
fmatch1 h = fmap (fromJust . firstField)
          . fmatch1' h
          . coRecToRec

restrictCoRec :: (RecApplicative ts, FoldRec ts ts) => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRec = fmatch1 (H id)

[ElvishJerricco]

That said, my overall goal was to implement GEq / GCompare for this Union type:

newtype Flap a f = Flap (f a)
newtype Union ts a = Union (CoRec (Flap a) ts)

I found instances based on restrictCoRec, but they call restrictCoRec a linear number of times, which itself is linear time. It seems reasonable that this could be constant time, but my solutions for these instances are quadratic. I might be able to swallow linear time for now, but quadratic is too much. I've tried rewriting the instances in terms of fmatch1 directly, but ultimately it's proving difficult or impossible to get the constraints I need without hard coding them into CoRec itself.

[acowley]

I'd be interested in discussing how to avoid bouncing between a CoRec and a Rec some time if you want to chat on IRC or email or something as I'd like some help improving things, but I don't want to dump an essay here.

Here's another take on these functions:

restrictCoRec :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
              => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRec = go . coRecToRec
  where go :: Rec (Maybe :. f) (t ': ts) -> Either (f t) (CoRec f ts)
        go (Compose Nothing :& xs) = Right (fromJust (firstField xs))
        go (Compose (Just x) :& _) = Left x

weakenCoRec :: (RecApplicative ts, FoldRec (t ': ts) (t ': ts))
            => CoRec f ts -> CoRec f (t ': ts)
weakenCoRec = fromJust . firstField . (Compose Nothing :&) . coRecToRec

The use of fromJust is annoying, but I didn't immediately see a way around it. In restrictCoRec, it's saying that since the wanted field was not first, it must be elsewhere in the record because we know that coRecToRec put a Just somewhere.

weakenCoRec is interesting because we don't know if t shadows another field already in the list (in particular, the type of the value we hold in the CoRec), but this type checks. Here the fromJust is because we know we started with a CoRec, so the result of coRecToRec has precisely one Just value, which means that firstField must return a Just.

If these seem okay, we can add them and see where that leads.