Thuật toán W sử dụng lược đồ đệ quy

Question

Tôi muốn có thể xây dựng thuật toán suy luận kiểu hindley-milner bằng cách sử dụng các kiểu dữ liệu điểm cố định và lược đồ đệ quy. Bất chấp tất cả chi tiết ngoài những phần đệ quy thực tế:

w env term = case term of 
    Lam n e -> lam (w (modify1 env) e) 
    App a b -> app (w (modify2 env) a) (w (modify3 env) b) 
    ... 

Thuật toán xây dựng một cấu trúc dữ liệu môi trường env vì nó đệ quy đi qua cây cho đến khi nó đạt đến lá. Sau đó, nó sử dụng thông tin này khi nó xây dựng lại kết quả.

Nếu không có phần env, điều này có thể dễ dàng được triển khai với cata. Điều này có thể (với env) được thực hiện nói chung bằng cách sử dụng lược đồ đệ quy không?

Answer 1

Có chỉ cần thực hiện mục tiêu của cata một hàm Env -> a

- luqui

Có, nhưng có thể bạn sẽ cần phải sử dụng cata với một loại tàu sân bậc cao, tính toán một hành động có thể thay đổi môi trường và có thể thất bại.

- pigworker

Answer 2

Nếu không có phần env, điều này có thể dễ dàng thực hiện với Cata. Điều này có thể (với env) được thực hiện nói chung bằng cách sử dụng chương trình đệ quy?

Điều bạn đang tìm kiếm là chronomorphism. Điều này cho phép bạn thực hiện đệ quy bằng cách sử dụng cả hai kết quả từ tương lai và quá khứ. Nó không hoàn toàn thân thiện với người dùng như nó âm thanh, nhưng nó là cách kinh điển để làm việc bằng cách sử dụng các lược đồ đệ quy.