时间戳

首页 > 解决方案 > 见证以前的类型家庭条款不匹配

haskell - 见证以前的类型家庭条款不匹配

问题描述

我有以下封闭类型系列：

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 或都不等于。

标签： haskelltype-familiestype-level-computationsingleton-type

解决方案

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

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

您仍然可以不安全地创建这种方式（您可以使用GHC.TypeNats.sameNat, 和unsafeCoerceaRefl在这种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

推荐阅读