haskell - 按类型级别自然排序

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 能够将您的新类型减少到原始类型。

定义像 (+)这样的操作其实更正常通过对第一个参数的案例分析，而不是我在这里所做的第二个。那会让事情像 (N1 + n)工作但不工作 (n + N1) .但是，我认为这只是一种约定，而不具有任何特定优势。

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