Warum nicht diese Idisis Schnipsel Typcheck ohne einen expliziten Typ?

Question

Ich bin gerade dabei, Idris zu lernen, und ich arbeite durch das 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:

average : String -> Double 
average phrase = 
    let werds = words phrase 
     numWords = length werds 
     numChars = the Nat (sum (map length werds)) in 
    cast numChars/cast numWords 

Allerdings habe ich eine Menge Ärger hatte aufgrund der numChars Linie bei dieser Lösung zu erzielen. Aus irgendeinem Grund wird dies nicht überprüft, es sei denn, ich mache den Typ explizit mit the Nat. Die Fehlerzustände:

Can't disambiguate since no name has a suitable type: 
     Prelude.List.length, Prelude.Strings.length 

Dies gilt nicht eine ganze Menge Sinn für mich, da unabhängig von der Definition von length verwendet wird, der Rückgabetyp ist 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? Diese

Answer 1

ist in der Tat eine seltsame ein gegeben, dass, wenn Sie die Zwischenrechen nennen map length werds dann Idris der Lage ist, den Typ zu folgern:

average : String -> Double 
average phrase = 
    let werds = words phrase 
     numWords = length werds 
     swerds = map length werds 
     numChars = sum swerds in 
    cast numChars/cast numWords 

Und die REPL ist auch in der Lage zu folgern, dass sum . map length . wordsString -> Nat hat geben. Wenn Sie hier keine zufriedenstellende Antwort erhalten, empfehle ich die Einreichung a bug report.

Answer 2

Es ist ein Implementierungsfehler. Idris wird eher in Haskell geschrieben als in Idris selbst. Da Haskell keine abhängigen Typen hat, sind Fehler wahrscheinlicher. Vielleicht wird Idris eines Tages in sich selbst umgeschrieben werden.