Медленная проверка типов и низкая производительность во время выполнения с большими натуральными числами в Idris 1.2.0 - PullRequest
Новая
       13

Медленная проверка типов и низкая производительность во время выполнения с большими натуральными числами в Idris 1.2.0

0 голосов
/ 24 июня 2018

Я занимался созданием собственного генератора случайных чисел в Идрисе для целей обучения. В моем решении я стремлюсь к полноте для всех функций, и поэтому я использую числа типа Nat и встроенную функцию modNatNZ, которая требует доказательства того, что второй аргумент не равен нулю.

При создании программы для проверки моей функции на некоторых больших натуральных числах в качестве входных данных я столкнулся с проблемами, связанными как с проверкой типов, так и с выполнением программы, невероятно медленной. 

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)

1. Проверка типа с большими натуральными числами занимает целую вечность.

Проверка типа, кажется, занимает вечность, чтобы убедиться, что жестко закодированное значение 2147483647 действительно больше нуля. Мое плохое решение - убедить Идриса с помощью выражения-случая. 

        ...
        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')

Очевидно, что мой обходной путь с выражением падежа не очень удовлетворяет. Так есть ли лучший способ убедить средство проверки типов в том, что m больше нуля, чтобы ускорить проверку типов?

Если это что-то, требующее обходного пути, то мне интересно, сможет ли это будущая реализация средства проверки типов в теории справиться за разумное время без обходных путей, или, если это то, что я всегда нужно ожидать, чтобы быстро проверить тип?

2. Выполнение программы с большими натуральными числами занимает вечность.

Я пытался как запустить программу в repl, так и выполнить скомпилированную версию программы, но мне пришлось прервать обе операции вручную, потому что кажется, что для их запуска требуется вечность.

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

Есть ли способ определить мою программу со всеми функциями, равными total, и при этом получить быструю производительность?

Опять же, если в настоящее время не существует хорошего способа получить более высокую производительность во время выполнения для такого рода программ, то мне интересно, можно ли это в конечном итоге / теоретически улучшить в будущих версиях Idris? , или, если это что-то, мне всегда придется обходиться или прибегать к частичным функциям, чтобы получить быструю производительность во время выполнения?

Я использую Idris версии 1.2.0

1 Ответ

0 голосов
/ 29 июня 2018

Тип проверки производительности

Рассмотрим 

N : Nat
N = 10000

nIsS : IsSucc N
nIsS = ItIsSucc

с 

ItIsSucc : IsSucc (S n)

Прямо сейчас, насколько я понимаю, все должно быть оценено при проверке типа, то есть 10000 должно быть построено, прежде чем найти n. Ни один из них не оптимизирован для целых чисел (на этапе компиляции), но вложенность S (S (S (S (S …)))). Вы можете %freeze N, чтобы остановить его оценку (что будет работать в вашем случае): 

N : Nat
N = 9999
%freeze N

nIsS : IsSucc (S N)
nIsS = ItIsSucc

Теоретически, в этом нет необходимости, поскольку по первому S (…) вы легко можете увидеть, что он удовлетворяет IsSucc (S n) (просто установите n = …). Этот ленивый подход к объединению называется слабая голова нормальной формы . WHNF реализован в некоторой степени, но, очевидно, не всегда используется при проверке типов. Так что это может быть улучшено в будущем, и, если я не ошибаюсь, Blodwen (WIP!) Поддерживает это. По крайней мере, есть bigsuc-пример . : -)

Выполнение во время исполнения

Idris компилирует Nat в bignums GMP и использует для них соответствующие функции C (такие как сложение, вычитание, умножение и т. Д.). Модуло среди них нет, но используется фактическое определение Идриса . Конечно, это не так быстро, как Integer, который использует встроенную функцию C.

На самом деле с этим ничего не поделаешь. Если вы действительно хотите тотальности, лучше всего будет утверждать это вручную, если вы действительно уверены, что эта функция полная: 

modIntNZ : (i, m : Integer) -> {auto prf : m == 0 = False} -> Integer
modIntNZ i m = assert_total (i `mod` m)
...