Что делает два типа выражений в 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

Answer 2

Три типа ...

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

Answer 3

Я согласен с вашей оценкой. Все три типа разные, и вы правильно их упростили. Вы уверены, что правильно прочитали вопрос и ответ, если считаете, что предоставленный ответ не соответствует вашему?