削弱GADT类型约束以处理不可预测的用户输入

Question

我正在尝试使用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是一个太复杂的例子,这个问题也适用于编译时大小的向量和矩阵.现在我只能解决硬编码任务,这使我的程序完全不灵活.

Answer 1

您可以使用另一个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)