Idris中如何通过floor丢弃小数点实现Double到Nat类型的转换

Idris默认不提供Double到Nat的直接cast实现，是为了避免隐式的信息丢失和非预期行为，你可以通过显式的取值校验+向下取整的逻辑实现需求，以下是两种常用实现：

1. 安全转换实现（推荐） #

通过Maybe类型封装转换结果，处理输入为负数的异常场景：

||| 将Double向下取整后转换为Nat，负数返回Nothing
doubleToNat : Double -> Maybe Nat
doubleToNat num = if num < 0 
                    then Nothing
                    else Just $ cast $ floor num

逻辑说明：

• 首先校验输入值非负，避免负数转Nat出现非预期结果
• 调用floor方法丢弃小数部分，得到取整后的Double值
• 先将取整后的Double转为Integer，再通过cast转为Nat，此时因为已经做了非负校验，转换是安全的

2. 不安全转换实现 #

如果你的场景可以保证输入永远非负，或者希望异常输入直接返回0，可以用无封装的实现：

||| 将Double向下取整后转换为Nat，负数/非法值默认返回0
unsafeDoubleToNat : Double -> Nat
unsafeDoubleToNat num = if num < 0 
                          then 0
                          else cast $ floor num

搭配divNat使用示例 #

你提到的divNat可以直接搭配转换后的Nat值使用，示例如下：

-- 将输入Double除以2后取整为Nat
halfToNat : Double -> Nat
halfToNat num = unsafeDoubleToNat num `divNat` 2

注意事项 #

• 若输入为NaN、无穷大等非法Double值，转换结果默认返回0，若你的场景可能出现这类值，建议在安全转换中增加额外的合法性校验
• 当Double的数值超过Integer的表达范围时，会出现精度丢失，需根据业务场景判断是否需要额外处理

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