RankNTypes: áp dụng các chức năng tương tự cho các cặp của các loại khác nhau

Question

Tôi đã cố gắng để xác định chức năng này để tập hợp lại ba danh sách các cặp:

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 


main = do 
    let x = mapAndZip3 (fst) [(1,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5,"cake"),(4,"pudding")] 
    print x -- was expecting [(1,"chips",5), (2,"rice",4)] 

Lúc đầu, tôi đã không bao gồm các RankNTypes hoặc forall, nhưng sau đó sau khi chụp this, cụ thể là định nghĩa liftTup, tôi nghĩ rằng điều đó là đủ.

Nhưng rõ ràng, đó không phải là, như tôi vẫn nhận được một lỗi:

mapAndZip3.hs:8:25: 
Couldn't match type `x' with `(f0 x, b0)' 
    `x' is a rigid type variable bound by 
     a type expected by the context: x -> f0 x at mapAndZip3.hs:8:13 
Expected type: x -> f0 x 
    Actual type: (f0 x, b0) -> f0 x 
In the first argument of `mapAndZip3', namely `(fst)' 

tôi rõ ràng có một sự hiểu biết hạn chế về từ khóa forall, nhưng từ những gì tôi hiểu nó nên, trong trường hợp này, cho phép cho f để chấp nhận bất kỳ loại nào. Những gì tôi không hiểu là: một lần trong một bối cảnh nhất định, và được sử dụng một lần, định nghĩa có được 'cố định' cho bối cảnh còn lại không? Nó không có vẻ như vậy, bởi vì nếu tôi thay thế "chip" và "gạo" với Ints, trình biên dịch vẫn phàn nàn, vì vậy tôi đoán tôi giả định một cái gì đó sai (tất nhiên, nếu tôi loại bỏ chú thích kiểu của mapAndZip3 trong trường hợp sau này, mọi thứ hoạt động vì chữ ký được đơn giản hóa thành mapAndZip3 :: (a -> t) -> [a] -> [a] -> [a] -> [(t, t, t)], nhưng đây không phải là điều tôi muốn).

Tôi cũng thấy question này, nhưng thực sự không thể làm nếu điều này là cùng một vấn đề hay không, kể từ khi chức năng tôi đang cố gắng áp dụng không phải là id, nhưng fst hoặc snd, chức năng mà thực sự trở lại các loại khác nhau (a -> b).

Answer 1

Sự cố trong chữ ký của bạn là f. Chúng ta hãy mở rộng nó một chút:

mapAndZip3 :: forall (a :: *) (b :: *) (c :: *) (f :: *->*) 
      => (forall x. x -> f x) -> [a] -> [b] -> [c] 
           -> [(f a, f b, f c)] 

f đang ở đây nghĩa vụ phải được "bất kỳ chức năng loại cấp", trong instantiation của bạn nó sẽ là type f (a,b) = a. Nhưng Haskell không cho phép bạn tóm tắt các chức năng cấp loại, chỉ hơn nhà xây dựng loại, như Maybe hoặc IO. Vì vậy, mapAndZip3 Just thực sự sẽ có thể, nhưng fst không xây dựng nhưng deconstruct một loại bộ dữ liệu.

Chức năng cấp loại thậm chí không thực sự tồn tại trong Haskell98, chúng chỉ có thể từ TypeFamilies. Vấn đề về cơ bản là ngôn ngữ loại của Haskell không được nhập sai , nhưng chức năng mức loại được yêu cầu phải là tổng hàm . Nhưng sau đó, bạn không thể thực sự xác định bất kỳ chức năng phi vật chất nào (tức là, một khác ngoài id hoặc loại nhà thầu) được xác định trên tất cả các loại. Loại cấp fst chắc chắn không phải là tổng số, nó chỉ hoạt động trên các loại tuple.

Vì vậy, để làm việc với các chức năng như vậy bạn cần xác định rõ ràng ngữ cảnh của chúng theo cách khác. Với TypeFamilies nó có thể làm việc như thế này:

class TypeFunctionDomain d where 
    type TypeFunction d :: * 

instance TypeFunctionDomain (a,b) where 
    type TypeFunction (a,b) = a 

mapAndZip3 :: (forall x. TypeFunctionDomain x => x -> TypeFunction x) 
      -> [a] -> [b] -> [c] 
        -> [(TypeFunction a, TypeFunction b, TypeFunction c)] 

Tuy nhiên, điều này là không thực sự những gì bạn muốn: nó sẽ không thực hiện được xác định trong phạm vi tương tự cũng một TypeFunctionDomain dụ corrsponding để snd, có nghĩa là mapAndZip3 hiệu quả wouldn 't được đa hình ở tất cả, nhưng chỉ làm việc với một chức năng duy nhất.

Các vấn đề này chỉ có thể được giải quyết đúng theo ngôn ngữ được nhập một cách phụ thuộc chẳng hạn như Agda, nơi các loại thực sự chỉ là các loại và bạn có thể xác định hàm loại mức cũng như chức năng mức giá trị. Nhưng điều này đến như một cái gì đó của một mức giá: tất cả các chức năng cần phải được tổng số chức năng! Điều này không thực sự là một điều xấu, nhưng nó có nghĩa là các ngôn ngữ này thường không thực sự Turing-hoàn thành (mà sẽ yêu cầu khả năng lặp/lặp lại vô hạn; tuy nhiên đó là ⟂ đối với đánh giá kết quả đầy đủ).

---

Mọi thứ đã thay đổi một chút với sự ra đời của kind polymorphism etc..

Không giống như trong ví dụ: C++, cho phép - mặc dù với cú pháp rất khủng khiếp - nhập kiểu vịt chức năng cấp loại, thông qua các mẫu. Đó có thể là một tính năng khá hay, nhưng một trong những hậu quả là bạn thường nhận được các thông báo lỗi hoàn toàn không thể đọc được (thậm chí còn ít quan hệ với vấn đề thực hơn Gợi ý "có thể sửa chữa" tồi tệ nhất của GHC ...) khi cố gắng tạo mẫu với một đối số kiểu bên ngoài miền ngầm.

Answer 2

Vấn đề là fst không có các loại cần

(forall x. x -> f x) 

Loại fst là

fst :: (a, b) -> a 

và a không có dạng f (a,b). Các f có một biến mà phải được instantiated với một constructor loại, một cái gì đó như [], Maybe, Either Bool. f không thể chịu được bất kỳ "loại hàm" nào như Λ (a,b) -> a, nó phải là một hàm tạo kiểu.

Nó hoạt động nếu chúng ta cung cấp cho nó một chức năng của các loại yêu cầu (xin lỗi, ví dụ ngu ngốc):

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 

fst0 x = (True,x) 

main = do 
    let x = mapAndZip3 (fst0) [(1 :: Int,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5 :: Int,"cake"),(4,"pudding")] 
    print x 

kể từ đây fst0 có loại a -> ((,) Bool) a, trong đó có hình thức x -> f x.