idris - 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 大于零，以便更快地进行类型检查？

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

2. 大自然数的程序执行需要永远。

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

我已经尝试了一些使用整数( Int 类型)的程序，在该程序中我能够获得快速的运行时性能，但我没有看到任何方法可以使所有函数 total使用整数制作相同的程序时。

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

同样，如果目前没有一种好方法可以为此类程序获得更快的运行时性能，那么我想知道这是否最终/理论上可以在 Idris 的 future 版本中得到改进，或者如果这是我总是不得不解决或退回到部分功能以获得快速运行时性能的东西？

我使用的是 Idris 版本 1.2.0

Answer 1

类型检查性能

考虑

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 = … )。这种懒惰的统一方法称为 weak head normal form . WHNF 在某种程度上得到了实现，但显然在类型检查时并不总是使用。所以这可以在 future 得到改进，如果我没记错的话，Blodwen(WIP!)支持这一点。至少还有一个 bigsuc-example . :-)

运行时性能

idris 编译 Nat GMP bignums 并为它们使用相应的 C 函数(如加法、减法、乘法等)。 Modulo 不在其中，但使用 actual Idris definition .当然这没有 Integer快，它使用 native C 函数。

你真的没有什么可以做的。如果你真的想要整体性，最好的办法可能是手动断言它，如果你真的确定这个函数是完整的:

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