是否有“给定形状的异构集合”的概念？

如何解决是否有“给定形状的异构集合”的概念？

函数式编程语言中的一种常见模式，具有足够先进的类型系统以具有“异构列表”的类型。例如，给定一个列表定义为：

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

（注意：为了具体起见，我将在这个问题中使用 Idris，但这也可以在 Haskell（具有正确的扩展名）、Agda 等中回答...）

我们可以定义HList：

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

这是一个列表，它在 List a 数据类型的每个“位置”保存不同的类型（由类型级别 List 指定）。这让我想知道：我们可以概括这个结构吗？例如，给定一个简单的树状结构：

data Tree a = Branch a [Tree a]

定义异构树有意义吗？

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

更一般地说，在依赖类型的语言中，是否可以定义一般构造：

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

采用 Type -> Type 类型的数据类型并返回形状为 f 的“异构容器”？如果可能的话，以前有人使用过这种结构吗？

解决方法

我们可以使用 map 和命题等式来讨论任何函子的形状。在伊德里斯 2 中：

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

类型(A : Type ** A)是非空类型的类型，即任意类型的值。我们通过将任意类型的值放入函子中，然后将类型元素限制为特定类型来获得异构集合。

一些例子：

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)