Folding over the closure of child types

[expipiplus1]

Take for example, this language of literals, type-annotated expressions and kind annotated types.

data Expr h
  = ExprLit Int
  | -- | ExprAdd (h :# Expr) (h :# Expr)
    ExprAnn (h :# Expr) (h :# Type)
  deriving stock (Generic)

data Type h
  = TypeUnit
  | TypeAnn (h :# Type) (h :# Kind)

type Kind :: AHyperType -> Data.Kind.Type
data Kind h
  = KindStar

makeHNodes ''Expr
makeHFunctor ''Expr
makeHNodes ''Type
makeHFunctor ''Type
makeHNodes ''Kind
makeHFunctor ''Kind
instance RNodes Expr
instance RNodes Type
instance RNodes Kind
instance (c Kind) => Recursively c Kind
instance (c Kind, c Type) => Recursively c Type
instance (c Kind, c Type, c Expr) => Recursively c Expr

If we want to perform a fold over an Expr we have to do a little dance with HRecWitness, deconstructing it recursively.

showE' :: Pure # Expr -> String
showE' = fold \case
  HRecSelf -> \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t
  HRecSub (HWitness W_Expr_Expr) HRecSelf -> \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t
  HRecSub (HWitness W_Expr_Type) HRecSelf -> \case
    TypeUnit -> "()"
    TypeAnn (Const t) (Const k) -> t <> " : " <> k
  ...

One can mechanically derive a GADT representing the closure of the HWitness relation, which makes defining these folds much more pleasant:

withWitnessClosure
  :: forall e t p a
   . (Recursively (WitnessClosure e) e)
  => (HWitnessClosure e t -> t # p -> a)
  -> HRecWitness e t
  -> t # p
  -> a
withWitnessClosure f = Proxy @(WitnessClosure e) ##>> f inClosure

type WitnessClosure :: HyperType -> HyperType -> Constraint
class WitnessClosure e t where
  inClosure :: HWitnessClosure e t

instance WitnessClosure Expr Expr where inClosure = E
instance WitnessClosure Expr Type where inClosure = T
instance WitnessClosure Expr Kind where inClosure = K

type HWitnessClosure :: HyperType -> HyperType -> Data.Kind.Type
data family HWitnessClosure a b
data instance HWitnessClosure Expr a where
  E :: HWitnessClosure Expr Expr
  T :: HWitnessClosure Expr Type
  K :: HWitnessClosure Expr Kind

-- Used thusly:
showE :: Pure # Expr -> String
showE =
  fold
    ( withWitnessClosure \case
        E -> \case
          ExprLit i -> show i
          ExprAnn (Const e) (Const t) -> e <> " : " <> t
        T -> \case
          TypeUnit -> "()"
          TypeAnn (Const a) (Const b) -> a <> " : " <> b
        K -> \case
          KindStar -> "*"
    )

Does this construct have a place in hypertypes, or is this actually quite an unidiomatic way of performing such a fold?

It seems like defining a Showable class and writing instances for Expr, Type and Kind might be the "proper" way to go? Something like:

type Showable :: HyperType -> Constraint
class Showable h where
  show' :: h # Const String -> String

instance Showable Expr where
  show' = \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t

instance Showable Type where
  show' = \case
    TypeUnit -> "()"
    TypeAnn (Const a) (Const b) -> a <> " : " <> b

instance Showable Kind where
  show' = \case
    KindStar -> "*"

showE' :: Pure # Expr -> String
showE' = fold $ Proxy @Showable ##>> show'

[yairchu]

It seems like defining a Showable class and writing instances for Expr, Type and Kind might be the "proper" way to go?

Yes, that's how I usually do it.

Another theoretical benefit of this approach is that if there was another expression language typed with Type, or another type language kinded with Kind, then you would have reused for the show' implementations rather than repeating in the cases.

That being said, I can definitely see the ergonomic usefulness of your GADT approach. If there was a TH generator for it then one would need to do less work in cases like these and it would make using the library easier. It's kind of a flattened version of HRecWitness, and reminds me of join too. It would definitely be useful to have :)

[expipiplus1]

I haven't tested this yet, but something along these lines should work, if the hypertypes internals were exposed then I think this could duplicate less logic

{-# INLINE withClosureWitness #-}
withClosureWitness ::
  forall s t p a.
  (Recursively (Closure s) s) =>
  (ClosureWitness s t -> t # p -> a) ->
  HRecWitness s t ->
  t # p ->
  a
withClosureWitness f = Proxy @(Closure s) ##>> f inClosure

type Closure :: HyperType -> HyperType -> Constraint
class Closure s t where
  inClosure :: ClosureWitness s t

type ClosureWitness :: HyperType -> HyperType -> Type
data family ClosureWitness s t

deriveClosureWitness :: Name -> DecsQ
deriveClosureWitness n = do
  ds <- hyperDepsRec n
  let ws =
        ds <&> \d ->
          (d, mkName ("CW_" <> nameBase n <> "_" <> nameBase d))
  is <-
    join
      <$> for ws \(d, w) -> [d|instance Closure $(conT n) $(conT d) where inClosure = $(conE w)|]
  g <- do
    a <- newName "a"
    let t = DConT ''ClosureWitness `DAppT` DConT n `DAppT` DVarT a
        cs =
          ws <&> \(d, w) ->
            let ct = DConT ''ClosureWitness `DAppT` DConT n `DAppT` DConT d
             in DCon [] [] w (DNormalC False []) ct
    pure $ DDataInstD Data [] Nothing t Nothing cs []
  pure (sweeten [g] <> is)

-- All the child hypertypes
hyperDepsRec :: Name -> Q [Name]
hyperDepsRec = closeM' hyperDeps

hyperDeps :: Name -> Q [Name]
hyperDeps n = do
  d <-
    dsReify n >>= \case
      Just (DTyConI d _) -> pure d
      Just i -> fail ("Expected a type, but " <> show n <> " is a " <> dInfoSummary i)
      Nothing -> fail ("Couldn't reify " <> show n)
  case d of
    DDataD _ _ _ vs _ cons _ -> do
      h <-
        maybe
          (fail (show n <> " doesn't have any type variables, is it a hypertype?"))
          ( \case
              DPlainTV v _ -> pure v
              DKindedTV v _ _ -> pure v
          )
          (lastMay vs)
      let ts = conFieldTypes =<< cons
      let hs = getHyperTypes h =<< ts
      pure hs
    _ -> fail (show n <> " isn't a data type")

-- The hypertypes contained in a type, for example (Either (h :# A) (h :# B))
-- contains A and B
getHyperTypes :: Name -> DType -> [Name]
getHyperTypes h = go
 where
  go =
    \case
      DConT hash `DAppT` DVarT h' `DAppT` DConT t
        | hash == ''(:#), h' == h -> pure t
      DForallT _ t -> go t
      DConstrainedT _ t -> go t
      DAppT t1 t2 -> go t1 <> go t2
      DAppKindT t _ -> go t
      DSigT t _ -> go t
      DVarT _ -> []
      DConT _ -> []
      DArrowT -> []
      DLitT _ -> []
      DWildCardT -> []

conFieldTypes :: DCon -> [DType]
conFieldTypes (DCon _ _ _ f _) = case f of
  DNormalC _ ts -> ts ^.. each . _2
  DRecC vs -> vs ^.. each . _3

dInfoSummary :: DInfo -> String
dInfoSummary = \case
  DTyConI{} -> "type"
  DVarI{} -> "value"
  DTyVarI{} -> "type variable"
  DPrimTyConI{} -> "primitive type"
  DPatSynI{} -> "pattern cinnamon"

--
-- Utils
--

-- Reflexive, transitive closure, on lists
closeM' :: (Ord a, Monad m) => (a -> m [a]) -> a -> m [a]
closeM' f = fmap Set.toList . closeM (fmap Set.fromList . f)

-- Reflexive, transitive closure
closeM :: (Ord a, Monad m) => (a -> m (Set a)) -> a -> m (Set a)
closeM f x = go (Set.singleton x) =<< f x
 where
  go seen next | Set.null next = pure seen
  go seen next = do
    novel <-
      (`Set.difference` seen)
        . Set.unions
        <$> traverse f (toList next)
    go (seen <> next) novel

data Foo h = Foo Int (Either (h :# Baz) (h :# Bar))
data Bar h = Bar Int (h :# Foo)
data Baz h = Baz Int (h :# Foo)

-- deriveClosureWitness ''Foo
data instance ClosureWitness Foo a_a8mpv
  where
    CW_Foo_Bar :: ClosureWitness Foo Bar
    CW_Foo_Baz :: ClosureWitness Foo Baz
    CW_Foo_Foo :: ClosureWitness Foo Foo
instance Closure Foo Bar where
  inClosure = CW_Foo_Bar
instance Closure Foo Baz where
  inClosure = CW_Foo_Baz
instance Closure Foo Foo where
  inClosure = CW_Foo_Foo

Another theoretical benefit of this approach is that if there was another expression language typed with Type, or another type language kinded with Kind, then you would have reused for the show' implementations rather than repeating in the cases.

Yeah, this is a strong motivation for doing it that way indeed