Haskell: Что такое нормальная форма слабой головы?

Question

Что означает Нормальная Форма Слабой Головы (WHNF)? Что означает нормальная форма головы (HNF) и нормальная форма (NF)?

Реальный мир Haskell утверждает:

Знакомая функция seq вычисляет выражение к тому, что мы называем нормальной формой головы (сокращенно HNF). Он останавливается, как только достигает самого внешнего конструктора ("головы"). Это отличается от нормальной формы (NF), в которой выражение полностью оценивается.

Вы также услышите, что программисты на Haskell ссылаются на нормальную форму слабой головы (WHNF). Для нормальных данных слабая нормальная форма головы такая же, как нормальная форма головы. Разница возникает только для функций, и она слишком сложна, чтобы беспокоить нас здесь.

Я прочитал несколько ресурсов и определений ( Haskell Wiki и Haskell Mail List и Free Dictionary), но я не понимаю. Может ли кто-нибудь привести пример или дать определение непрофессионала?

Я предполагаю, что это будет похоже на:

WHNF = thunk : thunk

HNF = 0 : thunk 

NF = 0 : 1 : 2 : 3 : []

Как seq а также ($!) относятся к WHNF и HNF?

Обновить

Я все еще в замешательстве. Я знаю, что некоторые ответы говорят, чтобы игнорировать HNF. Из прочтения различных определений кажется, что нет никакой разницы между обычными данными в WHNF и HNF. Тем не менее, кажется, что есть разница, когда дело доходит до функции. Если не было никакой разницы, почему seq необходимо для foldl'?

Еще один момент путаницы из Хаскель Вики, которая утверждает, что seq сводится к WHNF и ничего не будет делать в следующем примере. Тогда они говорят, что они должны использовать seq форсировать оценку. Разве это не принуждает его к HNF?

Общий код переполнения стека новичков:

myAverage = uncurry (/) . foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0)

Люди, которые понимают seq и нормальную форму слабой головы (whnf), могут сразу понять, что здесь не так. (acc+x, len+1) уже находится в whnf, поэтому seq, который уменьшает значение до whnf, ничего не делает для этого. Этот код будет создавать thunks точно так же, как и оригинальный пример foldl, они просто будут внутри кортежа. Решение состоит в том, чтобы просто заставить компоненты кортежа, например,

myAverage = uncurry (/) . foldl' 
          (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

- Haskell Wiki на Stackru

Answer 1

Я постараюсь дать объяснение простыми словами. Как уже отмечали другие, нормальная форма головы не относится к Хаскеллу, поэтому я не буду ее здесь рассматривать.

Нормальная форма

Выражение в нормальной форме полностью вычисляется, и никакое подвыражение не может быть оценено далее (то есть оно не содержит необработанных блоков).

Все эти выражения в нормальной форме:

42
(2, "hello")
\x -> (x + 1)

Эти выражения не в нормальной форме:

1 + 2                 -- we could evaluate this to 3
(\x -> x + 1) 2       -- we could apply the function
"he" ++ "llo"         -- we could apply the (++)
(1 + 1, 2 + 2)        -- we could evaluate 1 + 1 and 2 + 2

Слабая голова нормальной формы

Выражение в нормальной форме со слабой головой было оценено как самый внешний конструктор данных или лямбда-абстракция (голова). Подвыражения могут или не могут быть оценены. Следовательно, каждое выражение нормальной формы также находится в нормальной форме со слабой головой, хотя в общем случае обратное не имеет места.

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

Эти выражения в слабой голове нормальной формы:

(1 + 1, 2 + 2)       -- the outermost part is the data constructor (,)
\x -> 2 + 2          -- the outermost part is a lambda abstraction
'h' : ("e" ++ "llo") -- the outermost part is the data constructor (:)

Как уже упоминалось, все перечисленные выше выражения в нормальной форме также находятся в нормальной форме со слабой головой.

Эти выражения не в слабой голове нормальной форме:

1 + 2                -- the outermost part here is an application of (+)
(\x -> x + 1) 2      -- the outermost part is an application of (\x -> x + 1)
"he" ++ "llo"        -- the outermost part is an application of (++)

Переполнение стека

При оценке выражения в нормальной форме со слабой головой может потребоваться, чтобы другие выражения сначала оценивались в WHNF. Например, чтобы оценить 1 + (2 + 3) для WHNF, мы должны сначала оценить 2 + 3, Если оценка одного выражения приводит к слишком многим из этих вложенных вычислений, результатом является переполнение стека.

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

foldl (+) 0 [1, 2, 3, 4, 5, 6]
 = foldl (+) (0 + 1) [2, 3, 4, 5, 6]
 = foldl (+) ((0 + 1) + 2) [3, 4, 5, 6]
 = foldl (+) (((0 + 1) + 2) + 3) [4, 5, 6]
 = foldl (+) ((((0 + 1) + 2) + 3) + 4) [5, 6]
 = foldl (+) (((((0 + 1) + 2) + 3) + 4) + 5) [6]
 = foldl (+) ((((((0 + 1) + 2) + 3) + 4) + 5) + 6) []
 = (((((0 + 1) + 2) + 3) + 4) + 5) + 6
 = ((((1 + 2) + 3) + 4) + 5) + 6
 = (((3 + 3) + 4) + 5) + 6
 = ((6 + 4) + 5) + 6
 = (10 + 5) + 6
 = 15 + 6
 = 21

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

Вы можете задаться вопросом, почему Haskell не уменьшает внутренние выражения раньше времени? Это из-за лени Хаскелла. Поскольку в общем случае нельзя предполагать, что каждое подвыражение будет необходимо, выражения оцениваются извне в.

(GHC имеет анализатор строгости, который обнаруживает некоторые ситуации, когда подвыражение всегда необходимо, и он может оценить его заранее. Однако это всего лишь оптимизация, и вы не должны полагаться на него, чтобы спасти вас от переполнений).

Такое выражение, с другой стороны, абсолютно безопасно:

data List a = Cons a (List a) | Nil
foldr Cons Nil [1, 2, 3, 4, 5, 6]
 = Cons 1 (foldr Cons Nil [2, 3, 4, 5, 6])  -- Cons is a constructor, stop. 

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

seq

seq это специальная функция, которая используется для принудительного вычисления выражений. Его семантика такова, что seq x y означает, что всякий раз, когда y оценивается как слабая голова нормальной формы, x также оценивается как слабая голова нормальной формы.

Это среди других мест, используемых в определении foldl'Строгий вариант foldl,

foldl' f a []     = a
foldl' f a (x:xs) = let a' = f a x in a' `seq` foldl' f a' xs

Каждая итерация foldl' заставляет аккумулятор к WHNF. Поэтому он избегает создания большого выражения и, следовательно, избегает переполнения стека.

foldl' (+) 0 [1, 2, 3, 4, 5, 6]
 = foldl' (+) 1 [2, 3, 4, 5, 6]
 = foldl' (+) 3 [3, 4, 5, 6]
 = foldl' (+) 6 [4, 5, 6]
 = foldl' (+) 10 [5, 6]
 = foldl' (+) 15 [6]
 = foldl' (+) 21 []
 = 21                           -- 21 is a data constructor, stop.

Но, как упоминается в примере на HaskellWiki, это не спасает вас во всех случаях, так как аккумулятор оценивается только в WHNF. В этом примере аккумулятор является кортежем, поэтому он будет принудительно вычислять конструктор кортежа, а не acc или же len,

f (acc, len) x = (acc + x, len + 1)

foldl' f (0, 0) [1, 2, 3]
 = foldl' f (0 + 1, 0 + 1) [2, 3]
 = foldl' f ((0 + 1) + 2, (0 + 1) + 1) [3]
 = foldl' f (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1) []
 = (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1)  -- tuple constructor, stop.

Чтобы избежать этого, мы должны сделать так, чтобы при оценке конструктора кортежей выполнялась оценка acc а также len, Мы делаем это с помощью seq,

f' (acc, len) x = let acc' = acc + x
                      len' = len + 1
                  in  acc' `seq` len' `seq` (acc', len')

foldl' f' (0, 0) [1, 2, 3]
 = foldl' f' (1, 1) [2, 3]
 = foldl' f' (3, 2) [3]
 = foldl' f' (6, 3) []
 = (6, 3)                    -- tuple constructor, stop.

Answer 2

В разделе " Нормальные формы Thunks и Weak Head" в описании лени на Haskell Wikibooks приводится очень хорошее описание WHNF вместе с этим полезным описанием:

Оценка значения (4, [1, 2]) пошаговая. Первый этап полностью неоценен; все последующие формы находятся в WHNF, и последняя также в нормальной форме.

Answer 3

Программы на Haskell являются выражениями и выполняются путем выполнения оценки.

Чтобы оценить выражение, замените все приложения функций их определениями. Порядок, в котором вы делаете это, не имеет большого значения, но он по-прежнему важен: начните с самого внешнего приложения и продолжайте слева направо; это называется ленивая оценка.

Пример:

   take 1 (1:2:3:[])
=> { apply take }
   1 : take (1-1) (2:3:[])
=> { apply (-)  }
   1 : take 0 (2:3:[])
=> { apply take }
   1 : []

Оценка останавливается, когда больше не осталось функциональных приложений для замены. Результат в нормальной форме (или уменьшенной нормальной форме, RNF). Независимо от того, в каком порядке вы оцениваете выражение, вы всегда будете иметь одну и ту же нормальную форму (но только если оценка завершится).

Есть немного другое описание для ленивой оценки. А именно, это говорит о том, что вы должны оценивать все, чтобы слабая голова только в нормальной форме Есть только три случая, когда выражение должно быть в WHNF:

• Конструктор: constructor expression_1 expression_2 ...
• Встроенная функция со слишком малым количеством аргументов, например (+) 2 или же sqrt
• Лямбда-выражение: \x -> expression

Другими словами, заголовок выражения (то есть самое внешнее приложение функции) не может быть вычислен дальше, но аргумент функции может содержать неоцененные выражения.

Примеры WHNF:

3 : take 2 [2,3,4]   -- outermost function is a constructor (:)
(3+1) : [4..]        -- ditto
\x -> 4+5            -- lambda expression

---

Заметки

1. "Заголовок" в WHNF относится не к заголовку списка, а к самому внешнему приложению функций.
2. Иногда люди называют недооцененные выражения "громкими", но я не думаю, что это хороший способ понять это.
3. Нормальная форма головы (HNF) не имеет значения для Haskell. Он отличается от WHNF тем, что тела лямбда-выражений также оцениваются в некоторой степени.

Answer 4

Хорошее объяснение с примерами дано по адресу http://foldoc.org/Weak+Head+Normal+Form Нормальная форма головы упрощает даже биты выражения внутри абстракции функции, в то время как нормальная форма "слабой" головы останавливается на абстракциях функции.,

Из источника, если у вас есть:

\ x -> ((\ y -> y+x) 2)

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

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

Answer 5

WHNF не хочет, чтобы тело лямбда оценивалось, поэтому

WHNF = \a -> thunk
HNF = \a -> a + c

seq хочет, чтобы его первый аргумент был в WHNF, поэтому

let a = \b c d e -> (\f -> b + c + d + e + f) b
    b = a 2
in seq b (b 5)

оценивает

\d e -> (\f -> 2 + 5 + d + e + f) 2

вместо того, что бы использовать HNF

\d e -> 2 + 5 + d + e + 2

Answer 6

В общем, предположим, что у вас есть какой-то стук, t,

Теперь, если мы хотим оценить t к WHNF или NHF, которые одинаковы, за исключением функций, мы обнаружили бы, что мы получаем что-то вроде

t1 : t2 где t1 а также t2 громкие В этом случае, t1 будет вашим 0 (или, скорее, спасибо 0 без дополнительной распаковки)

seq а также $! оценивать WHNF. Обратите внимание, что

f $! x = seq x (f x)

Answer 7

Я понимаю, что это старый вопрос, но вот явное математическое определение WHNF, HNF и NF. В чистом лямбда-исчислении :

• Срок находится в НФ, если он имеет форму

  где - переменная, а находятся в НФ.

• Термин находится в HNF, если он имеет форму

  где - переменная, а - произвольные члены.

• Термин находится в WHNF, если он является лямбда-термином для любого термина или имеет форму

  где - переменная, а e1, e2, ..., em являются произвольными терминами.

---

Теперь рассмотрим язык программирования с конструкторами. a,b,c... артистичности na, nb, nc..., что означает, что всякий раз, когда они находятся в NF, термин a t1 t2 ... tm куда m = naявляется редексом и может быть оценен. Например, конструктор сложения + в Haskell есть арность 2, потому что он оценивается только тогда, когда ему передаются два аргумента в нормальной форме (в данном случае целые числа, которые сами по себе могут рассматриваться как конструкторы с нулевым значением).

• Срок находится в НФ, если он имеет форму

          λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
  

  где либо переменная, либо конструктор арности с m < n, и t1, t2, ..., tm находятся в НФ.

• Термин находится в HNF, если он имеет форму

          λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
  

  где либо переменная, либо конструктор арности, и являются произвольными терминами, если не все первые аргументы находятся в NF.

• Термин находится в WHNF, если он является лямбда-термином λ x. e на любой срок e или если он имеет форму

          x e1 e2 ... em
  

  куда x является либо переменной, либо конструктором арности, а e1, e2, ... emявляются произвольными терминами до тех пор, пока первые nаргументы не все в НФ.

---

В частности, любой член в NF находится в HNF, и любой член в HNF находится в WHNF, но не наоборот.

Answer 8

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

Это объясняется в главе 11 «Реализация языков функционального программирования » Саймона Пейтона Джонса.

Answer 9

Нормальная форма головы означает, что голова отсутствует.

(λx.((λy.y+x)2))2

Уменьшается до: R для редекса (и да, внутри него есть еще один редекс, но это не имеет значения). Это главный редекс, потому что это крайний левый редекс (единственный редекс), и перед ним нет лямбда-терминов (переменные или лямбда-выражения (приложения или абстракции)), только от 0 до n абстракторов (если R - это редекс). (λx.A)B абстрактором R является λx), в данном случае 0.

Поскольку существует редекс головы, его нет в HNF и, следовательно, также нет в NF, потому что есть редекс.

WHNF означает, что это лямбда-абстракция или в HNF. Вышеупомянутое не находится в HNF, и это не лямбда-абстракция, а приложение, и, следовательно, не в WHNF.

λx.((λy.y+x)2)2 находится в WHNF

Это лямбда-абстракция, но не в HNF, потому что есть голова λx.R2

Сократить до λx.((2+x)2). Редекса нет, поэтому он в нормальной форме.

Рассмотреть возможность λx.((λy.zyx)2), это упрощает λx.R, значит, его нет в HNF. λx.(k(λy.zyx)2) упрощает до λx.kR поэтому он находится в HNF, но не в NF.

Все NF находятся в HNF и WHNF. Все HNF - это WHNF.