Круглые и функции абс в Идриса

Question

Я пытаюсь написать функцию

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

Существуют функции

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

или что-то аналогичное в Идрис?

Edit:

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

бы оба приемлемые альтернативы round для моего сценария использования.

Answer 1

Один из способов узнать, что вы просите, это использовать Idris REPL. В частности, команда :search (или ее аббревиатура :s). Для того, чтобы узнать, что нам нужно для того, чтобы применить sqrt типа Double -> Double к 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.

Стандарт Prelude также определяет

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

Итак, снова немного работы, можно переделать их в Double -> Int.

Нет стандартной функции round, и если она вам по-прежнему нужна, вы можете попробовать ее реализовать, используя в качестве примера Haskell RealFrac typeclass.