基于运行时值 (maxBound :: Int) 创建类型约束

Question

我对类型级计算和类型族等非常陌生，我正在尝试制作一个Constraint，以防止类型级Nat超过maxBound :: Int.

为了使代码面向未来，我希望有一个解决方案可以正常工作，无论是正常编译还是交叉编译到具有不同字大小的机器上。它应该根据运行时maxBound :: Int的目标计算机值来限制Nat(如果有办法在编译时获取该确切值并从那里开始，那很好(。

---

我在学习如何对编译器错误消息进行约束时得到了一些帮助，这是我解决这个问题的不太好的第一次尝试：

type family BigUpperLimit (n :: Nat) (c :: Constraint) :: Constraint where
BigUpperLimit n c = If (CmpNat n (maxBound :: Int) == 'GT)
(TypeError (    Text "UInt "
:<>: ShowType n
:<>: Text " exceeds UInt "
:<>: ShowType (maxBound :: Int)
:<>: Text ", the maximum size allowed with this machine's word size."
)
)
c

它抱怨maxBound不是已知的类型变量。如果我在maxBound前面放一个'，它会抱怨"类型中的非法提升项变量：maxBound"。

---

如何实现我的目标？我对修复上述方法的方法和完全不同的方法持开放态度。

Answer 1

我认为你最好的选择是在这里使用 CPP 本身。

{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
import Data.Type.Bool
import Data.Kind
#include "MachDeps.h"
type family BigUpperLimit (n :: Nat) :: Constraint where
BigUpperLimit n = ( KnownNat n
, If (0 <=? n && n <=? WORD_SIZE_IN_BITS)
(() :: Constraint)
(TypeError (    Text "UInt "
:<>: ShowType n
:<>: Text " exceeds UInt "
:<>: ShowType WORD_SIZE_IN_BITS
:<>: Text ", the maximum size allowed with this machine's word size.")))

现在，您可以：

*Main> 2 :: BigUpperLimit 12 => Int
2
*Main> 2 :: BigUpperLimit 120 => Int
<interactive>:34:1: error:
• UInt 120 exceeds UInt 64, the maximum size allowed with this machine's word size.
• In the expression: 2 :: BigUpperLimit 120 => Int
In an equation for ‘it’: it = 2 :: BigUpperLimit 120 => Int

请注意，后者是类型错误：

*Main> :t 2 :: BigUpperLimit 120 => Int
<interactive>:1:1: error:
UInt 120 exceeds UInt 64, the maximum size allowed with this machine's word size.