Is it possible to construct record from function?

[michaelmesser]

If I have f :: (forall r. (RElem r rs (RIndex r rs)) => proxy r -> b r and I know the rs at compile time. Is it possible to construct a Rec b rs? I was thinking I could rmap a Rec Proxy rs but I could not get the RElem constraint to work.

[acowley]

Here are two approaches:

1. Create a type class like RElem but with the arguments in the reverse order, then use rpureConstrained to build the record.

class r ∈ rs => ElemOf rs r where
instance r ∈ rs => ElemOf rs r where

fromWitnesses' :: forall rs b.
                  (AllConstrained (ElemOf rs) rs, RecApplicative rs)
               => (forall r. (r ∈ rs) => b r) -> Rec b rs
fromWitnesses' f = rpureConstrained (Proxy @(ElemOf rs)) f

2. Write the recursion yourself in a typeclass, capturing the membership dictionary in a Dict-like value. This is a lot like foldRec from the CoRec module (that is in the process of moving into vinyl from Frames).

data Wit rs r where Wit :: r ∈ rs => Wit rs r
class Witnesses ss ts where
  witnesses :: Rec (Wit ss) ts
instance Witnesses ss '[] where
  witnesses = RNil
instance (Witnesses ss ts, t ∈ ss) => Witnesses ss (t ': ts) where
  witnesses = Wit :& witnesses

fromWitnesses :: forall rs b. Witnesses rs rs
              => (forall r. r ∈ rs => b r) -> Rec b rs
fromWitnesses f = rmap aux witnesses
  where aux :: Wit rs r -> b r
        aux Wit = f

[michaelmesser]

@acowley Where are AllConstrained and rpureConstrained defined? Searching stackage and this repo gives no results. The second piece of code works. Thanks

[acowley]

Sorry, I was using the CoRec branch. They're probably adapted from Frames. Getting that branch ready is taking me a little time as I'm trying to figure out exactly what to include, but those two things will be there.

[michaelmesser]

type family FRec f a where
    FRec _ '[] = '[]
    FRec f ('(l,t) : r) = '(l, f t) : FRec f r

class FunctorMaybe f where
    fmapMaybe :: (a -> Maybe b) -> f a -> f b

g :: forall l v f us rs. (KnownSymbol l, us ~ FRec Maybe rs, FunctorMaybe f, l ::: Maybe v ∈ us) => Proxy rs -> Label l -> f (FieldRec us) -> ElField (l ::: f v)
g _ _ r = Field (fmapMaybe (getField . rget (Proxy @(l ::: Maybe v))) r)

Any ideas on how to turn g into a record? I tried to use the fromWitnesses function but was not getting anywhere. The record I end up with should have type FieldRec (FRec f rs). Or is there a better way to reach my goal of writing the function FunctorMaybe f => f (FieldRec (FRec Maybe rs)) -> FieldRec (FRec f rs)?

[acowley]

FunctorMaybe seems unusual to me, can you give me an example instance? I'm curious.

On with the show, do you think you could work with Rec (Maybe :. ElField) rs records instead of FieldRec (FRec Maybe rs)? I'm finding FRec gets in the way of the type checker's happiness, so maybe treating our functor as a composite would work for you. I realize this is a bit different, because rather than, say, "foo" ::: Maybe a, we have Maybe ("foo" ::: a).

What I was able to come up with is this,

class (a ~ '(Fst a, Snd a), a ∈ fs, FieldType (Fst a) fs ~ Snd a)
      => KnownFieldElem fs a where
instance (KnownSymbol l, (l ::: v) ∈ fs, FieldType l fs ~ v)
         => KnownFieldElem fs (l ::: v) where

goal :: forall f rs.
        (FunctorMaybe f, RecApplicative rs,
         AllConstrained (KnownFieldElem rs) rs)
     => f (Rec (Maybe :. ElField) rs) -> Rec (f :. ElField) rs
goal x = rpureConstrained (Proxy :: Proxy (KnownFieldElem rs))
                          (Compose (fmapMaybe (getCompose . rgetf Label) x))

But note that I didn't write it so compactly for the first few iterations. The second argument to rpureConstrained, I wrote originally as an auxiliary definition in a where clause,

  where aux :: forall a. (KnownFieldElem rs a, HasField (Fst a) rs (Snd a))
            => f (ElField a)
        aux = fmapMaybe (getCompose . rgetf Label) x

That let me write down the type of an individual element, and let me figure out what constraints I needed.

The main technique here is the use of rpureConstrained which requires that we be able to write a constraint former (i.e. something of kind * -> Constraint), so we define a class and the one instance we should ever need.

I also don't know if goal works as I've only type checked it.

[michaelmesser]

@acowley https://github.com/reflex-frp/reflex/blob/c56abf28018161cac6c8042fecec21dda669c5f4/src/Reflex/FunctorMaybe.hs I was hoping to use FieldRec instead of using :.. It should be possible with a modified version Witness but the closest I got was this:

data Wit rs f r where
    Wit :: forall l v rs f r. (r ~ (l ::: f v), KnownSymbol l, r ∈ (FRec f rs)) => Wit rs f r

class Witnesses ss f ts where
    witnesses :: Rec (Wit ss f) ts
instance Witnesses ss f '[] where
    witnesses = RNil
instance (Witnesses ss f ts, KnownSymbol l, (l ::: f v) ∈ (FRec f ss)) => Witnesses ss f ((l ::: f v) ': ts) where
    witnesses = Wit :& witnesses

fromWitnesses :: forall f rs b. Witnesses rs Maybe (FRec Maybe rs) => Proxy rs
    -> (forall l v. (KnownSymbol l, l ::: Maybe v ∈ (FRec Maybe rs)) => ElField (l ::: f v))
    -> FieldRec (FRec f rs)
fromWitnesses _ q = undefined
    where aux :: Wit rs Maybe '(l, Maybe v) -> ElField '(l, f v)
          aux Wit = q

g :: forall l v f us rs. (KnownSymbol l, us ~ FRec Maybe rs, FunctorMaybe f, l ::: Maybe v ∈ us) => Proxy rs -> Label l -> f (FieldRec us) -> ElField (l ::: f v)
g _ _ r = Field (fmapMaybe (getField . rget (Proxy @(l ::: Maybe v))) r)

h :: (Witnesses rs Maybe (FRec Maybe rs), FunctorMaybe f) => Proxy rs -> f (FieldRec (FRec Maybe rs)) -> FieldRec (FRec f rs)
h p r = fromWitnesses p (g p Label r)

I don't know what to put for undefined.

[acowley]

I'd really recommend you reconsider using the composition of functors. Pushing the functor into the field types makes it much harder to work with. If you do need to stay with a Rec ElField type, you can use this to push the functor argument down into the fields of the record.

hideF :: (Functor f, AllConstrained KnownField rs)
      => Rec (f :. ElField) rs -> FieldRec (FRec f rs)
hideF RNil = RNil
hideF (Compose x :& xs) = Field (fmap getField x) :& hideF xs

[michaelmesser]

@acowley Thanks. I think you are right about the composition of functors. Maybe in Idris what I was hoping for would be possible.

[acowley]

Note that we have the function you wanted by composing hideF . goal, but the issue of pushing the functor into the fields is more of a design question.

Since it’s the same functor for every field, mentioning it once has some appeal on the efficiency front. But doing so also makes using natural transformations more straightforward with something like rmap because we can very concisely write that the functor is changing, but the field types to which that functor is applied remain the same. By pulling out the common part of every field, we can write functions on that common part without the individual field types getting in the way.

[michaelmesser]

@acowley Functor composition makes constructing and getting/setting fields more tedious. I also would need an unhideF function to go from FieldRec (FRec Maybe rs) to Rec (Maybe :. ElField) rs to get the function I truly want. I tried to write it but failed because ghc could not figure out that FRec Maybe rs ~ [] implies that rs ~ [].

[michaelmesser]

I finally got unhideF to work.

class (frs ~ FRec f rs) => UnhideF f rs frs where
    unhideF :: FieldRec (FRec f rs) -> Rec (f :. ElField) rs
instance UnhideF f '[] '[] where
    unhideF RNil = RNil
instance (Functor f, UnhideF f rs frs) => UnhideF f ('(l,a):rs) ('(l,f a):frs) where
    unhideF (Field x :& xs) = Compose (fmap Field x) :& unhideF xs