Subtrees with existentially quantified types

[ggreif]

Neither the Concr nor the Abstr ways of describing the subtrees of a value allow existentially typed subtrees. I have come up with a new way, but I would like to know how others have tackled this problem. I'd gladly follow up with a pull request (a 2-liner) if there is no known good practice for this.

[ggreif]

To resolve the cliff-hanger... The critical commit is https://github.com/ggreif/gdiff/commit/578b18250d9952a3196eeb7677058597e3e84d52 but it is not a pull-request yet. The idea is to solve the problem of the exposure of subtree types ts (which is forbidden for existentially abstracted types) by appealing to another layer of indirection. See the Meta thingy. Comments welcome.

[ggreif]

pull request #8 contains a small example, here is a more elaborate one:

{-#  LANGUAGE FlexibleContexts, ScopedTypeVariables  #-}

data Hidden = forall t ts . Type Fam t => Hide t (Fam t ts)

data Fam ft ts where
  Hidden' :: Fam t ts -> Fam Hidden ts
  False' :: Fam Bool Nil
  True' :: Fam Bool Nil

instance Family Fam where
  False' `decEq` False' = Just (Refl, Refl)
  True' `decEq` True' = Just (Refl, Refl)
  Hidden' l `decEq` Hidden' r = do (Refl, Refl) <- l `decEq` r; Just (Refl, Refl)
  _ `decEq` _ = Nothing

  fields False' False = Just CNil
  fields True' True = Just CNil
  fields (Hidden' fam) (Hide a fam') = do (Refl, Refl) <- fam `decEq` fam'; fields fam a
  fields _ _ = Nothing

  string False' = "F"
  string True' = "T"
  string (Hidden' a) = "[" ++ string a ++ "]"

instance Type Fam Hidden where
  constructors = [Meta $ \(Hide (a :: t) _) -> head $ [ Concr (Hidden' con)
                                                      | Concr con :: Con Fam t <- constructors
                                                      , Just _ <- [fields con a]
                                                      ]
                 ]

instance Type Fam Bool where
  constructors = [Concr False', Concr True']

hDiff :: Hidden -> Hidden -> EditScript Fam Hidden Hidden
hDiff = diff

Here the result: *Data.Generic.Diff> Hide True True' hDiff Hide True True' Cpy [T] $ End *Data.Generic.Diff> Hide True True' hDiff Hide False False' Ins [F] $ Del [T] $ End

I am cheating a little bit by embedding a family member in the Hide constructor, but it is only needed for convincing the type checker. It could be obtained with the same technique as in instance Type Fam Hidden on the fly in fields.

[ggreif]

Okay, for posterity, here is the complete code with the trick mentioned in my previous comment:

{-#  LANGUAGE FlexibleContexts, ScopedTypeVariables  #-}

data Hidden = forall t ts . Type Fam t => Hide t

data Fam ft ts where
  Hidden' :: Fam t ts -> Fam Hidden ts
  False' :: Fam Bool Nil
  True' :: Fam Bool Nil

instance Family Fam where
  False' `decEq` False' = Just (Refl, Refl)
  True' `decEq` True' = Just (Refl, Refl)
  Hidden' l `decEq` Hidden' r = do (Refl, Refl) <- l `decEq` r; Just (Refl, Refl)
  _ `decEq` _ = Nothing

  fields False' False = Just CNil
  fields True' True = Just CNil
  fields (Hidden' fam) (Hide (a :: t)) = head [ fields fam a
                                              | Concr fam' :: Con Fam t <- constructors
                                              , Just (Refl, Refl) <- [fam `decEq` fam']
                                              ]
  fields _ _ = Nothing

  string False' = "F"
  string True' = "T"
  string (Hidden' a) = "[" ++ string a ++ "]"

instance Type Fam Hidden where
  constructors = [Meta $ \(Hide (a :: t)) -> head $ [ Concr (Hidden' con)
                                                    | Concr con :: Con Fam t <- constructors
                                                    , Just _ <- [fields con a]
                                                    ]
                 ]

instance Type Fam Bool where
  constructors = [Concr False', Concr True']

hDiff :: Hidden -> Hidden -> EditScript Fam Hidden Hidden
hDiff = diff

*Data.Generic.Diff> Hide True hDiff Hide False Ins [F] $ Del [T] $ End

*Data.Generic.Diff> Hide True hDiff Hide True Cpy [T] $ End