弱化 GADTs 类型约束以应对不可预知的数据

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 树并按顺序 return（假设定义了这些函数）：

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)

弱化 GADTs 类型约束以应对不可预知的数据

Weaken GADTs type constraints to deal with unpredictable data

haskell

io

gadt