弱化 GADT 类型约束以处理不可预测的数据

我试图利用 GADT 来获得良好的约束类型，但某些依赖项在编译期间无法处理 - 例如用户输入。让我们考虑以下 AVL 树定义：

data Zero
data S a

data AVL depth where
  Nil :: AVL Zero
  LNode :: AVL n -> Int -> AVL (S n) -> AVL (S (S n))
  RNode :: AVL (S n) -> Int -> AVL n -> AVL (S (S n))
  MNode :: AVL n -> Int -> AVL n -> AVL (S n)

GADT 的魔力确保每棵 AVL 树都保持良好的平衡。我可以定义一些基本功能，例如

singleton :: a -> AVL (S Zero) x
singleton a = MNode Nil a Nil

insert :: a -> AVL n a -> AVL (S n) a
insert = ...

现在我想编写一个程序来读取n数字，将它们插入AVL树并按顺序返回（假设定义了这些函数）：

main = IO ()
main = do
  (n :: Int) <- readInt  -- some IO defined somewhere
  (inp :: [Int]) <- readInts
  let avl = foldl (\tree x -> insert x tree) Nil inp
  print $ toList avl

显然我得到了错误：

    • Couldn't match type ‘S Zero’ with ‘Zero’
      Expected type: AVL Zero
        Actual type: AVL (S Zero)

因为树的类型（深度）会随着每个insert。我明白这里发生了什么，但我没有看到任何合理的方法来在处理“在线”输入时使用此 AVL - 即不知道我要插入多少元素。

有没有任何解决方案可以让我抽象出这种情况下树的深度？即使 AVL 是一个过于复杂的示例，这个问题也适用于编译时大小的向量和矩阵。目前我只能解决硬编码的任务，这使得我的程序完全不灵活。

您可以使用另一个 GADT 来隐藏树的深度。 （这称为存在类型。）

data SomeAVL a where
  SomeAVL :: AVL n a -> SomeAVL a

带有可操作的包装器SomeAVLs:

insert' :: a -> SomeAVL a -> SomeAVL a
insert' a (SomeAVL t) = SomeAVL (insert a t)