以数据类型编码二叉搜索树

问题描述

因此，我一直在尝试在 Idris 中以一种新的数据类型对二叉搜索树（而不仅仅是二叉树）的属性进行编码。

如果只使用数据类型（例如在 repl 中）来创建新树，它似乎工作得相当好。

这是目前的数据类型，它接收一个类型和那个类型的Maybe，基本上就是这棵树的最大值。函数 isLMaybe 和 isGMaybe 用于检查子树的值是否大于或小于根值。

isLMaybe: Ord a => Maybe a -> a -> Bool
isLMaybe nothing _ = True
isLMaybe (Just x) y = x < y

isGMaybe: Ord a => Maybe a -> a -> Bool
isGMaybe nothing _ = True
isGMaybe (Just x) y = x > y

data BST: (x: Type) -> Maybe x -> Type where
  EmptyBST: Ord a => BST a nothing
  NodeBST: Ord a => (l: BST a b) -> (v: a) -> (r: BST a c) -> {auto leftValues: So (isLMaybe b v)} -> {auto rightValues: So (isGMaybe c v)} -> BST a (Just v)

问题是，一旦我尝试创建一个插入函数，如下所示，它会抛出以下错误：

insertTest : (a: Type,c: Maybe a,d: Maybe a) => (x: a) -> BST a c -> BST a d
insertTest x EmptyBST = NodeBST EmptyBST x EmptyBST
insertTest x (NodeBST l v r) = case lessEqualGreater x v of
                                     L => NodeBST (insertTest x l) v r
                                     E => NodeBST l v r
                                     G => NodeBST l v (insertTest x r)
                                     N => NodeBST l v r

When checking right hand side of insertTest with expected type
             BST a d
     
     Type mismatch between
             BST a (Just x) (Type of NodeBST EmptyBST x EmptyBST)
     and
             BST a d (Expected type)
     
     Specifically:
             Type mismatch between
                     Just x
             and
                     d

我不明白为什么它认为 d 不是 Maybe a 的实例，因为在我得到错误之后，我试图将它明确地放入函数中，但我仍然得到同样的错误.

解决方法

您提供的类型签名并不代表您的想法。

insertTest : (a: Type,c: Maybe a,d: Maybe a) => (x: a) -> BST a c -> BST a d

此函数必须能够为 d 的任何可能值生成一个值。不只是Just x。如果使用 insertTest 调用 {d=Nothing} 会发生什么？也许看看依赖对？

idris idris idris