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

因为类型">

仅零"与类型变量"代理 s"匹配。

最后，令人困惑的部分：

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

我不明白构造函数的类型 零 ：： 零 -> 零显然与类型变量"代理 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。