Chức năng Haskell trả về kiểu tồn tại

Question

Có thể viết hàm Haskell để sinh ra một kiểu tham số trong đó tham số kiểu chính xác bị ẩn không? I E. một cái gì đó như f :: T -> (exists a. U a)? Nỗ lực rõ ràng:

{-# LANGUAGE ExistentialQuantification #-} 

data D a = D a 

data Wrap = forall a. Wrap (D a) 

unwrap :: Wrap -> D a 
unwrap (Wrap d) = d 

thất bại trong việc biên dịch với:

Couldn't match type `a1' with `a' 
    `a1' is a rigid type variable bound by 
     a pattern with constructor 
     Wrap :: forall a. D a -> Wrap, 
     in an equation for `unwrap' 
     at test.hs:8:9 
    `a' is a rigid type variable bound by 
     the type signature for unwrap :: Wrap -> D a at test.hs:7:11 
Expected type: D a 
    Actual type: D a1 
In the expression: d 
In an equation for `unwrap': unwrap (Wrap d) = d 

Tôi biết đây là một ví dụ giả tạo, nhưng tôi tò mò nếu có một cách để thuyết phục GHC rằng tôi không quan tâm cho loại chính xác mà D được tham số hóa, mà không đưa vào một loại trình bao bọc tồn tại khác cho kết quả của unwrap.

Để làm rõ, tôi làm muốn loại an toàn, nhưng cũng muốn để có thể áp dụng một hàm dToString :: D a -> String mà không quan tâm đến a (ví dụ bởi vì nó chỉ trích ra một lĩnh vực String từ D) để kết quả của unwrap. Tôi nhận ra có nhiều cách khác để đạt được nó (ví dụ: định nghĩa wrapToString (Wrap d) = dToString d) nhưng tôi quan tâm hơn đến việc liệu có lý do cơ bản nào không cho phép ẩn giấu như vậy dưới sự tồn tại.

Answer 1

Có, bạn có thể, nhưng không phải là một cách đơn giản.

{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE RankNTypes #-} 

data D a = D a 

data Wrap = forall a. Wrap (D a) 

unwrap :: Wrap -> forall r. (forall a. D a -> r) -> r 
unwrap (Wrap x) k = k x 

test :: D a -> IO() 
test (D a) = putStrLn "Got a D something" 

main = unwrap (Wrap (D 5)) test 

Bạn không thể trả về một D something_unknown từ chức năng của bạn, nhưng bạn có thể giải nén nó và ngay lập tức vượt qua nó đến một chức năng chấp nhận D a, như được hiển thị.  

Answer 2

Có, bạn có thể thuyết phục GHC rằng bạn không quan tâm đến loại chính xác mà D được tham số hóa. Chỉ là, đó là một ý tưởng khủng khiếp.

{-# LANGUAGE GADTs #-} 

import Unsafe.Coerce 

data D a = D a deriving (Show) 

data Wrap where  -- this GADT is equivalent to your `ExistentialQuantification` version 
    Wrap :: D a -> Wrap 

unwrap :: Wrap -> D a 
unwrap (Wrap (D a)) = D (unsafeCoerce a) 

main = print (unwrap (Wrap $ D "bla") :: D Integer) 

Đây là những gì xảy ra khi tôi thực hiện mà chương trình đơn giản:

và như vậy, cho đến khi tiêu thụ bộ nhớ mang xuống hệ thống.

Các loại quan trọng! Nếu bạn phá vỡ hệ thống kiểu, bạn phá vỡ bất kỳ khả năng dự đoán nào của chương trình của bạn (tức là mọi thứ có thể xảy ra, bao gồm thermonuclear war hoặc demons flying out of your nose nổi tiếng).

---

Bây giờ, rõ ràng bạn nghĩ rằng các loại cách nào đó hoạt động khác nhau. Trong các ngôn ngữ động như Python, và cũng ở một mức độ trong các ngôn ngữ OO như Java, một kiểu theo nghĩa là một thuộc tính mà một giá trị có thể có. Vì vậy, các giá trị (tham chiếu) không chỉ mang theo thông tin cần thiết để phân biệt các giá trị khác nhau của một loại đơn, mà còn thông tin để phân biệt các loại (phụ) khác nhau. Đó là trong nhiều giác quan khá kém hiệu quả – đó là một lý do chính tại sao Python là quá chậm và Java cần một máy ảo rất lớn.

Trong Haskell, các loại không tồn tại khi chạy. Một hàm không bao giờ biết loại giá trị mà nó làm việc. Chỉ vì trình biên dịch biết tất cả về các loại nó sẽ có, chức năng không cần bất kỳ kiến ​​thức nào như vậy – trình biên dịch đã mã hóa cứng nó! (Tức là, trừ khi bạn phá vỡ nó với unsafeCoerce, mà như tôi đã giải thích là như không an toàn như âm thanh.)

Nếu bạn muốn đính kèm kiểu như một “ tài sản ” đến một giá trị, bạn cần phải làm điều đó một cách rõ ràng và đó là những gì những trình bao bọc tồn tại đó có. Tuy nhiên, thường có những cách tốt hơn để làm điều đó bằng một ngôn ngữ chức năng. Ứng dụng của bạn thực sự là gì?

---

Có lẽ cũng hữu ích khi nhớ lại chữ ký với kết quả đa hình nghĩa là gì. unwrap :: Wrap -> D a không có nghĩa là “ kết quả là một số D a ... và người gọi tốt hơn không quan tâm đến số a đã sử dụng ”. Đó sẽ là trường hợp trong Java, nhưng nó sẽ là khá vô ích trong Haskell bởi vì không có gì bạn có thể làm với một giá trị của loại không rõ.

Thay vào đó có nghĩa là: cho bất kỳ điều gì loại a yêu cầu người gọi, chức năng này có thể cung cấp giá trị D a phù hợp. Tất nhiên đây là khó khăn để cung cấp – mà không cần thêm thông tin nó chỉ là không thể như làm bất cứ điều gì với một giá trị của loại chưa biết. Nhưng nếu đã có a giá trị trong luận, hoặc a được bằng cách nào đó hạn chế đến một lớp kiểu (ví dụ fromInteger :: Num a => Integer -> a, sau đó nó khá tốt và rất hữu ích.

---

Để có được một String lĩnh vực – không phụ thuộc vào a tham số – bạn chỉ có thể hoạt động trực tiếp trên giá trị gói:

data D a = D 
    { dLabel :: String 
    , dValue :: a 
    } 

data Wrap where Wrap :: D a -> Wrap 

labelFromWrap :: Wrap -> String 
labelFromWrap (Wrap (D l _)) = l 

Để viết các chức năng như trên Wrap hơn chung (với bất kỳ “ nhãn accesor mà không quan tâm đến a ”), sử dụng Rank2-đa hình như được hiển thị trong câu trả lời của n.m.