Search code examples
haskelltypesequivalence

What makes two type expressions in Haskell equivalent?


So I was asked whether these 3 type expressions where equivalent in Haskell:

τ1 = (a -> a) -> (a -> a -> a)
τ2 = a -> a -> ((a -> a) -> a)
τ3 = a -> a -> (a -> (a -> a))

if I take away the parenthesis I'm left with this

τ1 = (a -> a) -> a -> a -> a
τ2 = a -> a -> (a -> a) -> a
τ3 = a -> a -> a -> a -> a

So it's obvious to me that they are all different from each other. However, according to the question, these two answers are wrong:

τ1 !≡ τ2 !≡ τ3 !≡ τ1
τ1 !≡ τ2 ≡ τ3

So I'm a bit confused right here, what would be the right answer and why?


Solution

  • Indeed, they are all distinct for the reason you mention.

    We can even ask GHC to confirm it. (Below, I chose a ~ Int to obtain a closed type.)

    > import Data.Type.Equality
    > type T1 a = (a -> a) -> (a -> a -> a)
    > type T2 a = a -> a -> ((a -> a) -> a)
    > type T3 a = a -> a -> (a -> (a -> a))
    > :kind! T1 Int == T2 Int
    T1 Int == T2 Int :: Bool
    = 'False
    > :kind! T1 Int == T3 Int
    T1 Int == T3 Int :: Bool
    = 'False
    > :kind! T2 Int == T3 Int
    T2 Int == T3 Int :: Bool
    = 'False