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 :)