在模式匹配的不同情况下推导不同的类型类约束 [英] Deducing different type class constraints in different cases of pattern match

问题描述

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

I am trying to use a type family to generate constraints which depend on some type level natural number. Here is such an function:

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

然后我有一个具有此约束的函数.

Then i have a function which has this constraint.

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

当我尝试在我的类型家族的模式匹配中使用此功能时应该产生这个约束，ghc说它不能推断出约束

When I am trying to use this function in a pattern match where my type family should produce this constraint, ghc says that it can't deduce the constraint

这里是一个例子:

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
    |          ^^^^^^^

推荐答案

模式匹配不产生任何约束的主要原因是您在 natVal(Proxy @n):: Integer ，它不是GADT.按照@chi的答案，您需要在GADT上进行匹配，以将类型信息纳入范围.

The main reason your pattern match doesn't produce any constraint is that you're case matching on natVal (Proxy @n) :: Integer which isn't a GADT. As per @chi's answer, you need to match on a GADT to get type information into scope.

对于类型家族的略微修改版本:

For a slightly modified version of your type family:

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

您将完成此操作的方式是:

the way you'd accomplish this would be:

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上进行大小写匹配，以在 Just Refl 分支中引入约束 n〜0 .这允许将类型族 F n m 解析为 m〜0 .请注意，我已经删除了不必要的 KnownNat 约束；这一点很重要，因为@chi的答案表明，如果在 g 的类型签名中具有 KnownNat m 约束，则可以轻松解决您的问题.毕竟，如果 m 是已知的，那么您可以直接确定其是否为 0 ，并且 F mn 约束是多余的，而无论 m 和 n 的值.

This case-matches on a GADT to introduce a constraint n ~ 0 in the Just Refl branch. This allows the type family F n m to be resolved to m ~ 0. Note that I've removed the extraneous KnownNat constraints; this is somewhat important, since @chi's answer shows that your problem is easily solved if you have a KnownNat m constraint available in g's type signature. After all, if m is known, then you can determine directly if it's 0 or not, and the F m n constraint is redundant, regardless of the values of m and n.

不幸的是，对于条件翻转的原始类型族:

Unfortunately, for your original type family with the condition flipped:

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

事情更加困难.类型族使用一个非常简单的正向求解器"来解析，因为缺少更好的术语，因此对于您的 F 版本，类型表达式 F nm 只能是解析为特定的 n ，例如 0 或 5 .没有任何限制可以表示 n 是除 0 之外的未指定类型的事实，您可以通过某种方式使用它来解析 F nm =(m〜0).因此，您可以这样写:

things are more difficult. Type families are resolved using a pretty simple "forward solver", for lack of a better term, so for your version of F, the type expression F n m can only be resolved for a specific n, like 0 or 5. There's no constraint expressing the fact that n is an unspecified type other than 0 that you could somehow use to resolve F n m = (m ~ 0). So, you could write:

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 nm 的范围内有待解决.但是似乎没有一种方法可以使它适用于任意非零的 n .

which uses the fact that in the Just Refl -> branch, the constraint n ~ 1 is in scope which allows F n m to be resolved. But there doesn't seem to be a way to get it to work for arbitrary non-zero n.

有一些可行的方法.改用Peano Naturals即可解决问题:

There are a few approaches that would work. Switching to Peano naturals would solve the problem:

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 案例分支将约束 n〜S n1 纳入范围，这样做表示n 是除 Z 之外的未指定自然数，它使我们能够解析类型族 F nm =(m〜Z).

Here, the SS n case branch brings into scope the constraint n ~ S n1, which does express the fact that n is an unspecified natural other than Z, allowing us to resolve the type family F n m = (m ~ Z).

您还可以使用类型级别的条件来表示 F 约束:

You could also represent the F constraint using a type-level conditional:

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 提供了适当的类型级别的证据，即一个值小于或等于另一个值.它可能看起来像作弊，但如果将其与 的定义，您会发现这是一种常见的作弊行为.

Here, the function leqNat provides the appropriate type-level evidence that one value is less than or equal to another. It probably looks like cheating, but if you compare it to the definition of sameNat, you'll see it's the usual sort of cheating.

这篇关于在模式匹配的不同情况下推导不同的类型类约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！