Ứng dụng thực tế của "Chuối, ống kính, phong bì và dây thép gai"?

Question

Trước hết, tiêu đề ngốc nghếch được trực tiếp tham khảo bài viết này:

http://eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf

Tôi hiểu giá trị lý thuyết điều này, vì nó mô hình hầu hết, nếu không phải tất cả, ngữ nghĩa lập trình.

Các vấn đề nào được giải quyết hiệu quả nhất và thực tế nhất với mô hình lập trình dựa trên điều này? Vấn đề gì không?

Hãy tưởng tượng toàn bộ chương trình được viết ở nơi 80% của tất cả logic liên quan đến các toán tử này. Tôi tự hỏi nếu một ngôn ngữ buộc các nhà khai thác trên người sử dụng có thể tận dụng cơ cấu của họ ...

Answer 1

Bài báo này là một trong một loạt các khám phá lý thuyết liên quan. Khu vực nghiên cứu là những gì các lập trình viên chức năng gọi là lập trình chung (điều gây nhầm lẫn là khác với những gì các lập trình viên C++ gọi là lập trình chung). Ý tưởng là bạn viết các hàm của mình theo cách mà khi bạn xác định một kiểu dữ liệu mới, bạn sẽ tự động nhận được mã mới để đi với nó. Một vấn đề cổ điển mà mọi người muốn giải quyết theo cách này là viết một hình ảnh của dữ liệu vào đĩa và sau đó đọc lại dữ liệu đẳng cấu từ hình ảnh đĩa.

Nếu bạn muốn cảm nhận ứng dụng thực tế của những ý tưởng này, tôi khuyên bạn nên dùng giấy tuyệt vời của Ralf Hinze Generics for the Masses, cho thấy cách bạn có thể thử tất cả những ý tưởng lập dị này trong đồng bằng cũ Haskell. Ví dụ, tôi đã sử dụng các kỹ thuật này để thực hiện thay thế bắt giữ cho các ngôn ngữ trung gian rất phức tạp bên trong các trình biên dịch.

Ralf đã viết một số bài báo hay về lập trình chung, như Jeremy Gibbons. Công cụ của họ không phải là khá xa như chuối, ống kính, và như vậy ...

Answer 2

Điều này có nghĩa là các giải pháp có thể được mô hình hóa trong một mô hình khác. được chuyển đổi thành chương trình khác.

Bây giờ, một số vấn đề nhất định được giải quyết dễ dàng hơn trong một mô hình so với cách khác. Ngoài ra, nó dễ dàng hơn để chứng minh tài sản trong một mô hình hơn trong khác. Vì vậy, nếu bạn có thể cho thấy sự tương đương như vậy, bạn mở cửa để giải quyết một số vấn đề trong dễ dàng hơn, và sau đó chuyển đổi các giải pháp thành mô hình mong muốn.

Điều này cũng tương tự như điều quái vật. Thỏa thuận lớn với monads không phải là cách bạn viết một. Các thỏa thuận lớn với họ là có tấn định lý về monads có thể được áp dụng một khi bạn giảm vấn đề của bạn để một monad. Các nguyên tắc tương tự áp dụng ở đây.