将"<=？"替换为"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取代。到目前为止，我试图用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))
|                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

将约束简化一点，也可以写得更简洁:

CmpNat 1 n ~ 'LT && CmpNat n 17 ~ '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