haskell - 将 `<=?` 替换为 `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 (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))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
稍微简化一下约束,也可以写得更简洁:
CmpNat 1 n ~ 'LT && CmpNat n 17 ~ 'LT
但是 GHC 仍然不喜欢这样,因为和以前一样的原因给出了相同的类型错误。
在这种情况下,最干净的使用方法是CmpNat
什么<=?
?
解决方案
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
推荐阅读
- javascript - 将数据从函数返回到 ajax javascript
- python - 客户端未从服务器 python 接收数据
- linux - cpu时间在虚拟机中跳跃很多
- highcharts - Highstock 设置 XAxis 极端没有数据
- spring - 初始化 List 的最佳实践?自动装配列表或构造函数初始化?
- amazon-web-services - 尽管输入了准确的话语,AWS Lex 仍匹配错误的意图
- javascript - ScrollIntoView() 不起作用 - vanilla JS,为什么?
- ios - 如何使用导航栏过渡到视图控制器?
- android - 使用 --env.aot 标志时未构建 Nativescript 应用程序
- sql - SQL Server:仅结合没有参考的日期