Idris 1.2.0 中的大自然数类型检查速度慢，运行时间性能差

Question

出于学习目的，我一直在尝试在 Idris 中制作自己的随机生成器。在我的解决方案中，我的目标是所有函数的完整性，因此我使用 Nat 类型的数字和内置函数 modNatNZ ，这需要证明第二个 arg 不为零。

在编写程序以将一些大的自然数作为输入来测试我的函数时，我遇到了类型检查和程序执行速度极慢的问题。

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 是否确实大于零。我对此的糟糕解决方法是用案例表达式来说服 Idris。

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

显然，我对 case-expression 的解决方法不是很令人满意。那么有没有更好的方法让类型检查器相信 m 大于零以获得更快的类型检查？

如果这需要解决方法，那么我想知道这是否是理论上类型检查器的未来实现是否能够在没有解决方法的情况下在合理的时间内处理，或者如果这是我应该始终期望解决的问题以获得快速类型检查？

2。具有大自然数的程序执行需要很长时间。

我试图在 repl 中执行程序并执行程序的编译版本，但不得不手动终止这两个程序，因为它们似乎永远运行。

我尝试了一些使用整数（Int 类型）的程序，在其中我能够获得快速的运行时间性能，但我没有看到任何使用整数制作相同程序时制作所有功能的方法total。

有没有办法定义我的程序，所有函数都是 total 并且仍然获得快速性能？

同样，如果目前没有一种好的方法可以使此类程序获得更快的运行时间性能，那么我想知道这是否是 eventually/theoretically 可以在 Idris 的未来版本中得到改进，-或者如果这是我总是必须解决的问题或退回到部分函数以获得快速运行时间性能？

我使用的是 Idris 版本 1.2.0

Answer 1

类型检查性能

考虑

N : Nat
N = 10000

nIsS : IsSucc N
nIsS = ItIsSucc

和

ItIsSucc : IsSucc (S n)

目前，据我了解，在类型检查时必须评估所有内容，即在查找 n 之前必须构造 10000。它们都没有优化为整数（在编译阶段），而是 S (S (S (S (S …)))) 的嵌套。您可以 %freeze N 阻止它被评估（这对您的情况有效）：

N : Nat
N = 9999
%freeze N

nIsS : IsSucc (S N)
nIsS = ItIsSucc

理论上这不是必需的，因为您可以很容易地从第一个 S (…) 看出它满足 IsSucc (S n)（只需设置 n = …）。这种懒惰的统一方法称为 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 将 Nat 编译为 GMP bignums 并为它们使用相应的 C 函数（如加法、减法、乘法等）。 Modulo 不在其中，但使用 actual Idris definition。当然，这不如使用原生 C 函数的 Integer 快。

您真的无能为力。如果你真的想要完整性，如果你真的确定这个函数是完整的，最好的办法可能是手动声明它：

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

Idris 1.2.0 中的大自然数类型检查速度慢，运行时间性能差

Slow type-checking and poor run-time performance with large natural numbers in Idris 1.2.0

idris

1。用大的自然数进行类型检查需要很长时间。

2。具有大自然数的程序执行需要很长时间。

类型检查性能

运行时间表现

Idris 1.2.0 中的大自然数类型检查速度慢，运行 时间性能差

Slow type-checking and poor run-time performance with large natural numbers in Idris 1.2.0

idris

1。用大的自然数进行类型检查需要很长时间。

2。具有大自然数的程序执行需要很长时间。

类型检查性能

运行时间表现

Idris 1.2.0 中的大自然数类型检查速度慢，运行时间性能差