Ich fange gerade an, Idris zu lernen, und arbeite gerade an dem Buch Type Driven Development mit Idris . Eine der Beispielaufgaben aus dem zweiten Kapitel besteht darin, eine Funktion zu schreiben, die bei einer gegebenen Zeichenkette die durchschnittliche Länge eines Wortes in dieser Zeichenkette bestimmt. Meine Lösung war wie folgt:
%Vor% Allerdings hatte ich aufgrund der numChars -Zeile große Schwierigkeiten, zu dieser Lösung zu kommen. Aus irgendeinem Grund wird dies nicht überprüft, es sei denn, ich mache den Typ explizit mit the Nat . Der Fehler lautet:
Das macht für mich keinen großen Sinn, denn unabhängig davon, welche Definition von length verwendet wird, ist der Rückgabetyp Nat . Dies wird durch die Tatsache unterstützt, dass dieselbe Sequenz von Operationen in der REPL fehlerfrei durchgeführt werden kann. Was ist der Grund dafür?
Das ist in der Tat ein seltsames, wenn man die Zwischenberechnung map length werds nennt, dann kann Idris auf den Typ schließen:
Und die REPL kann auch folgern, dass sum . map length . words den Typ String -> Nat hat. Wenn Sie hier keine zufriedenstellende Antwort erhalten, empfehle ich, einen Fehlerbericht einzureichen.
Tags und Links type-conversion functional-programming type-inference idris