`Unalign` instances for sequence types? (list, vector, etc.)

[LightAndLight]

I'm creating this issue because I thought that Unalign was missing instances for sequences, like list and vector. I'm technically wrong, according to the class's laws, but I think it's still worth discussing.

My intuition went like this: just as Unzip can be implemented for any Functor, it looks like Unalign can be implemented for any Filterable:

unalignDefault :: Filterable f => f (These a b) -> (f a, f b)
unalignDefault xs =
  ( mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) xs
  , mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) xs
  )

Despite my intuition, sequences don't satisfy one of the Unalign laws: uncurry align (unalign xs) ≡ xs. They do satisfy the other, however: unalign (align xs ys) ≡ (xs, ys).

While it's not a lawful Unalign implementation, I still feel like unalignDefault is a reasonable function, which is why I think this is worth talking about. unalign <-> uncurry align is currently specified as an isomorphism, which rules out sequence types, but it seems reasonable to only require unalign to be a left inverse of uncurry align.

Curiously, Unzip has a sort of "dual" version of this relaxation: unzip is only required be the right inverse of uncurry zip, because requiring them to form an isomorphism would rule out map types.

---

Proofs / working out

A quick proof for Unalign [] to check that my intuition is lawful:

uncurry align (unalign xs) ≡ xs:

forall (xs :: [a]).

uncurry align (unalign xs)
= { unalign definition }
uncurry align
  ( mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) xs
  , mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) xs
  )
= { uncurry definition }
align
  (mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) xs)
  (mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) xs)

induction on xs:

* xs@[]

  align
    (mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) [])
    (mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) [])
  = { mapMaybe _ [] }
  align [] []
  = { align definition }
  That <$> []
  = { (<$>) definition }
  []

* xs@(x : ys)
  uncurry align (unalign ys) = ys

  align
    (mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (x : ys))
    (mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (x : ys))
  = { mapMaybe definition }
  align
    (maybe id (:) ((\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) x) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
    (maybe id (:) ((\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) x) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)

  case analysis on x:

  * x@(These a b)

    align
      (maybe id (:) ((\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (These a b)) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) ((\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (These a b)) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { beta reduction }
    align
      (maybe id (:) (Just a) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) (Just b) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { maybe definition }
    align
      (a : mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (b : mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { align definition }
    These a b :
    align
      (mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { unalign definition, uncurry definition }
    uncurry align (unalign ys)
    = { inductive hypothesis }
    ys

  * x@(This a)

    align
      (maybe id (:) ((\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (This a)) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) ((\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (This a)) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { beta reduction }
    align
      (maybe id (:) (Just a) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) Nothing $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { maybe definition }
    align
      (a : mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)

    (stuck)

  * x@(That b)

    align
      (maybe id (:) ((\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (That b)) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) ((\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (That b)) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { beta reduction }
    align
      (maybe id (:) Nothing $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (maybe id (:) (Just b} $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)
    = { maybe definition }
    align
      (mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) ys)
      (b : mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) ys)

    (stuck)

It looks like it doesn't work out. A counterexample:

exists (xs :: [This a b]). uncurry align (unalign xs) != xs:

uncurry align (unalign [This 1, That "a", This 2, That "b", This 3])
=
uncurry align ([1, 2, 3], ["a", "b"])
=
[These 1 "a", These 2 "b", This 3]

How does this law work out for Map, then?

uncurry align (unalign [("k1", This 1), ("k2", That "a"), ("k3", This 2), ("k4", That "b"), ("k5", This 3)])
=
uncurry align ([("k1", This 1), ("k3", This 2), ("k5", This 3)], [("k2", That "a"), ("k4", That "b")])
=
[("k1", This 1), ("k2", That "a"), ("k3", This 2), ("k4", That "b"), ("k5", This 3)]

It works out because the Map "preserves keys"; each value has the same key before and after unaligning.

The other law does hold for lists: unalign (align xs ys) ≡ (xs, ys). Less formally:

• unalign (align [] ys) ≡ ([], ys)
• unalign (align xs []) ≡ (xs, [])

• unalign (align (x : xs) (y : ys))
  =
  unalign (These x y : align xs ys)
  =
  ( mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (These x y : align xs ys)
  , mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (These x y : align xs ys)
  )
  =
  ( maybe id (:) ((\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (These x y)) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (align xs ys)
  , maybe id (:) ((\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (These x y)) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (align xs ys)
  )
  =
  ( maybe id (:) (Just x) $ mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (align xs ys)
  , maybe id (:) (Just y) $ mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (align xs ys)
  )
  =
  ( x : mapMaybe (\case; This a -> Just a; That _ -> Nothing; These a _ -> Just a) (align xs ys)
  , y : mapMaybe (\case; This _ -> Nothing; That b -> Just b; These _ b -> Just b) (align xs ys)
  )
  =
  ( x : fst (unalign (align xs ys))
  , y : snd (unalign (align xs ys))
  )
  =
  ( x : xs
  , y : ys
  )
  

[phadej]

Curiously, Unzip has a sort of "dual" version of this relaxation: unzip is only required be the right inverse of uncurry zip, because requiring them to form an isomorphism would rule out map types.

Fair observation.

And obvious f (These a b) -> (f a, f b) operation for list-like types deserve a name.

Maybe uncurry align (unalign xs) ≡ xs law could be dropped. Zip and Align are dual-ish after all. (I can't remember of anyone relying on the law, or actually doing any polymorphic over Unalign f programming)

I have to think a bit about this.

[LightAndLight]

In my own work I realised that I reached for Unalign too soon, and used partitionEithers instead.

Here's how I've started thinking about it:

class Functor f => Unzip f where
  unzipWith :: (a -> (b, c)) -> f a -> (f b, f c)

unzipFmapDefault1 :: Unzip f => (a -> b) -> f a -> f b
unzipFmapDefault1 f = fst . unzipWith (\a -> (f a, ()))

unzipFmapDefault2 :: Unzip f => (a -> b) -> f a -> f b
unzipFmapDefault2 f = snd . unzipWith (\a -> ((), f a))


class Functor f => Partition f where
  partitionWith :: (a -> Either b c) -> f a -> (f b, f c)

partitionFmapDefault1 :: Partition f => (a -> b) -> f a -> f b
partitionFmapDefault1 f = fst . partitionWith (Left . f)

partitionFmapDefault2 :: Partition f => (a -> b) -> f a -> f b
partitionFmapDefault2 f = snd . partitionWith (Right . f)


class (Unzip f, Partition f) => Unalign f where
  unalignWith :: (a -> These b c) -> f a -> (f b, f c)

unalignUnzipWithDefault :: Unalign f => (a -> (b, c)) -> f a -> (f b, f c)
unalignUnzipWithDefault f = unalignWith (uncurry These . f)

unalignPartitionWithDefault :: Unalign f => (a -> Either b c) -> f a -> (f b, f c)
unalignPartitionWithDefault f = unalignWith (either This That . f)

[mniip]

I will add here that Filterable is morally a superclass of Unalign, meaning any Unalign instance is automatically Filterable:

catMaybesDefault :: Unalign f => f (Maybe a) -> f a
catMaybesDefault = snd . unalignWith (maybe (This ()) (These ()))

So if we accept the proposed semantics and relax the inverse restriction, then all instances of Filterable become instances of Unalign, i.e. the two type classes become equivalent. Then why have two typeclasses?

Hence I argue that Unalign should retain its additional law to make it a strictly narrower typeclass than Filterable. And if you want to "unalign" lists you should just use filterable machinery instead.