在Idris中如何为二叉搜索树数据类型强制实现顺序合法性约束

问题核心原因 #

你遇到的问题本质出在mkIsLft/mkIsRgt的实现上：这类用于构造So实例的工具函数（通常是Data.So模块提供的mkSo）底层是通过believe_me实现的，仅会在运行时校验布尔值是否为True，校验失败就抛出运行时错误，但编译阶段不会做任何静态校验，这才让错误的插入逻辑通过了编译，并不是So类型本身允许构造So False的实例。

这种用So包裹布尔运算做约束的方案本身就不适合实现编译期的静态校验：布尔运算的结果对Idris的类型系统是不透明的，你没有给出对应的命题证明，自然没法靠类型系统拦住逻辑错误。

正确实现思路 #

在Idris中实现类似Liquid Haskell的精化类型约束，更合适的方案是把BST的顺序约束直接嵌入到类型结构中，为二叉树增加上下界类型参数，不需要额外单独定义IsBST谓词：

-- 带上下界约束的二叉搜索树，minBound是允许的最小值（Nothing表示无下界），maxBound是允许的最大值（Nothing表示无上界）
data BST : Ord a => (minBound : Maybe a) -> (maxBound : Maybe a) -> Type where
  -- 空树满足任意边界约束
  Leaf : BST min max
  -- 节点构造要求：
  -- 1. 当前值在上下界范围内
  -- 2. 左子树的上界为当前值，即左子树所有节点≤当前值
  -- 3. 右子树的下界为当前值，即右子树所有节点>当前值
  Node : Ord a => (val : a) ->
         (So (case minBound of Nothing => True; Just low => val >= low)) ->
         (So (case maxBound of Nothing => True; Just high => val < high)) ->
         (left : BST minBound (Just val)) ->
         (right : BST (Just val) maxBound) ->
         BST minBound maxBound

-- 对外暴露的无边界约束的BST类型
ValidBST : Ord a => Type
ValidBST a = BST {a} Nothing Nothing

这种实现下，插入函数的逻辑如果出错（比如把大于当前节点的值插入左子树），类型检查器会直接报错：左子树的上界是当前节点值，插入的新值大于该上界，无法构造出满足范围约束的证明，编译直接不通过，完全不需要等到运行时。

如果你想要进一步避免So的使用，可以把Ord的比较操作替换为自定义的可判定命题类型，这样所有约束证明都可以在编译期自动推导，完全不需要手动构造So实例，安全性更高。

内容的提问来源于stack exchange，提问作者Lucas Tornai