Tại sao đoạn mã Idris này không gõ một loại rõ ràng?

Question

Tôi chỉ mới bắt đầu học Idris và tôi đang làm việc thông qua cuốn sách Phát triển định hướng kiểu với Idris. Một trong những bài tập ví dụ từ chương thứ hai là viết một hàm, được đưa ra một chuỗi, xác định chiều dài trung bình của một từ trong chuỗi đó. Giải pháp của tôi là như sau:

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

Tuy nhiên, tôi gặp rất nhiều rắc rối khi đến giải pháp này do đường dây numChars. Đối với một số lý do, điều này không typecheck trừ khi tôi làm cho loại rõ ràng bằng cách sử dụng the Nat. Các trạng thái lỗi:

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

này không làm cho một toàn bộ rất nhiều ý nghĩa với tôi, vì bất kể là định nghĩa của length được sử dụng, kiểu trả về là Nat. Điều này được hỗ trợ bởi thực tế rằng cùng một chuỗi các hoạt động này có thể được thực hiện không có lỗi trong REPL. Lý do cho việc này là gì?

Answer 1

Đây thực sự là một kỳ lạ cho rằng nếu bạn đặt tên cho tính toán trung gian map length werds sau đó Idris có thể suy ra các loại:

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

Và REPL cũng có thể suy ra rằng sum . map length . words có kiểu String -> Nat. Nếu bạn không nhận được bất kỳ câu trả lời thỏa đáng nào ở đây, tôi khuyên bạn nên nộp a bug report.

Answer 2

Đó là lỗi triển khai. Idris được viết bằng Haskell chứ không phải trong bản thân Idris. Vì Haskell không có loại phụ thuộc, lỗi có nhiều khả năng hơn. Có lẽ, một ngày nào đó, Idris sẽ tự viết lại.