Patching an isomorphic structure

[schell]

I have a remote data structure that is isomorphic to the local structure I'm diff'ing and I'd like to use the edit script to patch the remote structure (in an effect-full way). @eelco - in your paper you describe the edit script referring to an internal stack that pushes and pops subtrees from the source and target tree. Is there any more information about that process you could provide me?

[schell]

@kosmikus, @ggreif - I realize @eelco may not be watching this repo. If you know how to get in touch with him please let me know - thank you! :)

[ggreif]

@schell you might get inspirations from my slides http://bobkonf.de/2015/slides/greif.pdf
Anyway, extending patch to effectful operation is on my agenda (especially when deletions must be reified effectfully, which I haven't so far managed to emulate in terms of stock patch).

[schell]

@ggreif thank you! This looks great. I'll let you know if I have questions. Is that okay?

[ggreif]

@schell yea, sure, keep asking!

[schell]

👍

[schell]

I'm definitely interested in the polymorphic containers addition - is that available now? Are there any examples you have of using located values?

I'm a little confused about calling diff on an (IO Configtree) - how can diff compare IO actions?

[ggreif]

@schell regarding IO you only ever diff purely packed values, where unsafePerformIO is safe :-). Then IO is "just like" a polymorphic Id functor. patch is a different issue, altogether.
For polymorphic containers you need -XRankNTypes IIRC. You start like this:

data Fam t ts where
  Just' :: Fam el elts -> Fam (Maybe el) elts
  Nothing' :: Fam (Maybe el) CNil

Writing the Family instance is pretty straightforward, Type is a bit tricky. Please look at the other open issue to get some hints. I have to run now, but if you wish I can set up a gist later (or add to the wiki?).
One more hint: I do not have a satisfying story for decEq on Nothing', since there is nothing we can delegate the decision to. I currently use unsafeCoerce Refl for this, but I also considered adding a Typeable constraint and an eqT test.

[schell]

Thank you! And yes, please start the wiki, that would be very helpful.

[ggreif]

@schell I have written https://github.com/eelco/gdiff/wiki/PolymorphicContainers. For now it explains [a], but Maybe should be the same, unless you want the optimization Just' :: Fam a ts -> Fam (Maybe a) ts which needs the Meta constructor descriptor, which is not on mainline (yet?).

[eelco]

@schell I’m still watching the repository, but @ggreif is doing excellent work and is way more on top of it (thanks!)

[schell]

Thank you :)

[schell]

@ggreif I think I've come up with another way of doing polymorphic containers without unsafeCoerce. By adding a qualifying type variable and one more constructor to the initial data type we can encode the values within the polymorphic type, and then we need some constraints on the Family and Type instances:

data ListFam a t ts where
    Nil'  :: ListFam a [a] Nil
    Cons' :: ListFam a a Nil -> ListFam a [a] (a `Cons` [a] `Cons` Nil)
    Val'  :: a -> ListFam a a Nil

instance (Eq a, Show a) => Family (ListFam a) where
    decEq (Cons' a) (Cons' a') = do (Refl, Refl) <- decEq a a'; Just (Refl, Refl)
    decEq Nil' Nil' = Just (Refl, Refl)
    decEq (Val' a) (Val' a') | a == a'   = Just (Refl, Refl)
                             | otherwise = Nothing
    decEq _ _ = Nothing

    fields (Cons' _) (a:as) = Just (a `CCons` as `CCons` CNil)
    fields Nil' [] = Just CNil
    fields (Val' _) _ = Just CNil
    fields _ _ = Nothing

    apply (Cons' _) (a `CCons` as `CCons` CNil) = a : as
    apply Nil'  CNil = []
    apply (Val' a) CNil = a

    string (Cons' _) = "Cons"
    string (Val' a)  = show a
    string Nil'      = "Nil"

instance (Eq a, Show a) => Type (ListFam a) a where
    constructors = [Abstr Val']

instance (Eq a, Show a) => Type (ListFam a) [a] where
    constructors = [ Concr Nil', Abstr $ \(x : _) -> Cons' $ Val' x ]

After that it's business as usual as far as I can tell.
I'm still working on a way of transforming a Editscript (ListFam a) [a] [a] into a EditScript (ListFam b) [b] [b]. I thought it would be as easy as

fmapEditList f (Ins (Val' a) es) = Ins (Val' $ f a) (fmapEditList f es)
fmapEditList f (Cpy (Val' a) es) = Cpy (Val' $ f a) (fmapEditList f es)
fmapEditList f (Del (Val' a) es) = Del (Val' $ f a) (fmapEditList f es)
fmapEditList f (CpyTree es) = CpyTree $ fmapEditList f es

But it isn't! Thoughts?

[schell]

I guess since the types in the AST can be heterogeneous, a transformation may not be possible. I'm not sure...

[ggreif]

@schell I think what is tripping you over are the List ListFam ts constraints that live in Ins and co. I suggest writing a slightly more complex function that also gives back a Dict (List ListFam) ts constraint reified as a value and pattern match on that. For Dict see the "dirt-eliminator" branch in my fork, or ekmett's constraints library.
But in this simple case you might get away with specifying

List (ListFam b) (b `Cons` [b] `Cons` Nil)

on your fmap's signature. You probably have to also check for Nil' etc. there.

[rvl]

Hi @schell, I am trying to do exactly the same thing. Did you have any success patching the isomorphic structure, or even just defining fmapEditList?