Chức năng như thế này thường gặp phải trong combinators điểm cố định. ví dụ. một hình thức của Y combinator được viết λf.(λx.f (x x)) (λx.f (x x))
. Các bộ phối hợp điểm cố định được sử dụng để thực hiện phép đệ quy chung trong phép tính lambda không định dạng mà không có bất kỳ cấu trúc đệ quy bổ sung nào, và đây là một phần của những gì làm cho phép tính lambda chưa hoàn thành Turing-complete.
Khi mọi người phát triển simply-typed lambda calculus, đó là một hệ thống kiểu tĩnh ngây thơ trên đỉnh phép tính lambda, họ phát hiện ra rằng không còn khả năng viết các hàm như vậy nữa. Trong thực tế, không thể thực hiện đệ quy chung trong phép tính lambda được đánh máy đơn giản; và do đó, tính toán lambda đơn giản, không còn là Turing-complete. (Một hiệu ứng phụ thú vị là các chương trình trong tính toán lambda đơn giản đã gõ luôn luôn là chấm dứt.)
Các ngôn ngữ lập trình tĩnh được tạo sẵn để khắc phục vấn đề, chẳng hạn như các hàm đệ quy được đặt tên (được xác định với val rec
hoặc fun
) và được đặt tên theo kiểu dữ liệu đệ quy.
Vẫn có thể sử dụng kiểu dữ liệu đệ quy để mô phỏng thứ gì đó giống như những gì bạn muốn, nhưng nó không đẹp.
Về cơ bản, bạn muốn xác định loại như 'a foo = 'a foo -> 'a
; tuy nhiên, điều này là không được phép. Bạn thay vì bọc nó trong một datatype: datatype 'a foo = Wrap of ('a foo -> 'a);
datatype 'a foo = Wrap of ('a foo -> 'a);
fun unwrap (Wrap x) = x;
Về cơ bản, Wrap
và unwrap
được sử dụng để chuyển đổi giữa 'a foo
và 'a foo -> 'a
, và ngược lại.
Bất cứ khi nào bạn cần tự gọi một hàm, thay vì x x
, bạn phải viết rõ ràng (unwrap x) x
(hoặc unwrap x x
); tức là unwrap
biến nó thành một hàm mà sau đó bạn có thể áp dụng cho giá trị ban đầu.
P.S. Một ngôn ngữ ML khác, OCaml, có một tùy chọn để kích hoạt các kiểu đệ quy (thường bị vô hiệu hóa); nếu bạn chạy trình thông dịch hoặc trình biên dịch với cờ -rectypes
, thì có thể viết những thứ như fun x -> x x
. Về cơ bản, đằng sau hậu trường, trình kiểm tra kiểu sẽ tìm ra những nơi bạn cần "quấn" và "unwrap" loại đệ quy, sau đó chèn chúng cho bạn. Tôi không biết bất kỳ việc triển khai ML tiêu chuẩn nào có chức năng đệ quy kiểu tương tự.
Nếu có ai quan tâm, tôi thấy rằng điều này được gọi là [U Kết hợp (xem dưới cùng của trang)] (http://www.ucombinator.org/), nhưng không thể tìm thấy nhiều hơn về nó. –
Tôi không biết nó được gọi là bộ kết hợp U, nhưng như trang đó nói, nó được sử dụng để xây dựng chương trình không kết thúc (rõ ràng là ngắn nhất) của phép tính lambda chưa được phân loại mà tôi đưa vào câu trả lời của tôi. –