Runde und ABS-Funktion in Idris

Question

I

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

sind Funktionen dort

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

oder etwas Analoges in Idris, eine Funktion zu schreiben, bin versucht?

Edit:

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

beide akzeptable Alternativen für meinen Anwendungsfall zu round wäre.

Answer 1

Eine Möglichkeit, herauszufinden, was Sie fragen, ist die Verwendung der Idris REPL. Insbesondere der Befehl :search (oder seine Abkürzung :s). Um herauszufinden, was wir brauchen, um sqrt vom Typ anwenden Double -> Double zu einem Nat könnten wir so etwas wie dies versuchen:

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

Mit der cast Funktion, die wir die folgende Version geschrieben haben könnte:

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

Leider wird nicht mit dem Fehler kompiliert:

, weil es keine Cast Double Nat Instanz in der Standardbibliothek gibt (also ist cast {to=Nat} nicht legitim).

Als Abhilfe, die ich vorschlagen auszuführen Doppel Besetzung (kein Wortspiel beabsichtigt) Double-Integer zu Nat:

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

die knapp rounding towards zero

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

cast {to=Integer} tut mehr geschrieben werden kann, auch bekannt als .

Übrigens ist die Verwendung von sqrt möglicherweise nicht der beste Weg, dies zu berechnen. Vorsicht vor den Gleitkomma-Rundungsfehlern, sie können Ihnen unerwarteterweise ein Einzelergebnis liefern. Da Ihre Funktion der integer square root ähnelt, ist es möglicherweise besser, etwas ähnliches zu implementieren.

---

Nun zum abs, floor, ceiling und round Funktionen.

Die Neg Schnittstelle definiert abs mit folgenden Art:

abs : Neg ty => ty -> ty 

So müssen Sie einige einfache Art Casting tun abs : Int -> Nat zu implementieren.

Der Standard Prelude definiert auch

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

Also, noch einmal mit einer wenig Arbeit man sie in Double -> Int Neufassung kann.

Es gibt keinen Standard round Funktion, und wenn Sie es immer noch brauchen, dann könnten Sie versuchen, es zu implementieren, indem Sie als Beispiel die Haskell RealFrac Typklasse verwenden.