按类型级自然排序

Question

我一直在尝试使用 DataKinds 扩展在 Haskell 中实现类型级别的自然属性。到目前为止，我的代码如下所示：

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

-- the kind of natural numbers
data Nat = Zero | Succ Nat

-- type synonyms for the naturals
type N0 = Zero
type N1 = Succ N0
type N2 = Succ N1
-- ...

-- singleton natural type
data SNat (n :: Nat) where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

-- type level lesser-than operator
type family (<) (x :: Nat) (y :: Nat) :: Bool where
    x < Zero = False
    Zero < y = True
    (Succ x) < (Succ y) = x < y

-- type level addition operator
type family (+) (x :: Nat) (y :: Nat) :: Nat where
    Zero + y = y
    x + Zero = x
    (Succ x) + y = Succ (x + y)
    x + (Succ y) = Succ (x + y)

infixr 5 :::
-- type of vectors with a certain length
data Vector (n :: Nat) a where
    Nil :: Vector N0 a
    (:::) :: a -> Vector n a -> Vector (Succ n) a

-- indexing operator
(!) :: ((k < n) ~ True) => Vector n a -> SNat k -> a
(x ::: _) ! SZero = x
(_ ::: xs) ! (SSucc n) = xs ! n

此代码编译良好并且按预期工作（在预期时也会出现类型错误）。

> (1 ::: 2 ::: 3 ::: Nil) ! (SSucc SZero)
2
> (1 ::: Nil) ! (SSucc SZero)
Couldn't match type 'False with 'True....

但是，如果我从这里更改上面的行之一：

(:::) :: a -> Vector n a -> Vector (Succ n) a

到这里：

(:::) :: a -> Vector n a -> Vector (n + N1) a

文件突然无法编译：

Could not deduce ((n2 < n1) ~ 'True)
from the context ((k < n) ~ 'True)
  bound by the type signature for
             (!) :: (k < n) ~ 'True => Vector n a -> SNat k -> a
  at question.hs:41:8-52
or from (n ~ (n1 + N1))
  bound by a pattern with constructor
             ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + N1) a,
           in an equation for ‘!’
  at question.hs:43:2-9
or from (k ~ 'Succ n2)
  bound by a pattern with constructor
             SSucc :: forall (n :: Nat). SNat n -> SNat ('Succ n),
           in an equation for ‘!’
  at question.hs:43:15-21
Relevant bindings include
  n :: SNat n2 (bound at question.hs:43:21)
  xs :: Vector n1 a (bound at question.hs:43:8)
In the expression: xs ! n
In an equation for ‘!’: (_ ::: xs) ! (SSucc n) = xs ! n

为什么 Haskell 能够推断出 n < Succ n 而不是 n < n + N1？在这种情况下，如何使我的类型函数正常运行？ （我宁愿不必使用unsafeCoerce）。

Answer 1

您可以通过减少 (+) 类型族的定义来使用更改的类型签名进行编译：

-- type level addition operator
type family (+) (x :: Nat) (y :: Nat) :: Nat where
    -- Zero + y = y
    x + Zero = x
    -- (Succ x) + y = Succ (x + y)
    x + (Succ y) = Succ (x + y)

使用您的原始定义，(n + N1) 无法减少，因为 GHC 不知道它可以应用哪些方程式；第一个可能适用，具体取决于 n 是否为 Zero。

使用缩减版很明显（在将 N1 缩减为其定义之后）只有 x + Succ y 规则可以应用，因此 GHC 能够将您的新类型缩减为原始类型。

实际上，通过对 first 参数的案例分析来定义像 (+) 这样的操作更正常，而不是像我在这里所做的那样。这将使(N1 + n) 之类的东西起作用，但(n + N1) 不起作用。但是我认为这只是一种惯例，并没有任何特定的优势。

通过同时拥有两组定义，您通常会得到两全其美的结果。