haskell - 在模式匹配的不同情况下推导出不同的类型类约束

Question

我正在尝试使用类型族来生成依赖于某些类型级别自然的约束
数字。
这是一个这样的功能:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)

然后我有一个有这个约束的函数。

f :: forall n m. (KnownNat n, KnownNat m, m ~ 0) => ()
f = ()

当我尝试在我的类型系列的模式匹配中使用此功能时
应该产生这个约束，ghc说它不能推断出这个约束
这是一个例子:

g :: forall n m. (KnownNat n, KnownNat m, F n m) => ()
g =
  case (natVal (Proxy @n)) of
    0 -> ()
    n -> f @n @m

它产生错误

• Could not deduce: m ~ 0 arising from a use of ‘f’
      from the context: (KnownNat n, KnownNat m, F n m)
        bound by the type signature for:
                   g :: forall (n :: Nat) (m :: Nat).
                        (KnownNat n, KnownNat m, F n m) =>
                        ()
    ‘m’ is a rigid type variable bound by
        the type signature for:
          g :: forall (n :: Nat) (m :: Nat).
               (KnownNat n, KnownNat m, F n m) =>
               ()
 • In the expression: f @n @m
      In a case alternative: n -> f @n @m
      In the expression:
        case (natVal (Proxy @n)) of
          0 -> ()
          n -> f @n @m
    |
168 |     n -> f @n @m
    |          ^^^^^^^

Answer 1

您的模式匹配不产生任何约束的主要原因是您在 natVal (Proxy @n) :: Integer 上进行大小写匹配。这不是 GADT。根据@chi 的回答，您需要在 GADT 上进行匹配才能将类型信息纳入范围。
对于您的类型系列的略微修改版本:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = (m ~ 0)
  F n m = ()

您完成此操作的方式是:

f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @0) of
  Just Refl -> f @n @m
  Nothing -> ()

此案例匹配 GADT 以引入约束 n ~ 0在 Just Refl分支。这允许类型族 F n m待解决 m ~ 0 .请注意，我已经删除了无关的 KnownNat约束；这有点重要，因为@chi 的回答表明，如果您有 KnownNat m，您的问题很容易解决。 g 中可用的约束的类型签名。毕竟，如果 m是已知的，那么可以直接判断是不是 0与否， F m n约束是多余的，与 m 的值无关和 n .
不幸的是，对于条件翻转的原始类型系列:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)

事情变得更加困难。类型族是使用非常简单的“正向求解器”解决的，因为没有更好的术语，所以对于您的 F 版本, 类型表达式 F n m只能针对特定的 n 解决，如 0或 5 .没有约束来表达 n 的事实。是 0 以外的未指定类型你可以用它来解决 F n m = (m ~ 0) .所以，你可以写:

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @1) of
      Just Refl -> f @n @m
      Nothing -> ()

它使用了 Just Refl -> 中的事实分支，约束 n ~ 1在允许 F n m 的范围内待解决。但似乎没有办法让它适用于任意非零 n .
有几种方法可行。切换到 Peano naturals 可以解决问题:

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
class KnownNat n where
  natSing :: SNat n
instance KnownNat Z where natSing = SZ
instance KnownNat n => KnownNat (S n) where natSing = SS natSing

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F Z m = ()
  F (S n) m = (m ~ Z)

f :: forall n m. (m ~ Z) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case natSing @n of
  SZ -> ()
  SS n -> f @n @m

在这里， SS n case 分支将约束 n ~ S n1 纳入范围, 这确实表达了 n是除 Z 之外的未指定的自然值，允许我们解析类型族 F n m = (m ~ Z) .
您也可以代表 F使用类型级条件的约束:

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

和写:

import Data.Kind
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import GHC.TypeLits
import Unsafe.Coerce

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case leqNat (Proxy @1) (Proxy @n) of
  Just Refl -> f @n @m
  Nothing -> ()

leqNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe ((a <=? b) :~: True)
leqNat x y | natVal x <= natVal y = Just (unsafeCoerce Refl)
           | otherwise            = Nothing

这里，函数 leqNat提供适当的类型级别证据，证明一个值小于或等于另一个值。它可能看起来像作弊，但如果你将它与 definition of sameNat 进行比较，你会发现这是一种常见的作弊行为。