Tại sao các kiểu dữ liệu quy nạp cấm các kiểu như `dữ liệu Xấu a = C (Xấu a -> a)` trong đó kiểu đệ quy xảy ra trước ->?

Question

Hướng dẫn sử dụng Agda trên Inductive Data Types and Pattern Matching tiểu bang:

Để đảm bảo bình thường, xuất hiện quy nạp phải xuất hiện ở các vị trí dương. Ví dụ, các kiểu dữ liệu sau đây không được phép:

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

kể từ khi có một sự xuất hiện tiêu cực của Bad trong đối số để các nhà xây dựng.

Tại sao yêu cầu này lại cần thiết cho các loại dữ liệu quy nạp?

Answer 1

Các kiểu dữ liệu bạn đã là đặc biệt ở chỗ nó là một nhúng của untyped phép tính lambda.

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

unbad : Bad → (Bad → Bad) 
unbad (bad f) = f 

Hãy xem cách thực hiện. Nhớ lại, các phép tính lambda untyped có các điều khoản:

e := x | \x. e | e e' 

Chúng ta có thể định nghĩa một dịch [[e]] từ các thuật ngữ giải tích lambda untyped với các điều khoản Agda loại Bad (mặc dù không phải trong Agda):

[[x]]  = x 
[[\x. e]] = bad (\x -> [[e]]) 
[[e e']] = unbad [[e]] [[e']] 

Bây giờ bạn có thể sử dụng thuật ngữ lambda không được chấm dứt không yêu cầu của bạn để tạo ra một thuật ngữ không kết thúc loại Bad. Ví dụ, chúng ta có thể dịch (\x. x x) (\x. x x) đến sự biểu hiện không chấm dứt kiểu Bad dưới đây:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x)) 

Mặc dù các loại đã xảy ra là một dạng đặc biệt thuận tiện cho việc lập luận này, nó có thể được khái quát hóa với một chút công việc cho bất kỳ loại dữ liệu với các lần xuất hiện âm của đệ quy.

Answer 2

Ví dụ về cách kiểu dữ liệu cho phép chúng tôi tồn tại bất kỳ loại nào được cung cấp trong Turner, D.A. (2004-07-28), Total Functional Programming, giáo phái. 3.1, trang 758 trong Quy tắc 2: Loại đệ quy phải hiệp biến "

---

Hãy làm một ví dụ phức tạp hơn sử dụng Haskell Chúng tôi sẽ bắt đầu với a. "Xấu" kiểu dữ liệu đệ quy

data Bad a = C (Bad a -> a) 

.

và xây dựng Y combinator từ nó mà không có bất cứ một sự đệ quy. Điều này có nghĩa rằng có như vậy một kiểu dữ liệu cho phép chúng ta xây dựng bất kỳ loại đệ quy, hoặc sống trong bất kỳ loại bởi một đệ quy vô hạn.

.210

Y Combinator trong giải tích lambda untyped được định nghĩa là

Y = λf.(λx.f (x x)) (λx.f (x x)) 

Chìa khóa để nó là chúng ta áp dụng x cho chính nó trong x x. Trong các ngôn ngữ đã nhập, điều này không thể trực tiếp thực hiện được vì không có loại x hợp lệ nào có thể có. Nhưng Bad kiểu dữ liệu của chúng tôi cho phép modulo này thêm/gỡ bỏ các nhà xây dựng:

selfApp :: Bad a -> a 
selfApp (x@(C x')) = x' x 

Lấy x :: Bad a, chúng ta có thể unwrap constructor của nó và áp dụng các chức năng bên trong để x riêng của mình. Một khi chúng ta biết làm thế nào để làm điều này, thật dễ dàng để xây dựng các combinator Y:

yc :: (a -> a) -> a 
yc f = let fxx = C (\x -> f (selfApp x)) -- this is the λx.f (x x) part of Y 
     in selfApp fxx 

Lưu ý rằng không selfApp cũng không yc là đệ quy, không có cuộc gọi đệ quy của một hàm cho chính nó. Việc đệ quy chỉ xuất hiện trong kiểu dữ liệu đệ quy của chúng tôi.

Chúng tôi có thể kiểm tra rằng bộ kết hợp được xây dựng thực sự làm những gì cần. Chúng ta có thể thực hiện một vòng lặp vô hạn:

loop :: a 
loop = yc id 

hoặc tính giả GCD:

gcd' :: Int -> Int -> Int 
gcd' = yc gcd0 
    where 
    gcd0 :: (Int -> Int -> Int) -> (Int -> Int -> Int) 
    gcd0 rec a b | c == 0  = b 
        | otherwise = rec b c 
     where c = a `mod` b