I have been playing around with making my own random generator in Idris for learning purpose. In my solution I am aiming for totality for all functions and thus I am using numbers of type Nat and the built-in function modNatNZ which requires proof that the second arg isn't zero.
While making a program to test my function on some large natural numbers as input, I encountered problems with both type checking and execution of the program being incredible slow.
module Main
%default total
getUnixEpoch : IO Int
getUnixEpoch = foreign FFI_C "#(unsigned long)time(NULL)" (IO Int)
isSuccNotZero : IsSucc n -> Not (n = Z)
isSuccNotZero {n = S _} ItIsSucc Refl impossible
congruentialMethod : (seed : Nat) -> (a : Nat) -> (b : Nat) ->
(m : Nat) -> {auto prf : IsSucc m} -> Stream Double
congruentialMethod seed a b m {prf} =
(cast seed / cast m) :: congruentialMethod (safeMod_m (a * seed + b)) a b m
where
safeMod_m : Nat -> Nat
safeMod_m x = modNatNZ x m (isSuccNotZero prf)
randomNumberGenerator : (seed : Nat) -> Stream Double
randomNumberGenerator seed =
let a : Nat = 16807
b : Nat = 0
m : Nat = 2147483647
in
case m of
Z => ?this_will_never_happen_but_it_makes_type_checking_faster
(S m') => congruentialMethod seed a b (S m')
main : IO ()
main = do seed <- getUnixEpoch
putStrLn $ show $ take 5 $ randomNumberGenerator (cast seed)
The type checker seems to take an eternity to verify that a hard-coded value of 2147483647 really is greater than zero. My poor fix to this, is to convince Idris with a case-expression.
...
m = 2147483647
in
case m of
Z => ?this_will_never_happen_but_it_makes_type_checking_faster
(S m') => congruentialMethod seed a b (S m')
Obviously my work-around with the case-expression isn't very satisfying. So is there a better way of convincing the type checker that m is greater than zero in order to get faster type checking?
If this is something that requires a workaround, then I am wondering if this is something a future implementation of the type checker in theory will be able to handle in reasonable time without workarounds, -or if it is something I should always expect to work around to get fast type checking?
I've attempted to both execute the program in the repl and execute a compiled version of the program, but had to terminate both manually because they seem to take forever to run.
I've experimented a little with making a program that used integers (Int type) in which I was able to get fast run-time performance, but I don't see any way to make all the functions total when making the same program with integers.
Is there a way to define my program with all functions being total and still get fast performance?
Again, if there currently isn't a good way to get faster run-time performance for this kind of program, then I am wondering if this is something that eventually/theoretically could be improved in future versions of Idris, -or if this is something I'll always have to work around or fall back to partial functions to get fast run-time performance?
I am using Idris version 1.2.0
Consider
N : Nat
N = 10000
nIsS : IsSucc N
nIsS = ItIsSucc
with
ItIsSucc : IsSucc (S n)
Right now, as far as I understand it, everything has to be evaluated when type checking, i.e. 10000 must be constructed, before finding n. Neither of them are optimized to integers (in the compile time stage), but a nesting of S (S (S (S (S …)))). You can %freeze N to stop it from being evaluated (which would work in your case):
N : Nat
N = 9999
%freeze N
nIsS : IsSucc (S N)
nIsS = ItIsSucc
Theoretically that shouldn't be necessary, as you can easily see by the first S (…) that it fulfills IsSucc (S n) (just set n = …). This lazy approach to unifying is called weak head normal form. WHNF is implemented to some extend, but apparently isn't used always when type checking. So this could be improved in the future, and if I'm not mistaken, Blodwen (WIP!) supports this. At least there is a bigsuc-example. :-)
Idris compiles Nat to GMP bignums and uses corresponding C functions for them (like addition, substraction, multiplication, …). Modulo isn't among them, but uses the actual Idris definition. Of course that's not as fast as Integer, which uses a native C function.
There isn't really anything clean you can do about it. If you really want totality, best thing would probably asserting it by hand if you're really sure that this function is total:
modIntNZ : (i, m : Integer) -> {auto prf : m == 0 = False} -> Integer
modIntNZ i m = assert_total (i `mod` m)