Pourquoi cet extrait de code Idris ne contient-il pas un type explicite?

Question

Je commence juste à apprendre Idris, et je travaille à travers le livre Type Driven Development avec Idris. L'un des exemples d'exercices du deuxième chapitre consiste à écrire une fonction qui, étant donné une chaîne, détermine la longueur moyenne d'un mot dans cette chaîne. Ma solution est la suivante:

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

Cependant, j'ai eu beaucoup de mal à arriver à cette solution en raison de la ligne numChars. Pour quelque raison, cela ne correspond pas à moins que je rende le type explicite en utilisant the Nat. Les états d'erreur:

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

Cela ne fait pas beaucoup de sens pour moi, car quelle que soit la définition de length est utilisé, le type de retour est Nat. Ceci est supporté par le fait que cette même séquence d'opérations peut être effectuée sans erreur dans le REPL. Quelle est la raison de cela?

Answer 1

C'est en effet un étrange étant donné que si vous nommez le calcul intermédiaire map length werds alors Idris est en mesure de déduire le type:

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

Et le REPL est également en mesure de déduire que sum . map length . words est de type String -> Nat. Si vous n'obtenez pas de réponse satisfaisante ici, je suggère de déposer a bug report.

Answer 2

C'est un bogue d'implémentation. Idris est écrit dans Haskell plutôt que dans Idris lui-même. Comme Haskell n'a pas de types dépendants, les bugs sont plus probables. Peut-être, un jour, Idris sera réécrit en lui-même.