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