Тип-сигнатура против функционального уравнения в Haskell

Question

Я новичок в 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 -> ...

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

Я нашел своего рода источник для этого в «Нежном введении в Хаскелл», здесь: http://haskell.cs.yale.edu/tutorial/functions.html в разделе 3.1, который называется Лямбда-абстракции.

На самом деле уравнения:

вкл. Х = х + 1 добавить х у = х + у

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

inc = \ x -> x + 1 add = \ x y -> x + y

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

Answer 1

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

Int -> Int -> Int

и

Int -> (Int -> Int)

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

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

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

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

Answer 2

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

Если переписать

f x y = x+y

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

f x = \y -> x + y

это мнение должно стать очевидным.

Answer 3

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

Функция 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 («уравнение») с 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 только один параметр и вернуть частичную функцию.

Также меняется приоритет в типе функции:

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

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

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 и возврат встроенных лямбд, как я подробно описал выше).

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

t5 f i = f i + i

Answer 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.

Answer 5

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

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

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

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

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

f 3

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

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

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

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