Tại sao suy luận kiểu của F # lại thay đổi?

Question

Trình biên dịch F # xuất hiện để thực hiện suy luận kiểu trong một (khá) nghiêm ngặt từ trên xuống dưới, từ trái sang phải. Điều này có nghĩa là bạn phải làm mọi thứ như đặt tất cả các định nghĩa trước khi sử dụng, thứ tự biên dịch tệp là quan trọng và bạn có xu hướng cần sắp xếp lại nội dung (qua |> hoặc bạn có gì) để tránh có chú thích loại rõ ràng.

Làm cách nào để nó linh hoạt hơn và được lên kế hoạch cho phiên bản F # trong tương lai? Rõ ràng nó có thể được thực hiện, kể từ Haskell (ví dụ) không có những hạn chế như vậy với suy luận mạnh mẽ như nhau. Có điều gì khác biệt về thiết kế hay ý thức hệ của F # đang gây ra điều này?

Answer 1

Về "suy luận mạnh mẽ của Haskell", tôi không nghĩ Haskell có để đối phó với

• OO kiểu subtyping động (các lớp học kiểu có thể làm một số công cụ tương tự, nhưng các lớp học kiểu dễ gõ/suy luận)
• phương pháp quá tải (các lớp học kiểu có thể làm một số công cụ tương tự, nhưng loại lớp dễ dàng nhập/suy luận hơn)

Tức là, tôi nghĩ F # phải đối phó với một số thứ khó mà Haskell không làm. (Gần như chắc chắn, Haskell phải đối phó với một số thứ khó mà F # không.Như được đề cập bởi các câu trả lời khác, hầu hết các ngôn ngữ chính của .NET đều có công cụ Visual Studio như là một ảnh hưởng lớn về thiết kế ngôn ngữ (xem ví dụ như LINQ có "từ ... chọn" thay vì SQL-y "như thế nào?" chọn ... từ ", được thúc đẩy bằng cách lấy intellisense từ tiền tố chương trình). Intellisense, error squiggles, và error-message comprehensibility là tất cả các yếu tố công cụ thông báo cho thiết kế F #. Bạn có thể làm tốt hơn và phỏng đoán thêm (mà không phải hy sinh những trải nghiệm khác), nhưng tôi không nghĩ rằng đó là một trong những ưu tiên cao của chúng tôi đối với các phiên bản ngôn ngữ trong tương lai. (Các Haskellers có thể thấy suy luận kiểu F # là hơi yếu, nhưng chúng có lẽ cao hơn nhiều so với C# ers, những người thấy suy luận kiểu F # rất mạnh. :))

Cũng có thể khó mở rộng suy luận kiểu trong một không phá vỡ thời trang; có thể thay đổi chương trình bất hợp pháp thành chương trình hợp pháp trong phiên bản tương lai, nhưng bạn phải rất cẩn thận để đảm bảo các chương trình pháp lý trước đó không thay đổi ngữ nghĩa theo quy tắc suy luận mới và độ phân giải tên (một cơn ác mộng khủng khiếp ở mọi ngôn ngữ) để tương tác với các thay đổi kiểu suy luận theo những cách đáng ngạc nhiên.

Answer 2

F # sử dụng một đường chuyền biên soạn như vậy bạn chỉ có thể tham khảo các loại hoặc chức năng mà đã được xác định hoặc trước đó trong file bạn hiện tại hoặc xuất hiện trong một tập tin mà được quy định trước đó trong thứ tự biên dịch.

Gần đây tôi đã hỏi Don Syme về việc thực hiện nhiều nguồn chuyển để cải thiện quy trình suy luận loại . trả lời của ông là "Vâng, nó có thể làm đa-pass loại suy luận. Ngoài ra còn có single-pass biến thể tạo ra một tập hợp hữu hạn những hạn chế.

Tuy nhiên những phương pháp tiếp cận có xu hướng cung cấp cho thông báo lỗi xấu và nghèo kết quả intellisense trong trình chỉnh sửa trực quan . "

http://www.markhneedham.com/blog/2009/05/02/f-stuff-i-get-confused-about/#comment-16153

Answer 3

Tôi nghĩ rằng các thuật toán được sử dụng bởi F # có những lợi ích mà nó rất dễ dàng để (ít nhất là xấp xỉ) giải thích cách thức hoạt động, do đó khi bạn hiểu nó, bạn có thể có một số dự đoán về kết quả.

Thuật toán sẽ luôn có một số hạn chế. Hiện tại, khá dễ hiểu chúng. Đối với các thuật toán phức tạp hơn, điều này có thể khó khăn. Ví dụ: tôi nghĩ bạn có thể gặp phải tình huống mà bạn cho rằng thuật toán có thể suy ra điều gì đó - nhưng nếu nó đủ chung để bao trùm trường hợp, nó sẽ không thể giải mã được (ví dụ: có thể lặp lại mãi mãi).

Một ý nghĩ khác là kiểm tra mã từ trên xuống dưới tương ứng với cách chúng ta đọc mã (ít nhất là đôi khi). Vì vậy, có thể là thực tế là chúng tôi có xu hướng viết mã theo cách cho phép loại suy luận cũng làm cho mã dễ đọc hơn đối với ...

Answer 4

Có điều gì khác biệt về thiết kế hoặc ý thức hệ của F # đang gây ra điều này không?

Có. F # sử dụng danh nghĩa chứ không phải là gõ cấu trúc vì nó đơn giản hơn và do đó, dễ dàng hơn cho các con người chỉ sử dụng.

Xem xét việc này F # ví dụ:

let lengths (xss: _ [] []) = Array.map (fun xs -> xs.Length) xss 

let lengths (xss: _ [] []) = xss |> Array.map (fun xs -> xs.Length) 

Các cựu không biên dịch vì loại xs bên trong hàm ẩn danh không thể được suy ra vì F # không thể diễn tả kiểu "một số lớp học với thành viên Length".

Ngược lại, OCaml thể diễn tả tương đương trực tiếp:

let lengths xss = Array.map (fun xs -> xs#length) xss 

vì OCaml thể diễn tả kiểu đó (nó được viết <length: 'a ..>). Lưu ý rằng điều này đòi hỏi suy luận kiểu mạnh mẽ hơn F # hoặc Haskell hiện có, ví dụ: OCaml có thể suy ra các loại tổng hợp.

Tuy nhiên, tính năng này được biết là một vấn đề về khả năng sử dụng. Ví dụ, nếu bạn vít lên ở nơi khác trong mã thì trình biên dịch vẫn chưa suy ra rằng loại xs được cho là một mảng vì vậy bất kỳ thông báo lỗi nào mà nó có thể cung cấp chỉ có thể cung cấp thông tin như "một số loại có độ dài" và không phải là "một mảng". Chỉ với mã hơi phức tạp hơn, điều này nhanh chóng mất kiểm soát khi bạn có các loại lớn với nhiều thành viên suy luận cấu trúc không hoàn toàn thống nhất, dẫn đến các thông báo lỗi không thể hiểu được (C++/STL).

Answer 5

Câu trả lời ngắn gọn là F # được dựa trên truyền thống của SML và OCaml, trong khi Haskell xuất phát từ một thế giới hơi khác biệt của Miranda, Gofer và tương tự. Sự khác biệt trong truyền thống lịch sử là tinh tế, nhưng phổ biến. Sự khác biệt này song song với các ngôn ngữ hiện đại khác, chẳng hạn như Coq giống như ML, có cùng giới hạn đặt hàng so với Agda giống như Haskell mà không có.

Sự khác biệt này có liên quan đến đánh giá chậm và nghiêm ngặt. Phía Haskell của vũ trụ tin vào sự lười biếng, và một khi bạn đã tin vào sự lười biếng, ý tưởng thêm sự lười biếng vào những thứ như suy luận kiểu là không có trí tuệ.Trong khi ở phía ML của vũ trụ bất cứ khi nào sự lười biếng hoặc đệ quy lẫn nhau là cần thiết, nó phải được ghi chú rõ ràng bằng cách sử dụng các từ khóa như với, và, rec, v.v. mã soạn sẵn, nhưng có rất nhiều người nghĩ rằng tốt hơn là làm cho những điều này rõ ràng.