なぜこのIdrisスニペット型チェックは明示的な型なしではありませんか？

Question

私はIdrisの学習を始めようとしています。私はIdrisでタイプドリブン開発を使って作業しています。 2番目の章の演習の1つは、文字列を与えられた文字列の単語の平均長さを決定する関数を書くことです。私のソリューションは、以下の通りであった：

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

しかし、私はトラブルnumCharsラインのために、このソリューションに到着するのがたくさんありました。なんらかの理由で、タイプをthe Natを使って明示的にしない限り、これは型チェックを行いません。エラー状態は：

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

これは関係なく、lengthの定義は、戻り値の型がNatで使用されているのため、私には意味の全体の多くを作成しません。これは、この同じ一連の操作がREPLでエラーなしで実行できるという事実によってサポートされています。これの理由は何ですか？

Answer 1

これは確かにあなたが中間の計算map length werdsに名前を付けるならば、イドリスは型を推論することが可能であることを考えると奇妙なものです：

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

そして、REPLもsum . map length . wordsがString -> Natを入力していることを推測することができます。満足のいく答えが得られない場合は、a bug reportを提出することをお勧めします。

Answer 2

これは実装のバグです。 IdrisはIdris自身ではなく、Haskellで書かれています。 Haskellには従属型がないため、バグが発生しやすくなります。多分、ある日、Idrisはそれ自身で書き直されるでしょう。