如何通过类型级别的奇偶校验检查找到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？现在，我遇到了许多不同的大型和复杂类型错误，尤其是could not deduce Opp p ~ p1。

Answer 1

给定的单身人士Parity：

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：请务必处理Zero此案！

Answer 2

如@chi所示，

除了允许某些类型被认为是模棱两可的类型外，GHC不会将注入性注释用于任何事情。只为了那个。他们不习惯，正如人们所期望的，推断a ~ b的F a ~ F b。就我个人而言，我认为它们以当前形式几乎是无用的。

因此，您必须定义Natural一些不同的地方：

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

现在，您可以获得所需的两个东西。