haskell - 是什么让 Haskell 中的两个类型表达式等效？

Question

所以有人问我这 3 种类型表达式在 Haskell 中是否等效:

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

如果我去掉括号，我就剩下这个

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

所以对我来说很明显它们彼此不同。然而，根据问题，这两个答案都是错误的:

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

所以我在这里有点困惑，正确的答案是什么以及为什么？

Answer 1

事实上，由于您提到的原因，它们都是不同的。

我们甚至可以要求 GHC 确认。 (下面，我选择了a ~ Int来获取封闭类型。)

> 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