伊德里斯的圆形和腹肌功能(Round and abs function in Idris)

伊德里斯的圆形和腹肌功能(Round and abs function in Idris)

我正在尝试写一个函数

roundedSqrt : Nat -> Nat roundedSqrt = abs . round . sqrt . fromIntegral

有功能吗？

round: Double -> Int abs : Int -> Nat

或者类似于伊德里斯的东西？

编辑：

floor : Double -> Int ceiling : Double -> Int

对于我的用例而言，这两者都是可接受的替代方案。

I'm trying to write a function

roundedSqrt : Nat -> Nat roundedSqrt = abs . round . sqrt . fromIntegral

Are there functions

round: Double -> Int abs : Int -> Nat

or something analogous in Idris?

Edit:

floor : Double -> Int ceiling : Double -> Int

would both be acceptable alternatives to round for my use-case.

最满意答案

找出问题的一种方法是使用Idris REPL。 特别是:search命令（或其缩写:s ）。 要发现我们需要什么才能将类型为Double -> Double sqrt应用于Nat我们可能会尝试这样的事情：

Idris> :s Nat -> Double < Prelude.Cast.cast : Cast from to => from -> to Perform a cast operation.

使用我们可以编写以下版本的cast函数：

roundedSqrtDoesntCompile : Nat -> Nat roundedSqrtDoesntCompile = cast {to=Nat} . sqrt . cast {to=Double}

不幸的是，它不会编译错误：

无法从Double为Nat

因为标准库中没有Cast Double Nat实例（所以cast {to=Nat}不合法）。

作为一种解决方法，我建议执行从Double到Integer到Nat双重（无双关语）演员：

roundedSqrt : Nat -> Nat roundedSqrt = cast {to=Nat} . cast {to=Integer} . sqrt . cast {to=Double}

这可以写得更简洁

roundedSqrt : Nat -> Nat roundedSqrt = cast . cast {to=Integer} . sqrt . cast

cast {to=Integer} 向零舍入 ，即截断 。

顺便说一下，使用sqrt可能不是计算它的最佳方法。 注意浮点舍入错误，他们可以出乎意料地得到一个一个接一个的结果。 由于您的函数类似于整数平方根 ，因此最好实现接近它的东西。

---

现在到了abs ， floor ， ceiling和round功能。

Neg接口使用以下类型定义abs ：

abs : Neg ty => ty -> ty

所以你需要做一些简单的类型转换来实现abs : Int -> Nat 。

标准Prelude也定义了

floor : Double -> Double ceiling : Double -> Double

所以，再做一点工作，可以将它们重铸为Double -> Int 。

没有标准的round函数，如果你仍然需要它，那么你可以尝试使用Haskell RealFrac类型类作为一个例子来实现它。

One way to find out what you are asking is using the Idris REPL. Specifically the :search command (or its abbreviation :s). To discover what we need in order to apply sqrt of type Double -> Double to a Nat we might try something like this:

Idris> :s Nat -> Double < Prelude.Cast.cast : Cast from to => from -> to Perform a cast operation.

Using the cast function that we could have written the following version:

roundedSqrtDoesntCompile : Nat -> Nat roundedSqrtDoesntCompile = cast {to=Nat} . sqrt . cast {to=Double}

Unfortunately, it won't compile with the error:

Can't cast from Double to Nat

because there is no Cast Double Nat instance in the standard library (so cast {to=Nat} is not legitimate).

As a workaround I propose to perform double (no pun intended) cast from Double to Integer to Nat:

roundedSqrt : Nat -> Nat roundedSqrt = cast {to=Nat} . cast {to=Integer} . sqrt . cast {to=Double}

which can be written more concisely

roundedSqrt : Nat -> Nat roundedSqrt = cast . cast {to=Integer} . sqrt . cast

cast {to=Integer} does rounding towards zero, a.k.a. truncation.

By the way, using sqrt might not be the best way of calculating this. Beware of the floating-point rounding errors, they can unexpectedly get you an off-by-one result. Since your function resembles the integer square root, it may be better to implement something close to that.

---

Now to the abs, floor, ceiling, and round functions.

The Neg interface defines abs with the following type:

abs : Neg ty => ty -> ty

So you will need to do some simple type casting to implement abs : Int -> Nat.

The standard Prelude also defines

floor : Double -> Double ceiling : Double -> Double

So, again with a little work one can recast them into Double -> Int.

There is no standard round function, and if you still need it, then you could try implementing it using as an example the Haskell RealFrac typeclass.