Idris: Funktion arbeitet mit Nat-Parameter und Fehlertyp Überprüfung mit Integer-Parameter

Question

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 alles in List so oft verschachtelt. Das Ergebnis für mkOnion 3 "Hello World" sollte [[["Hello World"]]] lauten. Ich habe eine solche Funktion hat, 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 das, was ich brauche. Aber wenn ich das gleiche tun, aber Nat wie diese

zu Integer ändern

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] 

bekomme ich einen Fehler:

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 geben Sie nicht Überprüfung fehlschlägt?

Ich denke, das ist, weil Integer kann negative Werte und Type kann nicht im Falle von negativen Werten berechnet werden. Wenn ich recht habe, wie versteht der Compiler das?

Answer 1

Sie haben Recht, dass der Typ nicht berechnet werden kann. Aber das ist, weil die onionListTypeI nicht insgesamt ist. Sie können dies in dem

*test> :total onionListTypeI 
Main.onionListTypeI is possibly not total due to recursive path: 
    Main.onionListTypeI, Main.onionListTypeI 

REPL überprüfen (Oder noch besser, %default total im Quellcode fordern, die einen Fehler auslösen würde.)

Da der Typkonstruktor nicht total ist, wird der Compiler nicht normalisieren onionListTypeI 0 y zu y. Es ist nicht total, wegen des Falls onionListTypeI a b = onionListTypeI (a-1) (List b). Der Compiler weiß nur, dass 1 von einem Integer Ergebnis zu einem Integer subtrahiert wird, aber nicht welche Nummer genau (anders als bei einer Nat). Dies liegt daran, dass die Arithmetik mit Integer, Int, Double und die verschiedenen Bits mit primären Funktionen wie prim__subBigInt definiert sind. Und wenn diese Funktionen nicht blind wären, sollte der Compiler ein Problem mit negativen Werten haben, wie Sie angenommen haben.