Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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?

like image 296
Jaime Fernández Avatar asked Dec 08 '22 13:12

Jaime Fernández


1 Answers

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
like image 68
chi Avatar answered Jan 15 '23 09:01

chi