하스켈 : 왜이 ​​형식 검사를합니까?

Question

이것은 Reflection-0.5에서 가져온 최소한의 예입니다.

는

>:t Zero 
Zero :: Zero -> Zero 

이 의미가 있습니다 : 나는 제로를 취하고 0을 반환 생성자의 유형에 대한 부탁 해요 GHCi에서

{-# 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 

, 나는 다음과 같은 얻을.

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

내가 유형 그냥 제로 된 형태 변수 '프록시의'일치

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

때문에 뭔가를 쓸 수있는 의미가 있습니다.

마지막으로, 혼란스러운 부분 :

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

제로 :: 제로 생성자의 종류 어떻게 이해하지 않는다 -> 제로 분명히 된 형태 변수 '프록시들'일치하지만은 분명히이 있기 때문에 수행 유형 (reflectNum Zero)은 'a'입니다.

이 예제를 이해하는 데 도움을 주셔서 감사 드리며 관련 개념에 대한 링크는 크게 감사하겠습니다.

감사합니다.

Answer 1

이것은 기능 화살표의 중급 구문입니다. 먼저 이해하기 쉬운 사례를 예로 들어 보겠습니다. Maybe Int. 이 proxy s을 일치하도록하기 위해, 우리는 단지 설정 :

proxy = Maybe 
s = Int 

은 이제 a -> b 대신 Fun a b를 작성, 그래서 Zero Fun Zero Zero (즉 (Fun Zero) Zero)를 입력 가지고있다 척하자. proxy이 (->) Zero입니다, 현실에서

proxy = Fun Zero 
s = Zero 

등 proxy s는 ((->) Zero) Zero ≡ (->) Zero Zero ≡ Zero -> Zero : 그것은 proxy s 일치하기 위해, 우리는 설정합니다.