Ich bin neu bei Idris. Ich experimentiere mit Typen und meine Aufgabe ist es, eine "Zwiebel" zu machen: eine Funktion, die zwei Argumente akzeptiert: eine Zahl und was auch immer und setzt was auch immer inList so oft geschachtelt.

Zum Beispiel das Ergebnis fürmkOnion 3 "Hello World" sollte sein[[["Hello World"]]]. Ich habe so eine Funktion gemacht, das ist mein 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

Das Ergebnis der Programmarbeit:

[[[4]]]  
[['a']]  
[[[[["Hello"]]]]]  
3.14

Das ist genau was ich brauche. Aber wenn ich das Gleiche tue, aber Nat in Integer ändere, so

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]

Ich erhalte eine Fehlermeldung:

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)

Warum schlägt die Typprüfung fehl?

Ich denke, das liegt daran,Integer kann negative Werte annehmen undType kann bei negativen Werten nicht berechnet werden. Wenn ich recht habe, wie versteht der Compiler das?