Is there a notion of "heterogenous collection of a given shape"?

Question

A common pattern in functional programming languages with a sufficiently advanced type system to to have a type of "heterogeneous lists". For instance, given a list defined as:

data List a = Nil | Cons a (List a)

(Note: For concreteness, I will use Idris in this question, but this could also be answered in Haskell (with the right extensions), Agda, etc...)

We can define HList:

data HList : List a -> Type where
  Nil  : HList []
  (::) : a -> HList as -> HList (a :: as) 

This is a list which holds a different type (specified by the type-level List a) at each "position" of the List data type. This made me wonder: Can we generalize this construction? For instance, given a simple tree-like structure:

data Tree a = Branch a [Tree a]

Does it make sense to define a heterogenous tree?

where HTree : Tree a -> Type where
   ...

More generally in a dependently-typed language, is it possible to define a general construction:

data Hetero : (f : Type -> Type) -> f a -> Type where
   ....

that takes a data type of kind Type -> Type and returns the "heterogeneous container" of shape f? Has anyone made use of this construction before if possible?

Answer 1

We can talk about the shape of any functor using map and propositional equality. In Idris 2:

Hetero : (f : Type -> Type) -> Functor f => f Type -> Type
Hetero f tys = (x : f (A : Type ** A) ** map fst x = tys)

The type (A : Type ** A) is the type of non-empty types, in other words, values of arbitrary type. We get heterogeneous collections by putting arbitrarily typed values into functors, then constraining the types elementwise to particular types.

Some examples:

ex1 : Hetero List [Bool, Nat, Bool]
ex1 = ([(_  ** True), (_ ** 10), (_ ** False)] ** Refl)

data Tree : Type -> Type where
  Leaf : a -> Tree a
  Node : Tree a -> Tree a -> Tree a

Functor Tree where
  map f (Leaf a)   = Leaf (f a)
  map f (Node l r) = Node (map f l) (map f r)

ex2 : Hetero Tree (Node (Leaf Bool) (Leaf Nat))
ex2 = (Node (Leaf (_ ** False)) (Leaf (_ ** 10)) ** Refl)