Dlaczego ten fragment kodu Idris nie sprawdza się bez wyraźnego typu?

Question

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:

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?

Answer 1

To rzeczywiście dziwne, biorąc pod uwagę, że jeden, jeśli wymienić pośredni obliczeń map length werds następnie Idris jest w stanie ustalić typ:

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

A REPL jest również w stanie wywnioskować, że sum . map length . words ma typ String -> Nat. Jeśli nie znajdziesz tutaj zadowalającej odpowiedzi, proponuję zgłoszenie a bug report.

Answer 2

To błąd związany z implementacją. Idris jest napisany raczej w Haskell niż w samym Idrisie. Ponieważ Haskell nie ma typów zależnych, błędy są bardziej prawdopodobne. Być może pewnego dnia Idrys zostanie przepisany sam w sobie.