CODEWITHSUNDEEP
haskellfunctional-programmingtype-inferencegadt
Damian Nadales
Damian Nadales

Reputation: 5037

Adventures with Types in Haskell: GADT's: why does the following typechecks?

I'm following this lecture by Simon Peyton-Jones on GADT's. There, the following data-type is declared:

data T a where
  T0 :: Bool -> T Bool
  T1 :: T a

And then the question that is asked is what is the type of the following function:

f x y = case x of
          T0 _ -> True
          T1   -> y

To me, it seems the only possible type is:

f :: T a -> Bool -> Bool

However, the following type:

f :: T a -> a -> a

is also valid! And indeed you could use f as follows:

 f (T1) "hello"

My question is why is the second type signature for f valid?

Upvotes: 4

Views: 197

Answers (2)

chi
chi

Reputation: 116174

Normally, to type check

case e of
  K1 ... -> e1
  K2 ... -> e2
  ...

it is required that all the expressions ei share a common type.

This is still true when using GADTs, except that in each branch the constructor provides some type equality equations T ~ T' which are known to hold in that branch. Hence, when checking that all ei share a common type, we no longer require their types to be identical, but only to be equal when the type equations hold.

In particular:

f :: T a -> a -> a
f x y = -- we know x :: T a , y :: a
   case x of
      T0 _ -> -- provides a ~ Bool
              True   -- has type Bool
      T1   -> -- provides a ~ a (useless)
              y      -- has type a

Here we need to check Bool ~ a which would be false in general, but here becomes true because we only need to check this under the provided equality a ~ Bool. And, in such case, it becomes true!

(To be honest, the type system does something slightly different, checking instead if both branches are equal to the type declared in the signature (under their known equalities) -- but let me keep it simple. For GADT pattern matching such a signature is always required in some form.)

Note that this is the whole point of GADTs -- they allow to type-check pattern matches whose branches apparently involve different types.

Upvotes: 3

sepp2k
sepp2k

Reputation: 370445

There are two cases in the definition of f and both match your second type signature:

T0 _ -> True

Here your argument was of type T Bool and your result is a Bool. So this matches your type signature for a ~ Bool.

T1 ->  y

Here your argument was of type T a and your result is y, which is of type a. So this matches the signature for any a.

To understand why this is type safe, just ask yourself the following question: Is there any way that you could call f, such that the result wouldn't match the type signature? Like could you get back anything other than an a if you passed in a T a and a a?

And the answer is: No, there isn't. If you passed in a T0 (meaning a is Bool), you'll get back a Bool. If you passed in a T1 you'll get back the second argument, which is guaranteed to be of type a as well. If you try to call it like f (T1 :: T Int) "notAnInt", it won't compile because the types don't match. In other words: Any application of the function that matches the type signature will produce the correct result type according to the signature. Therefore f is type safe.

Upvotes: 6

Related Questions