Subsumption trong các loại đa hình

Question

Trong ‘Practical type inference for arbitrary-rank types’, các tác giả nói về subsumption:

tôi cố gắng để kiểm tra mọi thứ trong GHCi như tôi đọc, nhưng mặc dù g k2 có nghĩa là để typecheck, nó doesn' t khi tôi thử với GHC 7.8.3:

λ> :set -XRankNTypes 
λ> let g :: ((forall b. [b] -> [b]) -> Int) -> Int; g = undefined 
λ> let k1 :: (forall a. a -> a) -> Int; k1 = undefined 
λ> let k2 :: ([Int] -> [Int]) -> Int; k2 = undefined 
λ> :t g k1 

<interactive>:1:3: Warning: 
    Couldn't match type ‘a’ with ‘[a]’ 
     ‘a’ is a rigid type variable bound by 
      the type forall a1. a1 -> a1 at <interactive>:1:3 
    Expected type: (forall b. [b] -> [b]) -> Int 
     Actual type: (forall a. a -> a) -> Int 
    In the first argument of ‘g’, namely ‘k1’ 
    In the expression: g k1 
g k1 :: Int 
λ> :t g k2 

<interactive>:1:3: Warning: 
    Couldn't match type ‘[Int] -> [Int]’ with ‘forall b. [b] -> [b]’ 
    Expected type: (forall b. [b] -> [b]) -> Int 
     Actual type: ([Int] -> [Int]) -> Int 
    In the first argument of ‘g’, namely ‘k2’ 
    In the expression: g k2 
g k2 :: Int 

Tôi chưa thực sự hiểu được vấn đề ở đâu nhưng tôi vẫn lo lắng rằng tôi đã hiểu lầm đứng một cái gì đó. Nên typecheck này? Các loại Haskell của tôi có sai không?

Answer 1

Máy đánh chữ doesn't know when to apply the subsumption rule.

Bạn có thể biết khi nào có chức năng sau.

Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n 

Điều này cho biết, với chức năng chuyển đổi cho một loại cụ thể, chúng tôi có thể thực hiện chức năng từ chuyển đổi tự nhiên forall b. f b -> f b.

Sau đó, chúng tôi có thể thử thành công trên ví dụ thứ hai.

Prelude> :t g (u k2) 
g (u k2) :: Int 

Ví dụ đầu tiên hiện cũng đưa ra một lỗi thông tin hơn.

Prelude> :t g (u k1) 
    Couldn't match type `forall a. a -> a' with `[a0] -> [a0]' 
    Expected type: ([a0] -> [a0]) -> Int 
     Actual type: (forall a. a -> a) -> Int 
    In the first argument of `u', namely `k1' 
    In the first argument of `g', namely `(u k1)' 

Tôi không biết liệu chúng tôi có thể viết phiên bản tổng quát hơn của u hay không; chúng ta cần một khái niệm hạn chế về đa hình ít hơn để viết một cái gì đó giống như let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x