haskell - 固定大小的完美平衡树的问题

Question

我尝试实现一个完美平衡的二叉搜索树，其中大小作为类型参数给出(就像 C++ 的 std::array 所做的那样)。

这是树的实现:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeNats
import Data.Foldable hiding (length)
import Data.Monoid
import Data.Proxy


data MultiSet (n :: Nat) a where
    Leaf :: MultiSet 0 a
    Odd :: MultiSet n a -> a -> MultiSet n a -> MultiSet (n+n+1) a
    Even :: MultiSet n a -> a -> a -> MultiSet n a -> MultiSet (n+n+2) a

这是 minView 的实现，与 containers 包中的 Data.Set 类似:

minView :: MultiSet (n+1) a -> (a, MultiSet n a) 
minView (Odd Leaf x Leaf) = (x, Leaf)
minView (Even Leaf x y Leaf) = (x, Odd Leaf y Leaf)
minView (Odd l x r) = let
    (u, l') = minView l
    (v, r') = minView r
    in (u, Even l' x v r')
minView (Even l x y r) = let
    (u, l') = minView l
    in (u, Odd (insert x l') y r)

但是当我尝试解释它时会出现许多错误:

PerfectBalance.hs:71:33: error:
    • Could not deduce: n ~ 0
    from the context: (n + 1) ~ ((n5 + n5) + 1)
        bound by a pattern with constructor:
                Odd :: forall (n :: Nat) a.
                        MultiSet n a -> a -> MultiSet n a -> MultiSet ((n + n) + 1) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:71:10-24
    or from: n5 ~ 0
        bound by a pattern with constructor:
                Leaf :: forall a. MultiSet 0 a,
                in an equation for ‘minView’
        at PerfectBalance.hs:71:14-17
    ‘n’ is a rigid type variable bound by
        the type signature for:
        minView :: forall (n :: Nat) a.
                    MultiSet (n + 1) a -> (a, MultiSet n a)
        at PerfectBalance.hs:70:1-48
    Expected type: MultiSet n a
        Actual type: MultiSet 0 a
    • In the expression: Leaf
    In the expression: (x, Leaf)
    In an equation for ‘minView’: minView (Odd Leaf x Leaf) = (x, Leaf)
    • Relevant bindings include
        minView :: MultiSet (n + 1) a -> (a, MultiSet n a)
        (bound at PerfectBalance.hs:71:1)
|
71 | minView (Odd Leaf x Leaf) = (x, Leaf)
|                                 ^^^^

PerfectBalance.hs:72:36: error:
    • Could not deduce: n ~ 1
    from the context: (n + 1) ~ ((n5 + n5) + 2)
        bound by a pattern with constructor:
                Even :: forall (n :: Nat) a.
                        MultiSet n a -> a -> a -> MultiSet n a -> MultiSet ((n + n) + 2) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:72:10-27
    or from: n5 ~ 0
        bound by a pattern with constructor:
                Leaf :: forall a. MultiSet 0 a,
                in an equation for ‘minView’
        at PerfectBalance.hs:72:15-18
    ‘n’ is a rigid type variable bound by
        the type signature for:
        minView :: forall (n :: Nat) a.
                    MultiSet (n + 1) a -> (a, MultiSet n a)
        at PerfectBalance.hs:70:1-48
    Expected type: MultiSet n a
        Actual type: MultiSet ((0 + 0) + 1) a
    • In the expression: Odd Leaf y Leaf
    In the expression: (x, Odd Leaf y Leaf)
    In an equation for ‘minView’:
        minView (Even Leaf x y Leaf) = (x, Odd Leaf y Leaf)
    • Relevant bindings include
        minView :: MultiSet (n + 1) a -> (a, MultiSet n a)
        (bound at PerfectBalance.hs:71:1)
|
72 | minView (Even Leaf x y Leaf) = (x, Odd Leaf y Leaf)
|                                    ^^^^^^^^^^^^^^^

PerfectBalance.hs:75:23: error:
    • Could not deduce: (n2 + 1) ~ n5
    from the context: (n + 1) ~ ((n5 + n5) + 1)
        bound by a pattern with constructor:
                Odd :: forall (n :: Nat) a.
                        MultiSet n a -> a -> MultiSet n a -> MultiSet ((n + n) + 1) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:73:10-18
    ‘n5’ is a rigid type variable bound by
        a pattern with constructor:
        Odd :: forall (n :: Nat) a.
                MultiSet n a -> a -> MultiSet n a -> MultiSet ((n + n) + 1) a,
        in an equation for ‘minView’
        at PerfectBalance.hs:73:10-18
    Expected type: MultiSet (n2 + 1) a
        Actual type: MultiSet n5 a
    • In the first argument of ‘minView’, namely ‘r’
    In the expression: minView r
    In a pattern binding: (v, r') = minView r
    • Relevant bindings include
        r' :: MultiSet n2 a (bound at PerfectBalance.hs:75:9)
        r :: MultiSet n5 a (bound at PerfectBalance.hs:73:18)
        l :: MultiSet n5 a (bound at PerfectBalance.hs:73:14)
|
75 |     (v, r') = minView r
|                       ^

PerfectBalance.hs:76:12: error:
    • Could not deduce: ((n2 + n2) + 2) ~ n
    from the context: (n + 1) ~ ((n5 + n5) + 1)
        bound by a pattern with constructor:
                Odd :: forall (n :: Nat) a.
                        MultiSet n a -> a -> MultiSet n a -> MultiSet ((n + n) + 1) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:73:10-18
    ‘n’ is a rigid type variable bound by
        the type signature for:
        minView :: forall (n :: Nat) a.
                    MultiSet (n + 1) a -> (a, MultiSet n a)
        at PerfectBalance.hs:70:1-48
    Expected type: MultiSet n a
        Actual type: MultiSet ((n2 + n2) + 2) a
    • In the expression: Even l' x v r'
    In the expression: (u, Even l' x v r')
    In the expression:
        let
        (u, l') = minView l
        (v, r') = minView r
        in (u, Even l' x v r')
    • Relevant bindings include
        l' :: MultiSet n2 a (bound at PerfectBalance.hs:74:9)
        r' :: MultiSet n2 a (bound at PerfectBalance.hs:75:9)
        minView :: MultiSet (n + 1) a -> (a, MultiSet n a)
        (bound at PerfectBalance.hs:71:1)
|
76 |     in (u, Even l' x v r')
|            ^^^^^^^^^^^^^^

PerfectBalance.hs:78:23: error:
    • Could not deduce: (n3 + 1) ~ n5
    from the context: (n + 1) ~ ((n5 + n5) + 2)
        bound by a pattern with constructor:
                Even :: forall (n :: Nat) a.
                        MultiSet n a -> a -> a -> MultiSet n a -> MultiSet ((n + n) + 2) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:77:10-21
    ‘n5’ is a rigid type variable bound by
        a pattern with constructor:
        Even :: forall (n :: Nat) a.
                MultiSet n a -> a -> a -> MultiSet n a -> MultiSet ((n + n) + 2) a,
        in an equation for ‘minView’
        at PerfectBalance.hs:77:10-21
    Expected type: MultiSet (n3 + 1) a
        Actual type: MultiSet n5 a
    • In the first argument of ‘minView’, namely ‘l’
    In the expression: minView l
    In a pattern binding: (u, l') = minView l
    • Relevant bindings include
        l' :: MultiSet n3 a (bound at PerfectBalance.hs:78:9)
        r :: MultiSet n5 a (bound at PerfectBalance.hs:77:21)
        l :: MultiSet n5 a (bound at PerfectBalance.hs:77:15)
|
78 |     (u, l') = minView l
|                       ^

PerfectBalance.hs:79:12: error:
    • Could not deduce: ((n5 + n5) + 1) ~ n
    from the context: (n + 1) ~ ((n5 + n5) + 2)
        bound by a pattern with constructor:
                Even :: forall (n :: Nat) a.
                        MultiSet n a -> a -> a -> MultiSet n a -> MultiSet ((n + n) + 2) a,
                in an equation for ‘minView’
        at PerfectBalance.hs:77:10-21
    ‘n’ is a rigid type variable bound by
        the type signature for:
        minView :: forall (n :: Nat) a.
                    MultiSet (n + 1) a -> (a, MultiSet n a)
        at PerfectBalance.hs:70:1-48
    Expected type: MultiSet n a
        Actual type: MultiSet ((n5 + n5) + 1) a
    • In the expression: Odd (insert x l') y r
    In the expression: (u, Odd (insert x l') y r)
    In the expression:
        let (u, l') = minView l in (u, Odd (insert x l') y r)
    • Relevant bindings include
        r :: MultiSet n5 a (bound at PerfectBalance.hs:77:21)
        l :: MultiSet n5 a (bound at PerfectBalance.hs:77:15)
        minView :: MultiSet (n + 1) a -> (a, MultiSet n a)
        (bound at PerfectBalance.hs:71:1)
|
79 |     in (u, Odd (insert x l') y r)
|            ^^^^^^^^^^^^^^^^^^^^^

maxView、insert和delete也有类似的问题。

如何解决这些问题？

Answer 1

GHC 不懂代数。 任何代数。像n + 1 /= 0之类的东西和n + 1 = m + 1 -> n = m都超出了它。它最多能做的就是评估，例如 1 + 1 = 2 。你必须明确地将它们写成公理，并用 unsafeCoerce 来实现它们，并告诉 GHC 使用它们。 (或者，您可以使用编译器插件将 GHC 连接到求解器，可以进行代数运算并将这些结果转换为公理。)

此外，即使 GHC 可以做代数，在 Odd l x r 中和Even l x y r案例，l, r :: MultiSet m a m = m' + 1 不知道在哪里。也就是说，即使您已经匹配 l和r反对Leaf ，因此“证明” l和r含有不止一种元素，这一点未经 GHC 证明。粗略地说，“l和r非空”背后的推理不够“直接”。失败的匹配不会为您提供有关受审查者的更多类型信息。我会写一个辅助函数:

{-# LANGUAGE AllowAmbiguousTypes, ExplicitForAll, ScopedTypeVariables, TypeApplications #-}
import Data.Proxy
import Data.Type.Equality
import Data.Void
import Unsafe.Coerce

data NatCheck (n :: Nat) where
  IsZero :: NatCheck 0
  IsSucc :: Proxy n -> NatCheck (n + 1)
  -- Proxy lets us bind the predecessor to a name
checkMultiSet :: forall n a. MultiSet n a -> NatCheck n
checkMultiSet Leaf = IsZero
checkMultiSet (Odd _ _ _) = IsSucc Proxy
-- get m :: Nat out of Even, learn n = (m + m) + (1 + 1) from it
-- reassociate: n = ((m + m) + 1) + 1
checkMultiSet (Even (_ :: MultiSet m a) _ _ _) | Refl <- addAssoc @(m + m) @1 @1 = IsSucc Proxy

-- axiom
addAssoc :: forall n m l. ((n + m) + l) :~: (n + (m + l))
addAssoc = unsafeCoerce Refl

并使用它而不是显式使用 MultiSet 的构造函数

{-# LANGUAGE EmptyCase #-}
minView :: forall n a. MultiSet (n + 1) a -> (a, MultiSet n a)
minView Leaf = case natDiscrim @n Refl of { } -- Leaf is not ruled out automatically, have to prove unreachability with axiom n + 1 /= 0
minView (Odd l x r) = -- get m :: Nat, learn n + 1 = m + m + 1, get l, r of size m
  case checkMultiSet l of -- i.e. check m =? 0
    -- learn m = 0, so n + 1 = 0 + 1
    -- injectivity: n = 0
    IsZero | Refl <- succInj @n @0 -> (x, Leaf) 
    -- get m' :: Nat, learn m = m' + 1
    -- get l', r' of size m'
    -- we know n + 1 = (m' + 1) + (m' + 1) + 1
    -- the Even has size ((m' + m') + 2) when it should be n
    -- algebra, except more painfully than ever before
    -- injectivity gets: n = (m' + 1) + (m' + 1)
    -- reassociate: n = ((m' + 1) + m') + 1
    -- commute: n = (m' + (m' + 1)) + 1
    -- reassociate: n = ((m' + m') + 1) + 1
    -- reassociate: n = (m' + m') + (1 + 1)
    IsSucc (Proxy :: Proxy m')
      | (u, l') <- minView l, (v, r') <- minView r
      , Refl <- succInj @n @((m' + 1) + (m' + 1))
      , Refl <- addAssoc @(m' + 1) @m' @1
      , Refl <- addComm @(m' + 1) @m'
      , Refl <- addAssoc @m' @m' @1
      , Refl <- addAssoc @(m' + m') @1 @1
      -> (u, Even l' x v r')
minView (Even (l :: MultiSet m a) x y r) = -- get m :: Nat, learn n + 1 = m + m + 2, get l, r of size m
  case checkMultiSet l of -- i.e. check m =? 0
    -- learn m = 0, so n + 1 = 1 + 1
    -- injectivity: n = 1
    IsZero | Refl <- succInj @n @1 -> (x, Odd Leaf y Leaf)
    -- get m' :: Nat, learn m = m' + 1, get l' of size m'
    -- we know n + 1 = (m + m) + (1 + 1)
    -- the Odd has size ((m + m) + 1) when it should be n
    -- algebra, less painful
    -- reassociate: n + 1 = ((m + m) + 1) + 1
    -- injectivity: n = (m + m) + 1
    IsSucc _
      | (u, l') <- minView l
      , Refl <- addAssoc @(m + m) @1 @1
      , Refl <- succInj @n @(m + m + 1)
      -> (u, Odd (insert x l') y r)

-- more axioms
natDiscrim :: forall n. (n + 1) :~: 0 -> Void
natDiscrim Refl = error "natDiscrim: impossible"
succInj :: forall n m. (n + 1) ~ (m + 1) => n :~: m
succInj = unsafeCoerce Refl
addComm :: forall n m. (n + m) :~: (m + n)
addComm = unsafeCoerce Refl

当然，您可以通过例如暴力破解来代替向 GHC 解释代数。更换 Odd 中的守卫 block , IsSucc案例 Refl <- unsafeCoerce Refl :: n ~ (m' + m' + 2) ，对于其他人也是如此。但我不会这样做，因为这是否正确并不明显。相比之下，公理显然是正确的。通过用它们来做代数，你也证明了你的推理是正确的。