working with functions that takes non-zero natural numbers

Question

I am trying to define a function (congruentialMethod) in Idris that amongst others applies modulus arithmetic on some of the arguments provided to my function. Modulus arithmetic requires that the second argument to be non-zero, so I have attempted to utilize modNatNZ and add a proof to my function type signature. However, I feel my attempt comes about very clunky.

First of all, when I define the value that ends up being the second arg to the modulus function (let m : Nat = 2147483647), -I have to perform some clunky case matching to convince Idris that the value is bigger than zero. If I don't do this then type checking takes forever.

Second, I don't really understand why I have to provide a proof when I call my function (congruentialMethod). I specified the proof as auto in the function signature thinking Idris would be able to infer it.

module Random

%default total

getUnixEpoch : IO Nat
getUnixEpoch = do time <- foreign FFI_C "#(unsigned long)time(NULL)" (IO Int)
                  pure $ fromInteger $ cast time

congruentialMethod : (seed : Nat) -> (a : Nat) -> (b : Nat) -> (m : Nat) -> {auto prf : (m = Z) -> Void} -> Stream Double
congruentialMethod seed a b m {prf} =
  (cast seed) / (cast m) :: loop seed
  where
    loop : (prev : Nat) -> Stream Double
    loop prev = let n = modNatNZ (a * prev + b) m prf
                in (cast n) / (cast m) :: loop n

main : IO ()
main = do time <- getUnixEpoch
          putStrLn $ "seed: " ++ (cast time)
          let a : Nat = 16807
          let b : Nat = 0
          let m : Nat = 2147483647
          case m of
               Z => ?shouldnt_happen
               S m' => do let random_number_stream = congruentialMethod time a b (S m') {prf = SIsNotZ}
                          ?continue

Can I somehow avoid passing a proof to my congruentialMethod function? and is there a less clunky way to convince Idris that let m : Nat = 2147483647 is bigger than zero (rather than using a case match)?

EDIT: Another problem with this code seems to be that performing calculations with Nat is extremely slow. Using Int, mod and changing the functions to being partial makes it fast to generate numbers. Obviously being forced to defining functions as partial sucks.. But perhaps this is material for another question....

HTNW HTNW · Accepted Answer · 2018-05-27T18:42:31

Idris has a very hard time inferring Not proofs, because they are functions, and Idris just doesn't try to infer functions, because functions are quite complicated. The standard library has already thought of your situtation. We have Prelude.Nat.IsSucc:

data IsSucc : Nat -> Type where
  ItIsSucc : IsSucc (S n)

This works with auto, but the existing Nat functions aren't compatible with it, so we use a bit of glue.

isSuccNotZero : IsSucc n -> Not (n = Z)
isSuccNotZero {n = S _} ItIsSucc Refl impossible

And that's it:

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 (modNatNZ (a * seed + b) m $ isSuccNotZero prf) a b m)

The usage site will now infer prf. However, with a number that big, the compiler still chokes, as you've seen in your edit. It will eventually get it right, but that'll take a while. I don't have a solution for that.

working with functions that takes non-zero natural numbers

1 Answers