Add ApSingle

[woehr]

ApSingle is like Ap, except a row of type operators are applied to a single type instead of a row of types.

As mentioned in #53 (comment), this adds ApplyRow renamed to ApSingle. Compared to ApplyRow, I reordered the arguments of ApSingle so it more closely matches Ap.

Please let me know if you'd like any changes!

[dwincort]

First off, thanks a ton for contributing!

I see no problem merging this as is, but I do wonder if there is any value-level functionality that we should add to make use of ApSingle. For instance, should row-types include something like your varFAlg function?

extractSingle
  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
   . (Forall fs c)
  => (forall f . (c f) => f x -> y)
  -> Var (ApSingle fs x)
  -> y

Another possibility is a way to map over ApSingle:

mapSingle
  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
   . (Forall fs c)
  => (forall f . (c f) => f x -> f y)
  -> Var (ApSingle fs x)
  -> Var (ApSingle fs y)

Using mapSingle, the Functor instance for VarF fs reduces to (I think):

fmap f = VarF . mapSingle @Functor @fs @a @b (fmap f) . unVarF

What do you think?

[woehr]

I think these value-level functions are easily generic enough to be included in row-types. I've already done extractSingle and mapSingle and am just looking if I can similarly extract the functionality I use for VarF's Eq1 and Ord1 instances. Once I finish that, I'll update the pull request.

On a somewhat related note: I wonder if it's possible to write these functions in terms of already existing functions in row-types. For example, extractSingle is basically erase.

erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b

and mapSingle is basically map.

map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r)

This was something I tried when I was originally working on open-adt but ultimately got no where with. My conclusion was that at the type level, these were all just a little too different. I'm still a beginner when it comes to this kind of stuff, so if you have any insight into this, I'd appreciate it.

On another (slightly less) related note, ApSingle could also be written in terms of Ap if we had some kind of ModifyAll (as below):

type family ModifyAllR (a :: k1) (ρ :: [LT k2]) :: [LT k1] where
  ModifyAllR a (l :-> _ ': ρ) = l :-> a ': ρ
  ModifyAllR a (l :-> _ ': ρ) = l :-> a ': ModifyAllR a ρ

Then perhaps some utility functions for Ap could be used with ApSingles as well. I do not know if it's worth exploring that or not though ...

[dwincort]

This is backwards!

[dwincort]

On a somewhat related note: I wonder if it's possible to write these functions in terms of already existing functions in row-types.

Yes, that's a great idea! The key to using erase in writing extractSingle is finding a way to turn the Forall fs c into something like Forall (ApSingle fs x) c'. Of course, what should c' be, and how can we make this conversion?

Actually, this is very similar to the mapForall entailment:

mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f)

The new constraint c' is this funky thing IsA c f x, which is a special class (and a related data type) that boils down to proof that x has the "type shape" f t for some t and further that the constraint c holds on t.

So, we can make a new version of IsA, now designed for ApSingle:

data As' c t a where
  As' :: forall c f a t. (a ~ f t, c f) => As' c t a

class ActsOn c t a where
  actsOn :: As' c t a

instance c f => ActsOn c t (f t) where
  actsOn = As'

If types satisfy ActsOn c t a, then we know that a is some type of the form f t, and f satisfies the constraint c. Great! This lets us write apSingleForall:

-- | An internal type used by the 'metamorph' in 'apSingleForall'.
newtype ApSingleForall c a (fs :: Row (k -> k')) = ApSingleForall
  { unApSingleForall :: Dict (Forall (ApSingle fs a) (ActsOn c a)) }

-- | This allows us to derive a `Forall (ApSingle f r) ..` from a `Forall f ..`.
apSingleForall :: forall a c fs. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
apSingleForall = Sub $ unApSingleForall $ metamorph @_ @fs @c @FlipConst @Proxy @(ApSingleForall c a) @Proxy Proxy empty uncons cons $ Proxy
  where empty _ = ApSingleForall Dict
        uncons _ _ = FlipConst Proxy
        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
             => Label ℓ -> FlipConst (Proxy τ) (ApSingleForall c a ρ)
             -> ApSingleForall c a (Extend ℓ τ ρ)
        cons _ (FlipConst (ApSingleForall Dict)) = case frontExtendsDict @ℓ @τ @ρ of
          FrontExtendsDict Dict -> ApSingleForall Dict
            \\ apSingleExtendSwap @ℓ @a @ρ @τ
            \\ uniqueApSingle @(Extend ℓ τ ρ) @a

With this entailment in hand, we can now write extractSingle in terms of erase:

extractSingle f = erase @(ActsOn c x) @ (ApSingle fs x) @y go
  \\ apSingleForall @x @c @fs
  where
    go :: forall a. ActsOn c x a => a -> y
    go a = case actsOn @c @x @a of As' -> f a

I haven't played with it, but maybe we can use a similar trick for map.

EDIT: I don't think this can be made to work with map because map specifies that the output is Map f r.

[woehr]

I've added the value-level functions I need in open-adt to the pull request. I wish I had more time to look work on writing the functions (where possible) in terms of existing row-types functions, but I unfortunately don't. One day I hope to come back to this, but for now they're all written in terms of metamorph.

The eraseZipSingle has a more complicated "zip function" than erase. I went with this because I need to know which label shows up first (the left or the right), to use eraseZipSingle to implement my Ord1 instance.

I've been able to rework open-adt to use these functions (yay!). There is just one function I'm still trying to fix type errors in, but I'm fairly sure it's unrelated to these changes.

[dwincort]

Awesome work! I suggested a few changes, but I do understand if you don't have time to work on this right now — my life has been hectic recently too (note how it's taken me nearly a week to get back to your latest changes). What would you rather see:

1. We leave this PR open, and you can make changes when you get the time.

2. We leave this PR open, and I'll make a PR on your branch, where I make some of the changes I have in mind.

3. We go ahead and merge this PR, and I'll make another PR soon to address my own comments.

[dwincort]

This type seems a little crazy. In the case that the variant isn't at the same label, I understand the desire to know which one "comes first" — I do the same thing in the Ord instance for Var at the top of this module — but I'm not sure it's a good call for a public function like this. I wonder if there's a more general eraseZip that I've been missing too, like where the given function is of type like:

forall a b. c a => Either (Label, a, a) ((Label, a), (Label, b)) -> c

With this generalEraseZip, we could recover eraseZip pretty easily:

eraseZip f = generalEraseZip $ \case
  Left (_, a, b) -> Just (f a b)
  Right _ -> Nothing

And then we could also use it in the Ord instance by doing:

compare = generalEraseZip $ \case
  Left (_, a, b) -> compare a b
  Right ((la,_),(lb,_)) -> compare (show la, show lb)

One really nice thing about this is that it's safe to reordering, meaning that if we change row-types in the future so that rows aren't necessarily ordered alphabetically be label, the meaning of compare won't suddenly change.

Anyway, I think a similar thing can be done for eraseZipSingle (or possibly the ApSingle version could be written in terms of generalEraseZip via the ActsOn trick I talked about in a previous comment).

[woehr]

Awesome work! I suggested a few changes, but I do understand if you don't have time to work on this right now — my life has been hectic recently too (note how it's taken me nearly a week to get back to your latest changes). What would you rather see:

1. We leave this PR open, and you can make changes when you get the time.
2. We leave this PR open, and I'll make a PR on your branch, where I make some of the changes I have in mind.
3. We go ahead and merge this PR, and I'll make another PR soon to address my own comments.

I'm happy to proceed with option 1! I think I'll have time this weekend to address your comments.

If once this pull request is merged you'd like to make further improvements (such as implementing the ActsOn trick), please don't let me hold those changes back. As much as I'd like to figure that out myself, it's unfortunately not a priority right now.

[woehr]

I think with my latest push, the comments you've made are addressed. Let me know if there are any other changes you'd like.

[dwincort]

Thanks a ton for putting in the effort to get all this done! It looks like there's something fishy with the CI, but that's not the fault of this PR, so I'm going to go ahead and merge.

FYI, I've been really busy with work recently, but I do have a couple of other things I want to do before cutting the next release. If that's problematic for you, please let me know and I'll see what I can do.