Idris中如何获取Int类型的maxBound值

Idris 中的 Int 类型实现了 Bounded 类型类，该类提供的 maxBound 函数可直接获取对应平台下 Int 的最大值，天然适配32位和64位字长环境——Idris会根据编译运行的系统自动将Int映射为对应位宽的有符号整数，maxBound会返回该位宽下的最大取值。

基础用法 #

直接调用maxBound即可，若上下文无法自动推断类型，可显式指定：

-- 定义获取Int最大值的函数
intMax : Int
intMax = maxBound

-- 在IO中打印最大值
main : IO ()
main = printLn maxBound {a=Int}

原理说明 #

• 32位系统下，Int对应32位有符号整数，maxBound返回2^31 - 1
• 64位系统下，Int对应64位有符号整数，maxBound返回2^63 - 1
• 无需手动判断环境，代码编译运行时会自动适配当前平台的字长

可选：验证Int的位宽 #

如果需要确认当前环境下Int的位宽，可使用Bits类型类的bitSizeMaybe函数：

getIntBitWidth : Maybe Nat
getIntBitWidth = bitSizeMaybe (the Int 0)

调用后会返回Just 32或Just 64，可辅助验证当前平台的字长，但不影响maxBound的自动适配逻辑。

内容的提问来源于stack exchange，提问作者Janus Troelsen