Блог

Главная - Вопросы по программированию - Проверка типа процедуры принятия решений Idris чрезвычайно медленная, неотъемлемая проблема производительности?

Проверка типа процедуры принятия решений Idris чрезвычайно медленная, неотъемлемая проблема производительности?

#idris #dependent-type

#idris #зависимый тип

Вопрос:

 decLte : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decLte Z _ = Yes LTEZero
decLte (S _) Z = No (x => case x of LTEZero impossible ; LTESucc _ impossible)
decLte (S n) (S m) with (decLte n m)
  | Yes ltePrf = Yes (LTESucc ltePrf)
  | No lteContra = No ((LTESucc p) => lteContra p)

data NatRange : Type where
   In : (l: Nat) -> (u: Nat) -> {auto yep : decLte l u = Yes _} -> NatRange

natRangeEx1 : NatRange
natRangeEx1 = In 500 2100

Проверка типа в этом коде занимает около 5 минут и использует > 2 ГБ памяти. Я ошеломлен чрезвычайно низкой производительностью. Может ли кто-нибудь назвать мне вескую причину, например, это проблема моего кода или проблема, присущая Idris?

Комментарии:

1. Вы уверены, что это сам Idris? Мой компьютер часто зависал в конце концов (с чрезвычайно высоким потреблением памяти) после того, как я запустил компиляцию своего кода. Однако я не совсем уверен, виноват ли сам Idris или, возможно, используемый мной плагин Atom. Однако в моем случае это происходит довольно случайно: иногда один и тот же код компилируется быстро, в другой раз это полностью убивает машину…

2. Я могу подтвердить, что это происходит очень медленно. Также переход на встроенную isLTE функцию не имеет значения. Причиной является 500 параметр. Если изменить его на что-то близкое к нулю, это будет значительно быстрее. К сожалению, мне не удалось скомпилировать код с помощью blodwen.

3. Действительно, теперь я также могу подтвердить, что мои проблемы вызваны самим Idris.