#idris
Вопрос:
Просто изучая Idris 2 и пытаясь реализовать универсальную функцию приращения, которая могла бы работать с любыми вещественными/целыми числами, насколько я знаю, тип Num должен охватывать дробные числа, поэтому я подумал, что это может удовлетворить требованиям определения:
inc : Num ty => ty -> ty
inc x = x 1
но при запуске этого с двойными числами он терпит неудачу.
Main> inc 2.3
Error: Can't find an implementation for FromDouble Integer.
(Interactive):1:5--1:8
1 | inc 2.3
Есть ли способ расширить Num для этого или существует другой тип, который мог бы мне помочь?
Ответ №1:
Это работает для меня:
inc : Num ty => ty -> ty
inc x = x 1
x : Double
x = inc 2.3
Комментарии:
1. что это значит? означает ли это, что функция правильно определена для работы с любым числовым типом, и это просто означает, что REPL нуждается в определении типа? Я мог бы заставить это работать в REPL, делая это:
the Double $ inc 3.3интересно, есть ли менее подробный способ, но я вижу в вашем примере, что в реальной программе это не понадобится, не могли бы вы немного объяснить это, пожалуйста?