Уравнение типа-подписи и функции в Haskell

Я новичок в Haskell и функциональном программировании. Я читаю через Real World Haskell, и я понял, что меня смущает несколько примеров.

В частности, это в главе 9, в разделе "Язык, специфичный для домена для предикатов", примеры, которые имеют параметры w x y z.

Я переварил это:

Почему этот код компилируется?

f :: Int -> (Int -> Int)
f x y = x+y

main = do
  let q = f 4 5
  putStr  (show (q))

В соответствии с сигнатурой типа f явно принимает 1 параметр и возвращает функцию. Однако, похоже, я могу написать уравнение функции, чтобы он принял два параметра и вернул int. Почему это возможно? Означает ли это, что подпись типа игнорируется?

Это карри? Это что-то вроде закрытия? Если я правильно понимаю этот http://www.haskell.org/haskellwiki/Currying, то он, кажется, несколько обращен к каррированию, как определено там, - моя функция f принимает несколько аргументов вместо одного!

Кроме того, может ли кто-либо ответить, укажите ссылку на какую-либо документацию Haskell, где указано это свойство (если возможно вообще).

EDIT:

Подумав об этом в течение некоторого времени, вы, кажется, подразумеваете следующее:

1) Этот синтаксис является синтаксическим сахаром, f всегда будет иметь один параметр, независимо от того, сколько параметров записано в уравнении

2) При применении функции f тело функции (всегда?) преобразуется в заглушку (фактически, возвращенную функцию), где x фиксируется с заданным параметром (4), а y является параметром.

3) Затем эта новая функция применяется к 5, которая заменяет y, а затем вычисляется функция +.

То, что меня действительно интересовало, заключалось в том, где именно он говорит что-то вроде "в уравнении функции, если вы пишете несколько параметров, это действительно синтаксический сахар, и на самом деле это происходит...", как я писал выше, Или это так очевидно для всех, кроме меня?

Изменить II:

Реальный ответ с открытием был в комментарии @luqui ниже, к сожалению, я не думаю, что могу отметить комментарий в качестве ответа.

Это тот факт, что f x y =... на самом деле является синтаксическим сахаром для: f =\x → \y → ...

И для меня все, что ниже сказано ниже, следует из этого.

Я нашел своего рода источник для этого в Gentle Introduction to Haskell, здесь: http://haskell.cs.yale.edu/tutorial/functions.html в разделе 3.1, называемом Lambda Abstractions,

Действительно, уравнения:

inc x = x + 1 добавьте x y = x + y

действительно сокращены для:

inc =\x → x + 1 add =\x y → x + y

В то время как в нем не используется фраза "синтаксический сахар", она использует более математическое ориентированное слово "стенография", но, как программист, я читаю это как "сахар": -)

Ответ 1

Это карри. Как говорит подпись типа, f принимает только один параметр. Это будет 4. Затем он возвращает функцию, которая немедленно применяется к 5. Фактически, эти две сигнатуры типа:

Int -> Int -> Int

Int -> (Int -> Int)

эквивалентны в Haskell.

РЕДАКТИРОВАТЬ: эта ссылка о Partial Application, которую я нашел внутри предоставленной вами страницы, объясняет это.

РЕДАКТИРОВАТЬ 2:. Вы спросили, где определено поведение харкеля. Я не знаю, если это то, что вы ищете: Haskell 98 Revised Report, в разделе 3.3. Закаленные приложения и абстракции лямбда, говорит:

Функциональное приложение написано e1 e2. Приложение связывает влево, поэтому круглые скобки могут быть опущены в (f x) y.

Ответ 2

Оператор -> является право-ассоциативным, т.е. t -> t -> t совпадает с t -> (t -> t).

Если вы переписываете

f x y = x+y

в эквивалентной форме

f x = \y -> x + y

эта связь должна стать очевидной.

Ответ 3

Это определенно немного карри. Хотя я не могу сразу найти, где в документации явно указывается это поведение, все, что нам нужно сделать, это немного проверить нашу математику о каррировании.

Как известно, функция с сигнатурой Int ->(Int -> Int) принимает Int и возвращает функцию, которая принимает Int и возвращает Int. И мы могли бы просто предоставить оба из Int, чтобы получить этот окончательный int, как в вашем примере:

f :: Int -> (Int -> Int)
f x y = x+y

И если мы предоставляем только первый аргумент, мы возвращаем функцию, которая нуждается в другом аргументе. Хлеб и масло карри.

Проще говоря, currying право-ассоциативный. Другими словами, Int -> (Int -> Int) совпадает с Int->Int->Int, мы добавили скобки, чтобы сделать более очевидным, что:

f 3

Не хватает аргумента, но на самом деле возвращает функцию типа Int->Int.

Это похоже на математику, когда вы изучаете ассоциативное свойство .

3 + 2 + 1 = (3 + 2) + 1 = 3 + (2 + 1)

Результат тот же, независимо от того, как мы помещаем наши круглые скобки.

Ответ 4

На самом деле это не синтаксис сахара, а просто как работает приложение функции в Haskell.

Рассмотрим:

f :: Int -> Int -> Int -> Int 
f x y z = x + y + z

g = f 4
h = g 4 5

f 4 4 5 -- 13
g 4 5   -- 13
g 6     -- 13

Вы можете играть с этим в ghci для подтверждения. g является частичным применением функции f - его тип g :: Int -> Int -> Int.

Вы также можете написать:

((f 4) 4) 5  -- 13

В этом случае (f 4) возвращает частично примененную функцию, которая принимает два дополнительных аргумента, ((f 4) 4) возвращает частично примененную функцию, которая принимает один аргумент, а целое выражение уменьшается до 13.

Ответ 5

Подумав еще об этом, я думаю, что полное объяснение должно быть чем-то вроде:

Функция Haskell может принимать только один аргумент и возвращать один параметр. Haskell позволяет нам притворяться, что передано несколько аргументов, но эта форма рассматривается как серия вложенных лямбда-функций.

f x y = x + y

рассматривается как

(1) f = \x -> \y -> x + y

Это лечение справедливо и для лямбда-функций \ x y → x + y рассматривается как \ x → \y → x + y

Это позволяет нам рассматривать объявление типа как лево-ассоциативное, то есть: f:: Int → Int → Int на самом деле f:: (Int → (Int → Int)) который точно соответствует (1): f не имеет аргументов, но возвращает функцию, которая принимает Int. Эта функция, в свою очередь, возвращает функцию, которая принимает другой Int, и возвращает Int.

Это означает, что если мы хотим вернуть функцию из функции, нам не нужно делать ничего особенного, поскольку этот режим по умолчанию Haskell.

Это также означает, что с учетом объявления типа f:: Int → Int → Int Мы можем написать f implementatin ( "уравнение" ) с 0, 1 или 2 параметрами. Если задан один или два параметра, компилятор будет генерировать необходимые лямбды для соответствия форме f:: (Int → (Int → Int))

f = \x -> \y -> x + y

f x = \y -> x + y  -- \x -> is generated

f x y = x + y -- \x -> \y is generated

Но в каждом из этих случаев приложение-функция, принимающее два параметра, будет скомпилировано успешно, так как оно всегда будет переведено в первую форму, например.

f 4 5 --> (\x -> (\y -> x + y) 5 ) 4

Если приложение внутренней функции вернет карри-форму (x + 5)

Это позволяет использовать приложение частичной функции, где мы можем дать только один параметр и вернуть частичную функцию.

Кроме того, изменение приоритета в типе функции:

f'' :: (Int -> Int) -> Int

изменяет значение - мы принимаем функцию, получающую Int и возвращающую ее как единственный параметр, и возвращаем Int.
Предположим, что мы где-то определили эту функцию, затем вызываем эту функцию с помощью параметров Integer, например

f'' 4 5

не будет компилироваться.

Edit:

Кроме того, даже если последние аргументы находятся в скобках или являются объявлением типа, это выполняется.

Например, последняя пара скобок не является обязательной, так как если бы они не были там, то компилятор мог бы поместить их в форму "lambda'd".

t4 :: (Int -> Int) -> (Int -> Int)
t4 f i = f i + i

Может применяться таким образом:

t4 (\x -> x*10) 5

Кроме того, данный:

type MyIntInt = Int -> Int

Тогда:

t5 :: MyIntInt -> MyIntInt

Является эквивалентным t4, но запутанным, так как значение MyIntInt отличается в обоих местах. Первый - тип первого параметра.
Второй "расширен" в Int → Int (вероятно, из-за правильной ассоциативности оператора), что означает, что t5 может принимать от 0 до 2 параметров в функциональном уравнении и приложении функции (хотя фактически всегда принимает 0 и возвращая встроенные lambdas, как я подробно описал выше).

например. мы можем написать t5 так же, как t4:

t5 f i = f i + i