haskell - 如何通过类型级奇偶校验找到 Natural 的前身？

Question

我一直在使用带有附加类型级奇偶校验信息的自然数。 succ 已以最直接的方式成功实现:

succ :: Natural p -> Natural (Opp p)
succ = Succ

但是，我仍然在努力让 pred 进行类型检查。一个最小的例子:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

data Parity = Even | Odd

type family Opp (p :: Parity) = (r :: Parity) | r -> p where
  Opp 'Odd = 'Even
  Opp 'Even = 'Odd

data Natural :: Parity -> * where
  Zero :: Natural 'Even
  Succ :: Natural p -> Natural (Opp p)

pred :: Natural (Opp p) -> Natural p
pred (Succ n) = n

如何才能成功实现 pred？现在我遇到了许多不同的大型且复杂的类型错误，尤其是无法推断出Opp p ~ p1。

Answer 1

给定奇偶校验的单例:

data SParity :: Parity -> Type where
  SEven :: SParity Even
  SOdd :: SParity Odd

我们可以证明Opp的单射性

oppInj' :: Opp p ~ Opp q => SParity p -> SParity q -> p :~: q
oppInj' SEven SEven = Refl
oppInj' SOdd SOdd = Refl

现在我们可以定义:

data Natural' :: Parity -> Type where
  Zero' :: Natural' Even
  Succ' :: SParity p -> Natural' p -> Natural' (Opp p)
pred' :: SParity p -> Natural' (Opp p) -> Natural' p
pred' p (Succ' q n) = case oppInj' p q of Refl -> n

您可以安全地执行删除以清除所有单例垃圾:

-- for maximum symmetry, instead of relying on type applications we could
-- just substitute Proxy# in place of SParity everywhere, but meh
oppInj :: forall p q. Opp p ~ Opp q => p :~: q
oppInj = unsafeCoerce Refl -- we know this is OK because oppInj' exists
data Natural :: Parity -> Type where
  Zero :: Natural Even
  Succ :: Natural p -> Natural (Opp p)
pred :: forall p. Natural (Opp p) -> Natural p
pred (Succ (n :: Natural q)) = case oppInj @p @q of Refl -> n

这种模式，用单例做一些事情，然后删除它们以改善空间和时间(这里它只是一个常数因子)在 Haskell 中进行依赖类型编程时很常见。通常，您不会编写 Natural' 或 pred'，但它们对于编写删除版本很有用。

PS:确保处理零情况!