I am new to Idris. I am experimenting with types and my task is to make an "onion": a function that takes two arguments: a number and whatever and puts whatever into
List nested such number of times.
For example, the result for
mkOnion 3 "Hello World" should be
I've made such a function, this is my code:
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
The result of program work:
[[]] [['a']] [[[[["Hello"]]]]] 3.14
This is exactly what I need. But when I do the same, but change Nat to Integer like this
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]
I get an 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)
Why does type checking fails?
I think this is because
Integer can take negative values and
Type can't be computed in case of negative values. If I am right, how does the compiler understand this?