Вывод типа Идриса для арифметической операции

В следующем коде

Idris> :t \x => x + x
\x => x + x : Integer -> Integer

Idris выводит тип Integer для переменной x, где я думаю, что он должен выводить ограничение интерфейса, как в Haskell:

Haskell> :t (\x y -> x + y)
(\x y -> x + y) :: Num a => a -> a -> a

Тогда он даже не ведет себя как Integer, принимая тип Double:

Idris> (\x => x + x) 2.0 
4.0 : Double

Кто-нибудь может мне это объяснить?


type-inference polymorphism idris
person Ivan Kleshnin    schedule 13.08.2017    source источник
comment
Вывод типа Idris не так совершенен, как в Haskell. С зависимыми типами ваш вывод типа не может быть таким хорошим. Вероятно, здесь происходит что-то похожее на ограничение мономорфизма. Чтобы найти лучшее объяснение этого поведения, вам, вероятно, следует открыть ошибку в репозитории idris-dev: github.com/ idris-lang/Idris-dev/issues   -  person Shersh    schedule 13.08.2017
comment
Зависимые типы @Shersh не влекут за собой каких-либо ограничений на вывод типов для независимых программ. Кроме того, этот случай касается обобщения, а не вывода, и Идрис не имеет обобщения по замыслу, а не по какой-либо фундаментальной причине.   -  person András Kovács    schedule 13.08.2017
comment
@ András Kovács, не могли бы вы направить меня к некоторому контенту на эту тему, у Идриса нет обобщения по теме дизайна?   -  person Ivan Kleshnin    schedule 13.08.2017

Ответы (1)


arrow_upward
0
arrow_downward

Думаю, в целом можно сказать, что проверка вывода типов в REPL idris — плохая идея. Код REPL и код, существующий в файлах Idris, ведут себя по-разному.

Ваша желаемая функция будет записана как:

addy: Num a => a -> a -> a
addy x y = x + y

и будет иметь тип, аналогичный тому, который вы ожидаете от Haskell. Вывод типов в Idris, как правило, очень слаб (потому что он не может быть решен для систем типов с зависимой типизацией).

person Markus    schedule 14.08.2017