GADT的类型约束不足，无法处理不可预测的数据 [英] Weaken GADTs type constraints to deal with unpredictable data

问题描述

我正在尝试利用GADT来限制类型，但是在编译期间无法处理某些依赖项，例如用户输入.让我们考虑以下AVL树定义:

I am trying to make use of GADTs to have well constrained types, but some dependencies are impossible to handle during compilation time – for example user input. Let's consider following AVL tree definition:

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树都得到很好的平衡.我可以定义一些基本功能，例如

Magic of GADTs ensures that every AVL tree is well balanced. I can define some basic functions like

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

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

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

Now I would like to write program that will read n numbers, insert them into AVL tree and return in order (assuming that these functions are defined):

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的合理方法-这是我不知道要插入多少个元素的信息.

because type (depth) of the tree is going to change along with every insert. I understand what is happening here, but I don't see any reasonable way to use this AVL while handling input "online" – that is without any knowledge of how many elements I am going to insert.

有什么解决方案可以让我为这种情况抽象出树的深度吗?即使AVL太复杂了，这个问题也适用于编译时大小的向量和矩阵.现在，我只能解决硬编码的任务，这使我的程序变得完全不灵活.

Is there any solution that would allow me to abstract out tree's depth for this case? Even if AVL is too complicated example, this problem applies also to compile-time-sized vectors and matrices. For now I can solve only hardcoded tasks, which makes my programs completely inflexible.

推荐答案

您可以使用其他GADT隐藏树的深度. (这被称为存在类型.)

You can use another GADT to hide the depth of the tree. (This is called an existential type.)

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

具有可在SomeAVL上运行的包装器:

With wrappers to operate on SomeAVLs:

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

这篇关于GADT的类型约束不足，无法处理不可预测的数据的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！