Idris: la función funciona con el parámetro Nat y falla la comprobación de tipo con el parámetro Integer
Soy nuevo en Idris. Estoy experimentando con tipos y mi tarea es hacer una "cebolla": una función que toma dos argumentos: un número y lo que sea y pone lo que sea enList
anidado tal cantidad de veces.
Por ejemplo, el resultado paramkOnion 3 "Hello World"
debiera ser[[["Hello World"]]]
. He hecho tal función, este es mi 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
El resultado del trabajo del programa:
[[[4]]]
[['a']]
[[[[["Hello"]]]]]
3.14
Esto es exactamente lo que necesito. Pero cuando hago lo mismo, pero cambio Nat a Integer así
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]
Me sale un error:
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 qué falla la verificación de tipo?
Creo que esto es porqueInteger
puede tomar valores negativos yType
no se puede calcular en caso de valores negativos. Si tengo razón, ¿cómo entiende esto el compilador?