работа с функциями, которые принимают ненулевые натуральные числа - PullRequest
Новая
       12

работа с функциями, которые принимают ненулевые натуральные числа

0 голосов
/ 26 мая 2018

Я пытаюсь определить функцию (congruentialMethod) в Идрисе, которая среди прочего применяет арифметику модуля к некоторым аргументам, предоставленным моей функции.Арифметика модуля требует, чтобы второй аргумент был ненулевым, поэтому я попытался использовать modNatNZ и добавить доказательство к моей сигнатуре типа функции.Тем не менее, я чувствую, что моя попытка оказывается очень неуклюжей.

Прежде всего, когда я определяю значение, которое в итоге становится вторым аргументом функции модуля (let m : Nat = 2147483647), -Я должен выполнить несколько неуклюжихсопоставление регистра, чтобы убедить Идриса, что значение больше нуля.Если я этого не сделаю, тогда проверка типов будет длиться вечно.

Во-вторых, я не совсем понимаю, почему я должен предоставить доказательство при вызове моей функции (congruentialMethod).Я указал доказательство как auto в сигнатуре функции, полагая, что Идрис сможет вывести его. 

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

Можно ли как-то избежать передачи доказательства моей функции congruentialMethod?и есть ли менее неуклюжий способ убедить Идриса, что let m : Nat = 2147483647 больше нуля (вместо использования сопоставления регистра) ?

РЕДАКТИРОВАТЬ: еще одна проблема сэтот код выглядит так, что выполнение вычислений с Nat выполняется крайне медленно.Использование Int, mod и изменение функций на partial позволяет быстро генерировать числа.Очевидно, что нас заставляют определять функции как partial отстой .. Но, возможно, это материал для другого вопроса ...

1 Ответ

0 голосов
/ 27 мая 2018

Идрису очень трудно вывести Not доказательства, потому что они являются функциями, а Идрис просто не пытается выводить функции, потому что функции довольно сложные.Стандартная библиотека уже подумала о вашей ситуации.У нас есть Prelude.Nat.IsSucc: 

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

Это работает с auto, но существующие функции Nat не совместимы с ним, поэтому мы используем немного клея.

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

Сайт использования теперь будет выводить prf.Однако, с таким большим числом, компилятор все еще задыхается, как вы видели в своем редактировании.В конечном итоге это будет правильно, но это займет некоторое время.У меня нет решения для этого.

...