在 Haskell 中，什么使两个类型表达式相等？

Question

我被问及这三种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

我有些困惑，什么是正确答案，为什么？

- Jaime Fernández

---

其他答案是错误的。 - Jaime Fernández

我会仔细检查我是否正确复制了问答内容。如果没有发现错误，我建议您向您的教师（假设他们编写了测试）报告此问答内容。 - chi

假设这个符号是在类中或者之前的测试中定义的。否则，如果这个符号完全没有定义，那么这个问题当然是无法回答的。但是我们没有像你们一样访问材料来搜索定义，所以... - Daniel Wagner

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

- chi

Answer 2

The three types...

type T1 a = (a -> a) -> (a -> a -> a)
type T2 a = a -> a -> ((a -> a) -> a)
type T3 a = a -> a -> (a -> (a -> a))

...确实是不同的。然而，T1和T2在某种意义上是等价的，这意味着它们之间存在一个同构，该同构等同于改变参数的顺序：

GHCi> :info T1
type T1 a = (a -> a) -> a -> a -> a
    -- Defined at <interactive>:12:1
GHCi> :info T2
type T2 a = a -> a -> (a -> a) -> a
    -- Defined at <interactive>:13:1

GHCi> :t flip
flip :: (a -> b -> c) -> b -> a -> c
GHCi> :t (flip .)
(flip .) :: (a1 -> a2 -> b -> c) -> a1 -> b -> a2 -> c

GHCi> f = (flip .) . flip
GHCi> :t f :: T1 a -> T2 a
f :: T1 a -> T2 a :: T1 a -> T2 a
GHCi> g = flip . (flip .)
GHCi> :t g :: T2 a -> T1 a
g :: T2 a -> T1 a :: T2 a -> T1 a

我们可以证明f和g是互逆的(即g . f = id和f . g = id)：

f . g
(flip .) . flip . flip . (flip .)
(flip .) . (flip .) -- flip . flip = id
id -- (flip .) . (flip .) = \h -> \x -> flip (flip (h x)) = \h -> \x -> h x = id

g . f
flip . (flip .) . (flip .) . flip
flip . flip 
id

- duplode

---

:t [f . g, g . f] 报告了一个类型。 :) 我们可以从中得出结论，无论 f 和 g 本身是什么，它们都是 id 吗？ - Will Ness

@WillNess 很好的问题，但我认为这并不普遍适用。一个远离的反例是 [join . return, return . join]。回到当前情况，一个快捷方式是指出f和g的最一般类型是(a -> b -> c -> d) -> c -> b -> a -> d，而参数性确保只能实现为\x c b a -> x a b c，它是自己的反转。 (只有在最一般的类型中才有效，例如f :: T1 -> T2，我们可以潜入一些东西--例如\x c b a -> x (a . a) b c)。 - duplode

Answer 3

我同意你的评估。三种类型都是不同的，你已经正确地简化了它们。如果你认为所提供的答案与你的观点不符，你确定你正在正确地阅读问题和答案吗？

- amalloy