Idris: a função funciona com o parâmetro Nat e falha na verificação de tipo com o parâmetro Inteiro
Eu sou novo em Idris. Estou experimentando tipos e minha tarefa é fazer uma "cebola": uma função que usa dois argumentos: um número e qualquer coisa e coloca tudoList
aninhado esse número de vezes.
Por exemplo, o resultado paramkOnion 3 "Hello World"
deveria estar[[["Hello World"]]]
. Eu fiz essa função, este é o meu código:
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
O resultado do trabalho do programa:
[[[4]]]
[['a']]
[[[[["Hello"]]]]]
3.14
É exatamente disso que eu preciso. Mas quando eu faço o mesmo, mas mudo Nat para Inteiro assim
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]
Eu recebo um erro:
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)
Por que a verificação de tipo falha?
Eu acho que isso é porqueInteger
pode assumir valores negativos eType
não pode ser calculado em caso de valores negativos. Se eu estiver certo, como o compilador entende isso?