Po prostu zacząłem uczyć się Idris i pracuję nad książką Typ Driven Development z Idrisem. Jednym z przykładowych ćwiczeń z drugiego rozdziału jest napisanie funkcji, która, biorąc pod uwagę ciąg, określa średnią długość słowa w tym ciągu. Moje rozwiązanie było następująco:Dlaczego ten fragment kodu Idris nie sprawdza się bez wyraźnego typu?
average : String -> Double
average phrase =
let werds = words phrase
numWords = length werds
numChars = the Nat (sum (map length werds)) in
cast numChars/cast numWords
jednak miałem sporo kłopotów przybywającego tego rozwiązania ze względu na linii numChars
. Z jakiegoś powodu nie sprawdza to typowania, chyba że podam typ jawnie za pomocą the Nat
. Stany błędów:
Can't disambiguate since no name has a suitable type:
Prelude.List.length, Prelude.Strings.length
To nie ma dużo sensu dla mnie, ponieważ niezależnie od tego, która definicja length
jest używany, typ zwracany jest Nat
. Potwierdza to fakt, że tę samą sekwencję operacji można wykonać bezbłędnie w REPL. Jaki jest tego powód?