sự khác biệt giữa Fix, Mu và Nu trong Ed Kmett của đệ quy hoạch gói

Question

Trong gói recursion-scheme Ed Kmett là gì, có ba tờ khai:

newtype Fix f = Fix (f (Fix f)) 

newtype Mu f = Mu (forall a. (f a -> a) -> a) 

data Nu f where 
    Nu :: (a -> f a) -> a -> Nu f 

sự khác biệt giữa ba kiểu dữ liệu là gì?

Answer 1

Mu đại diện cho loại đệ quy làm nếp gấp của nó và Nu đại diện cho nó như được mở ra. Trong Haskell, chúng là đẳng cấu và là những cách khác nhau để biểu diễn cùng loại. Nếu bạn giả vờ rằng Haskell không có sự đệ quy tùy ý, sự khác biệt giữa các kiểu này trở nên thú vị hơn: Mu f là điểm cố định (ban đầu) ít nhất là f và Nu f là điểm cố định lớn nhất (đầu cuối) của nó.

Một điểm cố định của f là một loại T một đẳng cấu giữa T và f T, ví dụ: một cặp hàm nghịch in :: f T -> T, out :: T -> f T. Kiểu Fix chỉ sử dụng phép đệ quy kiểu dựng sẵn của Haskell để khai báo trực tiếp đẳng cấu. Nhưng bạn có thể triển khai thực hiện vào/ra cho cả Mu và Nu.

Ví dụ cụ thể, giả vờ trong một khoảnh khắc bạn không thể viết giá trị đệ quy. Cư dân của Mu Maybe, tức là các giá trị :: forall r. (Maybe r -> r) -> r, là các số nguyên bản, {0, 1, 2, ...}; những cư dân của Nu Maybe, tức là các giá trị :: exists x. (x, x -> Maybe x), là các con số {0, 1, 2, ..., ∞}. Hãy suy nghĩ về các giá trị có thể có của các loại này để xem lý do tại sao Nu Maybe có thêm người dân.

Nếu bạn muốn nhận được một số trực giác cho các loại, nó có thể là một bài tập thú vị để thực hiện những điều sau đây mà không đệ quy (khoảng thứ tự tăng dần độ khó):

• zeroMu :: Mu Maybe, succMu :: Mu Maybe -> Mu Maybe
• zeroNu :: Nu Maybe, succNu :: Nu Maybe -> Nu Maybe, inftyNu :: Nu Maybe
• muTofix :: Mu f -> Fix f, fixToNu :: Fix f -> Nu f
• inMu :: f (Mu f) -> Mu f, outMu :: Mu f -> f (Mu f)
• inNu :: f (Nu f) -> Nu f, outNu :: Nu f -> f (Nu f)

Bạn cũng có thể cố gắng thực hiện những việc đó thì phải đệ quy:

• nuToFix :: Nu f -> Fix f, fixToMu :: Fix f -> Mu f

Mu f là điểm cố định tối thiểu, và Nu f là lớn nhất, do đó, viết một hàm :: Mu f -> Nu f là rất dễ dàng, nhưng viết một hàm :: Nu f -> Mu f khó; nó giống như bơi lội ngược dòng.

(Có lúc tôi đã có nghĩa là để viết một lời giải thích chi tiết hơn về các loại, nhưng nó có thể là một chút quá dài cho định dạng này.)