Haskell:为什么这种类型检查？

Question

这是一个取自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',但显然它确实是因为(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 s,我们设置:

proxy = Fun Zero
s = Zero

在现实中,proxy是(->) Zero等proxy s是((->) Zero) Zero≡ (->) Zero Zero≡ Zero -> Zero.