CODEWITHSUNDEEP
haskelltypes
mac10688
mac10688

Reputation: 2205

Haskell why does this type check

import Data.Monoid

newtype Constant a b =
    Constant { getConstant :: a }
    deriving (Eq, Ord, Show)

instance Functor (Constant a) where
    fmap _ (Constant a) = Constant a

instance (Monoid a) => Applicative (Constant a) where
    pure x = Constant (mempty x )
    _ <*> (Constant a) = Constant a

--:t (<*>)
--(<*>) :: Applicative f => f (a -> b) -> f a -> f b

--:t Constant (Sum 1)
--Constant (Sum 1) :: Num a => Constant (Sum a) b

--Constant (Sum 1) <*> Constant (Sum 2)
--Constant { getConstant = Sum { getSum = 2 }}

My question is why does the last statement type check?

I expected the left side of <*> to be of type f ( a -> b)
Where
f = Constant
(a -> b) = Sum 1?

There's nothing I can apply to (Sum 1) because it is fully applied, yet this statement compiles.

Upvotes: 2

Views: 130

Answers (3)

Justin L.
Justin L.

Reputation: 13600

For Const:

(<*>) :: Const c (a -> b) -> Const c a -> Const c b

Your input was a Const c (a -> b) a Const c a. You gave a Const c b in return -- if x :: c, then Const x :: Const c a, for any a. It can be Const c Int, Const c Bool, etc.

For example:

Const "Hello" :: Const String Int
Const "Hello" :: Const String Bool
Const "Hello" :: Const String Double
Const "Hello" :: Const String a
Const "Hello" :: Const String (a -> b)
Const "Hello" :: Const String b

all typecheck, because the last parameter can be anything -- "Hello" only constrains the first parameter.

However, you should note that your Applicative instance doesn't obey the Applicative laws.

u <*> pure y = pure ($ y) <*> u

in particular is violated:

Const "hello" <*> pure 4
== Const "hello" <*> Const ""
== Const ""

but

pure ($ 4) <*> Const "hello"
== Const "" <*> Const "hello"
== Const "hello"

Upvotes: 4

Dietrich Epp
Dietrich Epp

Reputation: 213308

The left side is f (a -> b). This is correct.

Remember the type here (let's make 1 :: Int for simplicity):

Constant (Sum 1) :: forall a. Constant (Sum Int) a

I've added the explicit forall. The type checker can unify a with anything.

Try this one:

Constant (Sum 1) :: Constant (Sum Int) (a -> b)

Works fine.

Upvotes: 4

Ian Henry
Ian Henry

Reputation: 22403

Because you have two type variables here:

newtype Constant a b =
    Constant { getConstant :: a }
    deriving (Eq, Ord, Show)

But you only "store" values of the first type, and the second is a phantom.

But your Applicative instance is only concerned with the second type variable that you have -- the b, the elusive phantom.

That means that values like Constant (Sum 1) can have any sort of thing as their second type variable -- it doesn't matter! You can write:

foo :: Constant Sum (a -> b)
foo = Constant (Sum 1)

bar :: Constant Sum String
bar = Constant (Sum 1)

baz :: Constant Sum (IO [Maybe Int])
baz = Constant (Sum 1)

Because you never actually need a value of the phantom type.

Thus when you write Constant (Sum 1) <*> Constant (Sum 2), the type checker infers the correct types:

let foo = Constant (Sum 1) :: Constant Sum (a -> b)
    bar = Constant (Sum 2) :: Constant Sum a
 in foo <*> bar

So the left-hand side of <*> does have the type f (a -> b), but f is Constant Sum, not just Constant.

Upvotes: 3

Related Questions