我试图实现一个完全平衡的二进制搜索树，其中大小作为类型参数给定(就像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也存在类似的问题。
我该如何解决这些问题？
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解释代数，不如强行使用它，例如用Refl <- unsafeCoerce Refl :: n ~ (m' + m' + 2)替换Odd、IsSucc情况下的保护块，其他情况也一样。不过我不会这么做，因为这并不明显是正确的。相反，这些公理显然是正确的。通过用它们做代数运算，你也证明了你的推理是正确的。