Идрис: функция работает с параметром Nat и не проходит проверку типа с параметром Integer
Я новичок в Идрисе. Я экспериментирую с типами, и моя задача - создать "лук": функцию, которая принимает два аргумента: число и все остальное и помещает все в List
вложенное такое количество раз.
Например, результат для mkOnion 3 "Hello World"
должно быть [[["Hello World"]]]
, Я сделал такую функцию, это мой код:
onionListType : Nat -> Type -> Type
onionListType Z b = b
onionListType (S a) b = onionListType a (List b)
mkOnionList : (x : Nat) -> y -> onionListType x y
mkOnionList Z a = a
mkOnionList (S n) a = mkOnionList n [a]
prn : (Show a) => a -> IO ();
prn a = putStrLn $ show a;
main : IO()
main = do
prn $ mkOnionList 3 4
prn $ mkOnionList 2 'a'
prn $ mkOnionList 5 "Hello"
prn $ mkOnionList 0 3.14
Результат работы программы:
[[[4]]] [['a']] [[[[["Hello"]]]]] 3.14
Это именно то, что мне нужно. Но когда я делаю то же самое, но меняю Nat на Integer вот так
onionListTypeI : Integer -> Type -> Type
onionListTypeI 0 b = b
onionListTypeI a b = onionListTypeI (a-1) (List b)
mkOnionListI : (x : Integer) -> y -> onionListTypeI x y
mkOnionListI 0 a = a
mkOnionListI n a = mkOnionListI (n-1) [a]
Я получаю ошибку:
When checking right hand side of mkOnionListI with expected type onionListTypeI 0 y Type mismatch between y (Type of a) and onionListTypeI 0 y (Expected type)
Почему проверка типов не проходит?
Я думаю это потому что Integer
может принимать отрицательные значения и Type
не может быть вычислено в случае отрицательных значений. Если я прав, как это понимает компилятор?
1 ответ
Вы правы, что тип не может быть вычислен. Но это потому, что onionListTypeI
не является полным Вы можете проверить это в REPL
*test> :total onionListTypeI
Main.onionListTypeI is possibly not total due to recursive path:
Main.onionListTypeI, Main.onionListTypeI
(Или даже лучше, требуя %default total
в исходном коде, что приведет к ошибке.)
Поскольку конструктор типа не тотален, компилятор не нормализуется onionListTypeI 0 y
в y
, Это не тотально, из-за случая onionListTypeI a b = onionListTypeI (a-1) (List b)
, Компилятор знает только, что вычитая 1 из Integer
результаты к Integer
, но не какое именно число (в отличие от Nat
). Это потому, что арифметика с Integer
, Int
, Double
и различные Bits
определяются с основными функциями, такими как prim__subBigInt
, И если эти функции не будут слепыми, у компилятора должна быть проблема с отрицательными значениями, как вы и предполагали.