用 `CmpNat` 替换 `<=?`

Question

我有以下类型系列：

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits
import Data.Type.Bool

type family Valid (n :: Nat) :: Constraint where
  Valid (n :: Nat) = ( KnownNat n
                     , If (2 <=? n && n <=? 16)
                          (() :: Constraint)
                          (TypeError ('Text "No Good"))
                     )

这按预期工作。但是，GHC有一个音符是<=?可能有利于消失CmpNat。到目前为止，我尝试替换<=?with 的尝试CmpNat失败了。这个版本，例如：

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits
import Data.Type.Bool

type family Valid (n :: Nat) :: Constraint where
  Valid (n :: Nat) = ( KnownNat n
                     , If ((CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT) && (CmpNat n 16 ~ 'EQ || CmpNat n 16 ~ 'LT))
                          (() :: Constraint)
                          (TypeError ('Text "No Good"))
                     )

不仅更冗长，GHC 理所当然地不喜欢它，因为类型级布尔值的组成部分和/或本身不再是布尔值：

    • Expected kind ‘Bool’,
        but ‘CmpNat 2 n ~ 'EQ’ has kind ‘Constraint’
    • In the first argument of ‘(||)’, namely ‘CmpNat 2 n ~ 'EQ’
      In the first argument of ‘(&&)’, namely
        ‘(CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT)’
      In the first argument of ‘If’, namely
        ‘((CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT)
          && (CmpNat n 16 ~ 'EQ || CmpNat n 16 ~ 'LT))’
   |
13 |                      , If ((CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT) && (CmpNat n 16 ~ 'EQ || CmpNat n 16 ~ 'LT))
   |                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

稍微简化一下约束，还可以写得更简洁：

    • Expected kind ‘Bool’,
        but ‘CmpNat 2 n ~ 'EQ’ has kind ‘Constraint’
    • In the first argument of ‘(||)’, namely ‘CmpNat 2 n ~ 'EQ’
      In the first argument of ‘(&&)’, namely
        ‘(CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT)’
      In the first argument of ‘If’, namely
        ‘((CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT)
          && (CmpNat n 16 ~ 'EQ || CmpNat n 16 ~ 'LT))’
   |
13 |                      , If ((CmpNat 2 n ~ 'EQ || CmpNat 2 n ~ 'LT) && (CmpNat n 16 ~ 'EQ || CmpNat n 16 ~ 'LT))
   |                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

但是 GHC 仍然不喜欢那样，出于与以前完全相同的原因给出相同的类型错误。

什么是用干净的方式CmpNat，而不是<=?在这方面？

Answer 1

CmpNat 2 n ~ 'EQ是一个约束，而不是一个布尔值。

Prelude> :k 'EQ ~ 'EQ
'EQ ~ 'EQ :: Constraint

基本上，约束只能被证明，不能被证伪，因此不能在If语句中使用。

（有一种“永远不会为假”的平等感似乎很愚蠢，但实际上这种事情是有充分理由的。与Coq 中的布尔值与命题进行比较。）

你想要的是.CmpNat 2 n == 'EQ`

Prelude Data.Type.Equality> :k 'EQ == 'EQ
'EQ == 'EQ :: Bool