Неожиданное выражение Хаскелла

Я хотел бы понять, почему следующее выражение является допустимым в Haskell:

Prelude> let e = (+) (-)
Prelude> :type e
e :: (Num (a -> a -> a), Num a) => (a -> a -> a) -> a -> a -> a

Более странно, что любое выражение в форме

e 1 2 3 4 ... N

все N - все допустимые выражения непонятного типа. Например,

Prelude> :t e 1 2 3 4 5
e 1 2 3 4 5
  :: (Num ((a -> a1 -> t) -> (a -> a1 -> t) -> a -> a1 -> t),
      Num (a -> a1 -> t), Num a1, Num a) =>
     t

Является ли это неудачным следствием каррирования и вывода типа?

Разъяснения приветствуются.

Ответ 1

Это не "неудачное последствие". На самом деле, некоторые могут видеть это как функцию! Типы (+) и (-) являются

> :t (+)
(+) :: Num a => a -> a -> a
> :t (-)
(-) :: Num a => a -> a -> a

Важно понимать, что это допустимо для любого типа a, даже если a является типом функции. Например, если тип b -> b -> b имеет экземпляр Num, вы можете ограничить (+) на

(+) :: Num (b -> b -> b) => (b -> b -> b) -> (b -> b -> b) -> b -> b -> b

просто установив a = b -> b -> b. Из-за currying круглые скобки вокруг трех последних b не нужны (вы могли бы написать их, но они были бы лишними).

Теперь Num b => b -> b -> b является именно типом (-) (при условии, что b сам должен иметь экземпляр Num), поэтому функция (-) заполняет первый "слот" (+) и тип (+) (-) равен

(+) (-) :: (Num b, Num (b -> b -> b)) -> (b -> b -> b) -> b -> b -> b

что вы наблюдали.

Это ставит вопрос о том, почему, возможно, было бы полезно иметь экземпляр Num для функций вообще. На самом деле, имеет ли смысл определять экземпляр Num для функций?

Я утверждаю, что это так! Вы можете определить

instance Num a => Num (r -> a) where
    (f + g) r = f r + g r
    (f - g) r = f r - g r
    (f * g) r = f r * g r
    abs f r = abs (f r)
    signum f r  = signum (f r) 
    fromInteger n r = fromInteger n

который имеет прекрасный смысл как экземпляр Num. И на самом деле, это именно тот экземпляр, который вам нужно интерпретировать как выражение e -

> let e = (+) (-)
> e 3 2 1
4

Буг?!?

Случилось следующее. Поскольку (Num a) => r -> a является допустимым экземпляром Num для любого r, вы можете заменить r на a -> a, что показывает, что (Num a) => a -> a -> a также является допустимым экземпляром Num. Таким образом, у вас есть

-- Remember that (+) f = \g r -> f r + g r

  (+) (-) 3 2 1
= (\g r s -> (-) r s + g r s) 3 2 1 -- definition of (+) on functions
= (\  r s -> (-) r s + 3 r s) 2 1   -- beta reduction
= (\    s -> (-) 2 s + 3 2 s) 1     -- beta reduction
=            (-) 2 1 + 3 2 1        -- beta reduction
=            (2 - 1) + 3            -- since (3 2) = 3 and (3 1) = 3
=               1    + 3
=               4

Немного запутанный (в частности, убедитесь, что вы понимаете, почему 3 2 = 3), но не слишком сбивает с толку, как только вы расширили все определения!

Вы попросили вывести тип (+) (-), который использует Haskell. Он опирается на идею "унификации" переменных типа. Это происходит примерно так:

Вы знаете, что (+) :: Num a => a -> a -> a и (-) :: Num b => b -> b -> b (я использую разные буквы, потому что мы захотим их смять).
Если вы поместите (-) в первый слот (+), вы должны иметь a ~ b -> b -> b, поэтому комбинированный тип
(+) (-) :: (Num a, Num b, a ~ b -> b -> b) => (b -> b -> b) -> (b -> b -> b)
Теперь вы "объединяете" a с b -> b -> b (как указано слева от стрелки жира, знаком ~), который оставляет вас с
(+) (-) :: (Num (b -> b -> b), Num b) => (b -> b -> b) -> (b -> b -> b)
Если мы удалим правые скобки (потому что они избыточны) и переименуем b в a, это сигнатура типа, которую указывает Haskell.