How can I constrain Vinyl / Composite Records?

Question

I have an extensible Vinyl / Composite record (similar to HList, Frames...), and I would like to generate the tuples of keys/values, such as

tuplify '[String :-> Whatevs, ...] :: [(String, String)]

This is surprisingly hard. original gist.

Solution Gist, thanks to Alec below

type FA = "a" :-> String
type FB = "b" :-> Int
type AB = '[FA, FB]

ab :: Rec Identity AB
ab = "A" :*: 1 :*: RNil

tuplify :: (Show a) => Rec Identity '[a] -> [(String, String)]
tuplify = recordToList . rmap undefined -- ??????
-- tuplify ab = [("a", "A"), ("b", "1")]

If you care to try out what I've done so far, check out that gist, and it has well-thought-out examples and the errors I see:

Here is the hardware for refying in Composite (reifyDicts):

And the same for Vinyl (reifyConstraints):

AFAICT, the problem is that in something like rmap:

rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs

The mapped fn is defined forall x, but my tuplify is constrained, and I think the reification should move the constraint into the type (that's what Dicts are for), but, alas, no luck so far.

Answer 1

I can't get composite related stuff to install on my global Stack setup but the following should still work (I just copy-pasted relevant definitions). That said, I think a simple type-class based dispatch based on type is simpler here (since the constraints are non-trivial). With all of the right extensions enabled [1], you just need:

class Tuplify a where
  tuplify :: a -> [(String, String)]

instance Tuplify (Rec Identity '[]) where
  tuplify RNil = []

instance (Show t, KnownSymbol s, Tuplify (Rec Identity rs)) =>
           Tuplify (Rec Identity (s :-> t ': rs)) where
  tuplify (v :*: rs) = (symbolVal (Proxy :: Proxy s), show v) : tuplify rs

Then, in GHCi:

ghci> tuplify ab
[("a","\"A\""),("b","1")]

---

If you really want to try the reifying constraint approach, you'll have to start by declaring a type class and instance for the particular constraint you want:

class ShowField a where 
  showField :: a -> (String, String)                                                                                

instance (KnownSymbol s, Show a) => ShowField (Identity (s :-> a)) where
  showField (Identity (Val v)) = (symbolVal (Proxy :: Proxy s), show v)

Then it becomes more straightforward to use reifyConstraints and rmap:

tuplify' :: RecAll Identity rs ShowField => Rec Identity rs -> [(String, String)]
tuplify' xs = recordToList
            . rmap (\(Vinyl.Compose (Dict x)) -> Vinyl.Const $ showField x)
            $ reifyConstraint (Proxy :: Proxy ShowField) xs

I imagine something similar is possible with reifyDicts, although I wish there was a variant of it defined using ValuesAllHave instead of just AllHave (then we could bypass declaring a ShowField typeclass and do everything in just a function).

---

[1] extensions needed for first example

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}