Haskell: Why is this type-checking?

Question

This is a minimal example taken from 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 

In GHCi, I get the following:

 >:t Zero Zero :: Zero -> Zero 

This makes sense: I am asking for a constructor type that takes zero and returns zero.

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

It makes sense that I could write something like

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

because the Just Zero type corresponds to the proxy server of type variables.

Finally, the confusing part:

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

I don’t understand how the constructor type Zero :: Zero → Zero seems to correspond to the proxy server of variable types s, but apparently this is because the type (reflectNum Zero) is just "a".

I would appreciate understanding of this example, as well as links to related concepts.

thanks

Answer 1

This is just the syntax of the arrow function throwing you away. First, here is an example with an easily understood case: Maybe Int . To make it match proxy s , we simply set:

 proxy = Maybe s = Int 

Now let's pretend that a -> b instead written Fun ab , and therefore Zero is of type Fun Zero Zero (i.e. (Fun Zero) Zero ). To make it match proxy s , we set:

 proxy = Fun Zero s = Zero 

In fact, proxy is (->) Zero , so proxy s is ((->) Zero) Zero ≡ (->) Zero Zero ≡ Zero -> Zero .