haskell - 见证之前的类型族子句不匹配

Question

我有以下封闭类型系列:

type family IsSpecialSize (n :: Nat) :: Bool where
    IsSpecialSize 8 = True
    IsSpecialSize 16 = True
    IsSpecialSize _ = False

我想为这种类型的族编写一个单例见证者和决策者:

data SSpecial (n :: Nat) where
    SSpecial8 :: SSpecial 8
    SSpecial16 :: SSpecial 16
    SNotSpecial :: (IsSpecialSize n ~ False) => SSpecial n

class DecideSSpecial (n :: Nat) where
    specialSize :: SSpecial n

特殊情况很容易涵盖:

instance {-# OVERLAPPING #-} DecideSSpecial 8 where
    specialSize = SSpecial8

instance {-# OVERLAPPING #-} DecideSSpecial 16 where
    specialSize = SSpecial16

但是，我们在通用实例方面遇到了麻烦。我们不能只写

instance {-# OVERLAPPABLE #-} (KnownNat n) => DecideSSpecial n where
    specialSize = SNotSpecial

因为范围内没有任何内容可以证明IsSpecialSize n ~ False。我们可以尝试将其添加到最后一个实例的上下文中:

instance {-# OVERLAPPABLE #-} (KnownNat n, IsSpecialSize n ~ False) => DecideSSpecial n where
    specialSize = SNotSpecial

但是我们不能使用它对n进行抽象；例如，以下定义无法进行类型检查:

data Unsigned (n :: Nat) where
    U8 :: Word8 -> Unsigned 8
    U16 :: Word16 -> Unsigned 16
    U :: (IsSpecialSize n ~ False) => Integer -> Unsigned n

instance forall n. (KnownNat n) => Num (Unsigned n) where
    fromInteger = case specialSize @n of
        SSpecial8 -> U8 . fromInteger
        SSpecial16 -> U16 . fromInteger
        SNotSpecial -> U . fromInteger

与

    • Couldn't match type ‘IsSpecialSize n’ with ‘'False’
        arising from a use of ‘specialSize’
    • In the expression: specialSize @n

我可以做的一件事是将 DecideSSpecial n 添加到 Num 实例的上下文中:

instance forall n. (KnownNat n, DecideSSpecial n) => Num (Unsigned n) where

但我非常想避免这种情况；毕竟，从道德上讲，我应该能够判断任何给定的 KnownNat 是否等于 8、16 或都不等于。

Answer 1

目前还没有办法安全地做到这一点。

如果有一种方法可以在运行时从 KnownNat 获取不平等的证据，那么这是可能的。约束。

您仍然可以不安全地创建这样的方式(您可以在 GHC.TypeNats.sameNat 情况下使用 unsafeCoerce 和 Refl a Nothing ):

-- (==) and (:~:) from Data.Type.Equality
eqNat :: forall n m. (KnownNat n, KnownNat m) => Either ((n == m) :~: 'False) (n :~: m)
eqNat =
  case GHC.TypeNats.sameNat @n @m Proxy Proxy of
    Just r -> Right r
    Nothing -> Left (unsafeCoerce (Refl :: 'False :~: 'False))
-- The only piece of unsafe code in this answer.

请注意，它并不像您想象的那么强大。特别是，不平等不是对称的:((n == m) ~ 'False)并不意味着((m == n) ~ 'False) 。所以你必须小心eqNat的参数顺序。 .

由于使用通用相等测试，IsSpecialSize测试也需要用到它:

type IsSpecialSize n = (n == 8) || (n == 16)

最后，您可以定义一个实例，实际上是一个简单的函数。

specialSize :: forall n. KnownNat n => SSpecial n
specialSize =
  case eqNat @n @8 of
    Right Refl -> SSpecial8
    Left Refl ->
      case eqNat @n @16 of
        Right Refl -> SSpecial16
        Left Refl -> SNotSpecial