Haskell: Почему эта проверка типов? - PullRequest
Новая
       8

Haskell: Почему эта проверка типов?

6 голосов
/ 24 января 2012

Это минимальный пример, взятый из 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

В GHCi я получаю следующее: 

>:t Zero
Zero :: Zero -> Zero

Это имеет смысл: я спрашиваю тип конструктора, который принимает ноль и возвращает ноль. 

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

Имеет смысл написать что-то вроде 

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

потому что тип Just Zero соответствует переменным типа 'proxy s'.

Наконец, запутанная часть: 

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

Я не понимаю, как тип конструктора Zero :: Zero -> Zero, по-видимому, соответствует переменным типа 'proxy s', но, очевидно, это так, потому что тип (refleNum Zero) просто 'a'.

Буду признателен за помощь в понимании этого примера, и ссылки на соответствующие концепции будут высоко оценены.

Спасибо

1 Ответ

11 голосов
/ 24 января 2012

Это просто инфиксный синтаксис стрелки функции, отбрасывающей вас. Во-первых, вот пример с простым для понимания кейсом: Maybe Int. Чтобы он соответствовал proxy s, мы просто установили: 

proxy = Maybe
s = Int

Теперь давайте представим, что вместо этого a -> b написано Fun a b, и поэтому Zero имеет тип Fun Zero Zero (т.е. (Fun Zero) Zero). Чтобы он соответствовал proxy s, мы устанавливаем: 

proxy = Fun Zero
s = Zero

В действительности proxy - это (->) Zero, и поэтому proxy s - это ((->) Zero) Zero ≡ (->) Zero Zero ≡ Zero -> Zero.

...