Haskell: Tại sao việc kiểm tra kiểu này?

Question

Đây là một ví dụ tối thiểu được lấy từ Reflection-0.5.

{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-} 
{-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in #-} 

import Control.Applicative 
import Data.Proxy 

newtype Zero = Zero Zero deriving (Show) 

class ReifiesNum s where 
    reflectNum :: Num a => proxy s -> a 

instance ReifiesNum Zero where 
    reflectNum = pure 0 

Trong GHCi, tôi nhận được như sau:

>:t Zero 
Zero :: Zero -> Zero 

này có ý nghĩa: Tôi đang yêu cầu cho các loại nhà xây dựng mà phải mất một Zero và trả về một Zero.

>:t reflectNum 
reflectNum :: (ReifiesNum s, Num a) => proxy s -> a 

Nó làm cho cảm giác rằng tôi có thể viết một cái gì đó giống như

>let x = Just (undefined::Zero) 
>reflectNum x 

vì loại Chỉ Zero, phù hợp với các biến kiểu 'Proxy s'.

Cuối cùng, phần khó hiểu:

>:t (reflectNum Zero) 
(reflectNum Zero) :: Num a => a 

Tôi không hiểu làm thế nào các loại nhà xây dựng Zero, :: Zero -> Zero, rõ ràng phù hợp với biến kiểu 'Proxy s', nhưng dường như nó không vì loại (reflectNum Zero) chỉ là 'a'.

Tôi đánh giá cao sự giúp đỡ để hiểu ví dụ này và các liên kết đến các khái niệm có liên quan sẽ được đánh giá cao.

Cảm ơn

Answer 1

Đó chỉ là cú pháp của cú pháp chức năng mà bạn ném. Đầu tiên, đây là một ví dụ với một trường hợp dễ hiểu: Maybe Int. Để làm cho nó phù hợp với proxy s, chúng ta chỉ cần đặt:

proxy = Maybe 
s = Int 

Bây giờ chúng ta hãy giả vờ a -> b được thay bằng văn bản Fun a b, vv Zero có kiểu Fun Zero Zero (ví dụ: (Fun Zero) Zero). Để làm cho nó phù hợp với proxy s, chúng tôi thiết lập:

proxy = Fun Zero 
s = Zero 

Trên thực tế, proxy là (->) Zero, vv proxy s là ((->) Zero) Zero ≡ ≡ (->) Zero ZeroZero -> Zero.