回合和ABS功能

Question

我試圖寫一個函數

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

是否有功能

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

或類似的東西在伊德里斯？

編輯：

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

都希望能爲我的用例來round可接受的替代品。

Answer 1

找出你要問的是使用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} 

不幸的是，它不會編譯錯誤：

Can't cast from Double to 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}確實rounding towards zero，又名truncation。

順便說一句，使用sqrt可能不是計算這個最好的方法。注意浮點舍入錯誤，他們可以意外地得到你一個結果。由於你的函數類似於integer square root，所以最好實現一些與之相近的東西。

---

我們的abs，floor，ceiling和round功能。

的Neg接口定義abs有以下類型：

abs : Neg ty => ty -> ty 

所以，你需要做一些簡單的類型轉換來實現abs : Int -> Nat。

的標準前奏還定義

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

所以，再一點點的工作可以重鑄他們進入Double -> Int。

沒有標準的round函數，如果你仍然需要它，那麼你可以嘗試使用Haskell RealFrac類型類來實現它。