Có trường hợp sử dụng cho `newtype T = MkT (T -> T)` không?

Question

Các giấy "System F with Type Equality Coercions" bởi Sulzmann, Chakravarty, và Peyton Jones minh họa bản dịch của Haskell của newtype vào hệ thống FC với ví dụ sau:

newtype T = MkT (T -> T) 

Theo tôi được biết, chặn unsafePerformIO, các giá trị chỉ có thể thuộc loại này là MkT id và MkT undefined vì tham số. Tôi tò mò nếu có một số sử dụng thực tế cho định nghĩa này (hoặc tương tự).

Answer 1

Tham số là về các giá trị của các loại với biến. T không có biến, do đó, tham số không áp dụng. Infact, T có nhiều cư dân

ap :: T -> T -> T 
ap (MkT f) t = f t 

idT :: T 
idT = MkT id 

constT :: T 
constT = MkT $ \t -> MkT $ \_ -> t 

axiom_sT :: T 
axiom_sT = MkT $ \f -> MkT $ \g -> MkT $ \a -> (g `ap` a) `ap` (f `ap` a) 

Loại T là một thực hiện các Untyped Lambda Calculus, một phổ biến chính thức hệ thống tương đương trong điện đến một máy Turing. Ba hàm trên (cộng ap) tạo thành phép tính SKI, một hệ thống chính thức tương đương.

Có thể mã hóa bất kỳ kiểu dữ liệu Haskell nào thành T. Xem xét các loại cho các số tự nhiên

data Nat = Zero | Succ Nat 

chúng ta có thể mã hóa Nat vào T

church :: Nat -> T 
church Zero  = MkT $ \f -> MkT $ \x -> x 
church (Succ n) = MkT $ \f -> MkT $ \x -> f `ap` (church n) 

bây giờ, bạn là một phần đúng mặc dù. Không có cách nào trong Haskell để viết hàm nghịch đảo của điều này (cho đến nay như tôi biết). Đó thực sự là một sự xấu hổ. Mặc dù bạn có thể viết một loại psuedo nghịch đảo với loại T -> IO Nat. Ngoài ra, sự hiểu biết của tôi là trình tối ưu hóa GHC có thể chết trên đệ quy newtypes (ai đó vui lòng sửa tôi nếu tôi sai về điều này, bởi vì tôi muốn quay lại sử dụng chúng).

Thay vào đó, các loại

data T = MkT (T -> T) | Failed String 

với

ap (MkT f) a = f a 
ap (Failed s) _ = Failed s 

đó là giải tích lambda với trường hợp ngoại lệ, có thể được sử dụng một cách đầy đủ invertable.

Tóm lại, theo một nghĩa nào đó, tất cả T không phải là loại hữu ích, nhưng theo một nghĩa khác, nó là loại hữu ích nhất trong tất cả.