Added a function for universal instantiation over constrained rows…

[gnumonik]

…, along with a supporting data type (Constrained) and type class (Known) to Data.Row.Records. This is an awkward place for it, but it doesn't seem like there's anywhere else where it could be put.

Motivation: Sometimes you have Forall r c, KnownSymbol l, and HasType l t r in scope, but you need c t. Since Forall r c means what it says, it should be possible to derive c t, but doing so can be surprisingly tricky. I came up with this solution when working on my row-extras library and then realized it would actually fit in here without much disruption.

If there actually is a more straightforward way to do this without these changes, please let me know. I tried pretty hard for quite some time and couldn't come up with anything...

Notes on the implementation:

• I don't think there's a way to do this without Known. Can't use default because it wants a function of type forall a. c a => a and we need something like forall a. c a => Proxy a. Can't use defaultA because applicatives then we'd lose kind polymorphism, can't build anything better out of fromLabels or fromLabelsA or fromLabelsMapA for the same reasons. This seems like the simplest solution.

• Constrained is kind of stupid but I don't see a way out of it. You can't partially apply a Dict c and you sure can't compose a Dict with a partially applied constraint so we need that stupidity.

• I have no idea what the performance hit of generating the HasType l t r :- c t entailment in the forall function is. Even if it's noticeable, I still think you should consider adding this. If you're going to give someone a universal quantifier, you ought to give them a way to instantiate it :)

• I don't think this needs any tests. If constraint entailment works the way the documentation for Data.Constraints says it does, and if the forall function is total (it is), this will do what it looks like it does.

• Arguably, something like:

-- | Produce the dictionary for (c t) directly when @(HasType l t r, Forall r c, KnownSymbol l,..etc)@
-- are satisfied. 
ui :: forall l c r t 
      . (  WellBehaved r
        ,  WellBehaved (Map Proxy r)
        ,  Forall (Map Proxy r) Known
        ,  Forall r c 
        ,  KnownSymbol l 
        ,  HasType l t r 
      ) => Dict (c t)
ui = mapDict (forall @r @c @l @t) Dict 

Might be better to expose to users than forall?

[dwincort]

This is very cool, and thanks so much for upstreaming! I have a busy weekend, so it might take me a few days to get to this, but I definitely will.

[dwincort]

If I'm reading your code correctly, the basic idea is that you create a record containing a Dict c t for every t in the row-type, and then you index into that record to grab the Dict at the particular label you care about. This is a pretty clever solution, and it doesn't require any axioms (that is, like stuff from Data.Row.Dictionaries) that don't already exist.

That said, the implementation feels a little frustrating and round-about. Why should we need to make the Dict c t for every element when we only want one of them (admittedly, laziness might save us here, but still)? Why should we need Record at all?

I took a stab at the problem by trying to write this directly in Data.Row.Internal, and I came up with the following:

forall :: forall r c l t. (Forall r c, KnownSymbol l) => HasType l t r :- c t
forall = unmapDict go
  where
    go :: Dict (HasType l t r) -> Dict (c t)
    go Dict = getConst $ metamorph @_ @r @c @Either @Proxy @(Const (Dict (c t))) @(Const (Dict (c t)))
      Proxy empty doUncons doCons Proxy
      where
        empty = error "Impossible"
        doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
           => Label ℓ -> Proxy ρ -> Either (Proxy (ρ .- ℓ)) (Const (Dict (c t)) τ)
        doUncons _ _ = case sameSymbol @l @ℓ Proxy Proxy of
          Just Refl -> Right $ Const $ UNSAFE.unsafeCoerce $ Dict @(c τ)
          Nothing -> Left Proxy
        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (Const (Dict (c t)) ρ) (Const (Dict (c t)) τ) -> Const (Dict (c t)) (Extend ℓ τ ρ)
        doCons _ (Left (Const Dict))  = Const Dict
        doCons _ (Right (Const Dict)) = Const Dict

I don't mind having the error "Impossible" for the empty case — this is essentially the same thing done in Variants — but the unsafeCoerce is pretty irritating. The issue is that we can show that l and ℓ are equal with sameSymbol, but that doesn't mean we can show that t and τ are equal (even though we know they must be).

I'd be okay adding an axiom to Dictionaries, but I don't know what it would be. The obvious choice is something like (HasType l t r, HasTyle l t' r) :- (t ~ t'), but that doesn't actually help us here. We know that HasType ℓ τ ρ and HasType l t r, but we don't have type information about how r and ρ are related. I tried changing the f type of metamorph from Proxy to some sort of Dict-carrying newtype that would carry HasType l t ρ, but I couldn't quite make that work either. I may give it another shot though...

Anyway, I'm currently leaning toward this version of forall because it presents a nicer interface (no reliance on records and fewer necessary constraints) even though it uses an unsafeCoerce under the hood (after all, most of this library is clever use of unsafeCoerce 🙃 ). What do you think?

[gnumonik]

Hi,

I agree that the implementation is frustrating and roundabout. I'd been playing with versions that use unsafeCoerce in roughly the way your version does before coming up with the code in this PR. To be honest I just wanted to see if I could write it without unsafeCoerce or any new axioms, since it seemed like it should be possible.

I can't think of an axiom that would actually help here. Having said that, the axiom you proposed above, or something like it, seems like it would be a useful addition to the library, and I have something similar in row-extras:

unique :: forall l t t' r 
        . (HasType l t r
        ,  HasType l t' r
        ,  AllUniqueLabels r) 
       => t :~: t' 
unique = UNSAFE.unsafeCoerce Refl 

Or maybe this would be more useful, not sure:

newtype UniquenessProof l t r 
  = UniquenessProof {proveUnique :: forall t'. HasType l t' r => t :~: t}

mkUniquenessProof :: forall l t r 
                   . (HasType l t r, AllUniqueLabels r) 
                   => UniquenessProof l t r 
mkUniquenessProof = UniquenessProof go 
  where 
    go :: forall t'. HasType l t' r => t :~: t' 
    go = unique @l @t @t' @r 

Back to the main issue: I think the problem (that we don't have any type information about the relation between r and ρ) is just a consequence of the way that Forall / metamorph are defined, which is a bit annoying since r and ρ obviously are related. Actually, this problem is the whole reason why row-extras exists. Unless I'm missing something (I might be! I'm just a self-taught guy who does this for fun while I look for an entry level Haskell job...), you'd have to define metamorph differently in order to make the relation apparent to GHC.

I hacked this together pretty quickly but it should give you an idea of what I mean:

-- you could shove this into Data.Row.Internal
class ForallX (r :: Row k) (c :: Symbol -> k -> Constraint) -- (c' :: Symbol -> Constraint) 
  where
  metamorphX :: forall (p :: * -> * -> *) 
                       (f :: Row k -> *) 
                       (g :: Row k -> *) 
                       (h :: k -> *)
             . Bifunctor p
            => Proxy (Proxy h, Proxy p)
            -> (f Empty -> g Empty)
               -- ^ The way to transform the empty element
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c ℓ τ, HasType ℓ τ ρ)
               => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
               -- ^ The unfold
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c ℓ τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
               => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
               -- ^ The fold   
            -> f r  -- ^ The input structure
            -> g r 

instance ForallX (R '[]) c  where
  {-# INLINE metamorphX #-}
  metamorphX _ empty _ _ = empty

instance (KnownSymbol ℓ, c ℓ τ, ForallX ('R ρ) c, FrontExtends ℓ τ ('R ρ), AllUniqueLabels (Extend ℓ τ ('R ρ))) => ForallX ('R (ℓ :-> τ ': ρ) :: Row k) c where
  {-# INLINE metamorphX #-}
  metamorphX h empty uncons cons = case frontExtendsDict @ℓ @τ @('R ρ) of
    FrontExtendsDict Dict ->
      cons (Label @ℓ) . first (metamorphX @_ @('R ρ) @c h empty uncons cons) . uncons (Label @ℓ)


type ForallC :: forall k. Row k -> (k -> Constraint) -> Symbol -> k -> Constraint 
class (HasType l t r, c t) => ForallC r c l t 
instance (HasType l t r, c t) => ForallC r c l t 

forallC :: forall r c l t. ForallC r c l t => Dict (HasType l t r, c t)
forallC = Dict 

-- | Any structure over a row in which every element is similarly constrained can
-- be metamorphized into another structure over the same row.
class ForallX r (ForallC r c) => Forall (r :: Row k) (c :: k -> Constraint) where
  metamorph :: forall (p :: * -> * -> *) (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *). Bifunctor p
            => Proxy (Proxy h, Proxy p)
            -> (f Empty -> g Empty)
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ r, HasType ℓ τ ρ) -- note the "HasType ℓ τ r", which gives us the relation we need (I think?)
               => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
               => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
            -> f r  
            -> g r
  metamorph h empty uncons cons = metamorphX @_ @r @(ForallC r c) @p @f @g h empty (goUncons uncons) (goCons cons) 
    where 
      goUncons :: forall l t p' 
                . (KnownSymbol l
                  , ForallC r c l t
                  , HasType l t p') 
                => (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k)
                    . (KnownSymbol ℓ
                    , c τ
                    , HasType ℓ τ r
                    , HasType ℓ τ ρ)
                        => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
                -> Label l -> f p' -> p (f (p' .- l)) (h t)
      goUncons f l fp = f l fp 

      goCons :: forall l t p' 
              . ( KnownSymbol l 
                , FrontExtends l t p'
                , ForallC r c l t
                , AllUniqueLabels (Extend l t p')) 
              => (forall ℓ τ ρ
                    . (KnownSymbol ℓ
                    , c τ
                    , FrontExtends ℓ τ ρ
                    , AllUniqueLabels (Extend ℓ τ ρ))
                    => Label ℓ 
                    -> p (g ρ) (h τ) 
                    -> g (Extend ℓ τ ρ))
              -> Label l 
              -> p (g p') (h t) 
              -> g (Extend l t p')
      goCons f l p = f l p 

instance ForallX r (ForallC r c) => Forall (r :: Row k) (c :: k -> Constraint) 

Unfortunately you can't just drop that in as a replacement for the Forall that's in the library right now because it breaks (at least) mapForall and apSingleForall. I don't see a reason why they couldn't be fixed, but it seemed difficult and I didn't really try that hard :)

(Another approach might be to have a quantified constraint superclass on Forall, e.g. (forall (l :: Symbol) (t :: Type). HasType l t r => c t) => Forall r c. I might play with that this week and see if it can work.)

Anyway, the point of all of this is: If you don't think it would be wise to make changes to Forall \ metamorph, then I think your version is probably the best one that can be written. I'm honestly not sure whether there would be any substantial benefit to a strengthened metamorph for most library users. From a theoretical point of view, the stronger version does seem nicer though.

P.S. - Entirely unrelated, but do you plan to move from * to Type or switch to standalone kind signatures? I'd be happy to do the work of updating the library for either of those changes, if only to make it more convenient for me to hack on :)

Edit: Pretty sure you can't make it work with a quantified constraint superclass.

[gnumonik]

I had a burst of inspiration today and managed to get everything working with the "stronger" version of Forall defined in terms of ForallX a la my last comment. Here's the comparison if you wanted to check that out: https://github.com/target/row-types/compare/master...gnumonik:master

That lets you write:

forall :: forall r c l t. (Forall r c, KnownSymbol l) => HasType l t r :- c t
forall = unmapDict go
  where
    go :: Dict (HasType l t r) -> Dict (c t)
    go Dict = getConst $ metamorph @_ @r @c @Either @Proxy @(Const (Dict (c t))) @(Const (Dict (c t)))
      Proxy empty doUncons doCons Proxy
      where
        empty = error "Impossible"

        doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ, HasType ℓ τ r)
           => Label ℓ -> Proxy ρ -> Either (Proxy (ρ .- ℓ)) (Const (Dict (c t)) τ)
        doUncons _ _ = case sameSymbol @l @ℓ Proxy Proxy of
          Just Refl -> Right $ Const Dict 
          Nothing -> Left Proxy

        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (Const (Dict (c t)) ρ) (Const (Dict (c t)) τ) -> Const (Dict (c t)) (Extend ℓ τ ρ)
        doCons _ (Left (Const Dict))  = Const Dict
        doCons _ (Right (Const Dict)) = Const Dict

I'm happy to open another PR and close this one if those changes look sane to you. I think it's also possible to make an analogously stronger version of BiForall and integrate it, but that'll probably take a bit longer than this did.

[gnumonik]

I just couldn't step away from this. Turns out BiForall is easy (relatively speaking...):

-- would go in Data.Row.Internal

class (HasType l t1 r1, HasType l t2 r2, c t1 t2) => BiForallC r1 r2 c l t1 t2 
instance  (HasType l t1 r1, HasType l t2 r2, c t1 t2) => BiForallC r1 r2 c l t1 t2 

class BiForallX (r1 :: Row k1) (r2 :: Row k2) (c :: Symbol -> k1 -> k2 -> Constraint) where
  -- | A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold).
  biMetamorphX :: forall (p :: * -> * -> *) (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
                        (h :: k1 -> k2 -> *). Bifunctor p
              => Proxy (Proxy h, Proxy p)
              -> (f Empty Empty -> g Empty Empty)
              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c ℓ τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2)
                  => Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
              -> (forall ℓ τ1 τ2 ρ1 ρ2. ( KnownSymbol ℓ
                                        , c ℓ τ1 τ2
                                        , FrontExtends ℓ τ1 ρ1
                                        , FrontExtends ℓ τ2 ρ2
                                        , AllUniqueLabels (Extend ℓ τ1 ρ1)
                                        , AllUniqueLabels (Extend ℓ τ2 ρ2))
                  => Label ℓ 
                  -> p (g ρ1 ρ2) (h τ1 τ2) 
                  -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
                  -> f r1 r2 
                  -> g r1 r2

instance BiForallX (R '[]) (R '[]) c1 where
  {-# INLINE biMetamorphX #-}
  biMetamorphX _ empty _ _ = empty

instance ( KnownSymbol ℓ
         , c ℓ τ1 τ2 
         , BiForallX ('R ρ1) ('R ρ2) c
         , FrontExtends ℓ τ1 ('R ρ1)
         , FrontExtends ℓ τ2 ('R ρ2)
         , AllUniqueLabels (Extend ℓ τ1 ('R ρ1))
         , AllUniqueLabels (Extend ℓ τ2 ('R ρ2)))
      => BiForallX ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)) c where
  {-# INLINE biMetamorphX #-}
  biMetamorphX h empty uncons cons = case (frontExtendsDict @ℓ @τ1 @('R ρ1), frontExtendsDict @ℓ @τ2 @('R ρ2)) of
    (FrontExtendsDict Dict, FrontExtendsDict Dict) ->
      cons (Label @ℓ) . first (biMetamorphX @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons) . uncons (Label @ℓ)


-- | Any structure over two rows in which the elements of each row satisfy some
--   constraints can be metamorphized into another structure over both of the
--   rows.
class BiForallX r1 r2 (BiForallC r1 r2 c) => BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) where
  -- | A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold).
  biMetamorph :: forall (p :: * -> * -> *) (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
                        (h :: k1 -> k2 -> *). Bifunctor p
              => Proxy (Proxy h, Proxy p)
              -> (f Empty Empty -> g Empty Empty)
              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2, HasType ℓ τ1 r1, HasType ℓ τ2 r2)
                  => Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1, FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1), AllUniqueLabels (Extend ℓ τ2 ρ2))
                  => Label ℓ -> p (g ρ1 ρ2) (h τ1 τ2) -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
              -> f r1 r2 -> g r1 r2
  biMetamorph h empty uncons cons = biMetamorphX @_ @_ @r1 @r2 @(BiForallC r1 r2 c) @p @f @g @h h empty uncons cons


instance BiForallX r1 r2 (BiForallC r1 r2 c) => BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint)

data BiProxy :: forall k1 k2. k1 -> k2 -> * where 
  BiProxy :: BiProxy a b 

data BiConst :: forall k1 k2. * -> k1 -> k2 -> * where 
  BiConst :: forall k1 k2 (a :: *) (j :: k1) (k :: k2). {getBiConst :: a} -> BiConst a j k  

biForall :: forall r1 r2 c l t1 t2  
          . (BiForall r1 r2 c, KnownSymbol l) 
         => (HasType l t1 r1, HasType l t2 r2) :- c t1 t2 
biForall = unmapDict go 
  where 
    go :: Dict (HasType l t1 r1, HasType l t2 r2) -> Dict (c t1 t2)
    go Dict = getBiConst $ biMetamorph @_ @_ @r1 @r2 @c @Either @BiProxy @(BiConst (Dict (c t1 t2))) @(BiConst (Dict (c t1 t2)))
                Proxy empty doUncons doCons BiProxy 
      where 
        empty = error "Impossible"

        doUncons :: forall ℓ τ1 τ2 ρ1 ρ2
                  . (KnownSymbol ℓ
                  , c τ1 τ2
                  , HasType ℓ τ1 ρ1
                  , HasType ℓ τ2 ρ2
                  , HasType ℓ τ1 r1   -- note these  
                  , HasType ℓ τ2 r2)  -- two lines  
                  => Label ℓ
                  -> BiProxy ρ1 ρ2
                  -> Either (BiProxy (ρ1 .- ℓ) (ρ2 .- ℓ)) (BiConst (Dict (c t1 t2)) τ1 τ2)
        doUncons _ BiProxy = case sameSymbol @l @ℓ Proxy Proxy of 
          Just Refl -> Right $ BiConst Dict
          Nothing   -> Left BiProxy 

        doCons :: forall ℓ τ1 τ2 ρ1 ρ2
                . (KnownSymbol ℓ
                , c τ1 τ2
                , FrontExtends ℓ τ1 ρ1
                , FrontExtends ℓ τ2 ρ2
                , AllUniqueLabels (Extend ℓ τ1 ρ1)
                , AllUniqueLabels (Extend ℓ τ2 ρ2)) 
               => Label ℓ
               -> Either (BiConst (Dict (c t1 t2)) ρ1 ρ2) (BiConst (Dict (c t1 t2)) τ1 τ2)
               -> BiConst (Dict (c t1 t2)) (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
        doCons _ (Left (BiConst Dict)) = BiConst Dict 
        doCons _ (Right (BiConst Dict)) = BiConst Dict 

That upgrades BiForall and makes it easy to write a biForall instantiation function for relations between rows.

I didn't originally intend to propose such significant changes, so let me know what you think when you get a chance to look at this. Probably this should be a new PR, but I'll wait for your feedback.

[dwincort]

@gnumonik Hey, I just wanted to apologize for taking so long to respond. I haven't forgotten about you, but I just have a bunch of other stuff on my plate right now.

[gnumonik]

@dwincort No worries about taking a while to respond.

Sorry to pile one more thing on (but I'll definitely forget if I don't mention it now):

Why isn't the type signature for metamorph (the version that's in the library now) this?

  metamorph :: forall (p :: * -> * -> *) (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *). Bifunctor p
            => Proxy (Proxy h, Proxy p)
            -> (f Empty -> g Empty)
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ, Forall ρ c) -- Note the Forall ρ c 
               => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, Forall ρ c, AllUniqueLabels (Extend ℓ τ ρ)) -- Note the  Forall ρ c 
               => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
            -> f r  
            -> g r

This apparently compiles just fine and doesn't seem to break anything. I ran into a (very very odd) circumstance where I needed (I think) those Forall ρ c constraints and baking them into metamorph was the only way to get them.

BTW: Saving one unsafeCoerce probably isn't a good enough reason to move to ForallX, but the fact that you can express the subset relation in terms of it might be. Every element in p is an element in r === ForallX p (ForallC r Unconstrained1). Can do some fun things with that, but I'll wait for feedback before elaborating.