Каковы точки строгости Haskell?

90

Все мы знаем (или должны знать), что Haskell по умолчанию ленив. Ничего не оценивается до тех пор, пока не будет оценено. Итак, когда нужно что-то оценивать? Есть моменты, в которых Haskell должен быть строгим. Я называю это «точками строгости», хотя этот конкретный термин не так широко распространен, как я думал. По мне:

Редукция (или оценка) в Haskell происходит только в точках строгости.

Возникает вопрос: в чем конкретно заключаются точки строгости Haskell? Моя интуиция говорит , что main, seq/ челка модель, сопоставление с образцом, и любое IOдействие , совершаемое с помощью mainявляются первичными точками Строгости, но я не знаю , почему я это знаю.

(Кроме того , если они не называются «точка строгости», что есть они называются?)

Думаю, хороший ответ будет включать обсуждение WHNF и так далее. Я также предполагаю, что это может коснуться лямбда-исчисления.


Изменить: дополнительные мысли по этому вопросу.

Размышляя над этим вопросом, я думаю, было бы яснее добавить что-нибудь к определению точки строгости. Пункты строгости могут иметь различный контекст и различную глубину (или строгость). Возвращаясь к моему определению, что «сокращение в Haskell происходит только в точках строгости», давайте добавим к этому определению следующее предложение: «точка строгости срабатывает только тогда, когда оценивается или уменьшается окружающий его контекст».

Итак, позвольте мне попытаться начать с того ответа, который я хочу. mainэто пункт строгости. Это специально обозначено как первичная точка строгости своего контекста: программа. Когда программа ( mainконтекст) оценивается, точка строгости main активируется. Глубина Main максимальна: ее нужно полностью оценить. Main обычно состоит из действий ввода-вывода, которые также являются точками строгости, контекст которых есть main.

Теперь вы попробуете: обсудить seqи сопоставить с образцом в этих терминах. Разъясните нюансы применения функции: насколько строго? Как это не так? О чем deepseq? letа caseзаявления? unsafePerformIO? Debug.Trace? Определения верхнего уровня? Строгие типы данных? Узоры взрыва? И т. Д. Сколько из этих элементов можно описать в терминах простой последовательности или сопоставления с образцом?

Дэн Бертон
источник
10
Ваш интуитивно понятный список, вероятно, не очень ортогонален. Я подозреваю, что seqи сопоставления с образцом достаточно, а все остальное определяется в их терминах. Я думаю, что сопоставление с образцом, например, обеспечивает жесткость IOдействий.
CA McCann,
Примитивы, такие как +встроенные числовые типы, также требуют строгости, и я предполагаю, что то же самое применимо к чистым вызовам FFI.
hammar
4
Кажется, здесь путают два понятия. Сопоставление с образцом и шаблоны seq и bang - это способы, с помощью которых выражение может стать строгим в своих подвыражениях, то есть, если вычисляется верхнее выражение, то же самое и подвыражение. С другой стороны, основные действия ввода-вывода - это то, как начинается оценка . Это разные вещи, и включение их в один список является своего рода ошибкой типа.
Крис Смит,
@ChrisSmith Я не пытаюсь путать эти два разных случая; во всяком случае, я прошу пояснить, как они взаимодействуют. Строгость каким-то образом случается, и оба случая являются важными, хотя и разными, частями «происходящего» строгости. (и @ monadic: ಠ_ಠ)
Дэн Бертон
Если вы хотите / вам нужно место для обсуждения аспектов этого вопроса, не пытаясь дать полный ответ, позвольте мне предложить использовать комментарии к моему сообщению / r / haskell для этого вопроса
Дэн Бертон

Ответы:

46

Хорошее место для начала - понимание этой статьи: Естественная семантика ленивого вычисления (Лаанчбери). Это подскажет вам, когда выражения оцениваются для небольшого языка, подобного GHC Core. Затем остается вопрос, как полностью отобразить Haskell на Core, и большая часть этого перевода дается самим отчетом Haskell. В GHC мы называем этот процесс «обессахариванием», потому что он удаляет синтаксический сахар.

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

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

Саймон Марлоу
источник
18
Мне всегда казалось забавным, что в том, что GHC называет «десугарингом», удаляемый синтаксический сахар включает в себя фактический синтаксис самого языка Haskell ... что, как может показаться, означает, что GHC на самом деле является оптимизирующим компилятором для GHC. Базовый язык, который, кстати, также включает очень сложный интерфейс для перевода Haskell в Core. :]
CA McCann
Однако системы типов не работают точно ... особенно, но не только в отношении перевода классов типов в явные словари, насколько я помню. И все последние разработки TF / GADT, насколько я понимаю, увеличили этот разрыв.
sclv
1
GCC также не оптимизирует C: gcc.gnu.org/onlinedocs/gccint/Passes.html#Passes
Дьердь Андрасек,
20

Я бы, вероятно, переформулировал этот вопрос так: при каких обстоятельствах Haskell будет оценивать выражение? (Возможно, закрепите «нормальную форму для слабой головы».)

В первом приближении это можно уточнить следующим образом:

  • Выполнение действий ввода-вывода будет оценивать любые выражения, которые им «нужны». (Таким образом, вам нужно знать, выполняется ли действие ввода-вывода, например, его имя - main, или оно вызывается из основного, и вам нужно знать, что требуется для действия.)
  • Выражение, которое оценивается (эй, это рекурсивное определение!), Будет оценивать любые выражения, которые ему нужны.

Из вашего интуитивно понятного списка основные действия и действия ввода-вывода попадают в первую категорию, а последовательность операций и сопоставление с образцом - во вторую категорию. Но я думаю, что первая категория больше соответствует вашей идее о «точке строгости», потому что именно так мы заставляем оценку в Haskell стать наблюдаемым эффектом для пользователей.

Предоставление всех деталей в частности - большая задача, поскольку Haskell - это большой язык. Это также довольно тонко, потому что Concurrent Haskell может оценивать вещи умозрительно, даже если мы в конечном итоге не используем результат: это третья разновидность вещей, вызывающих оценку. Вторая категория достаточно хорошо изучена: вы хотите посмотреть на строгость задействованных функций. Первая категория тоже можно рассматривать как своего рода «строгость», хотя это немного хитроумный , потому что evaluate xи seq x $ return ()на самом деле это разные вещи! Вы можете относиться к этому должным образом, если дадите какую-то семантику монаде ввода-вывода (явная передача RealWorld#токена работает для простых случаев), но я не знаю, есть ли вообще название для такого рода стратифицированного анализа строгости.

Эдвард З. Янг
источник
17

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

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

Программисты также могут использовать seqпримитив, чтобы заставить выражение вычисляться независимо от того, будет ли когда-либо использоваться результат.

$!определяется в терминах seq.

- Ленивый против нестрогого .

Итак, вы думаете о !/ $!и seqпо сути правильно, но сопоставление с образцом подчиняется более тонким правилам. ~Конечно, вы всегда можете использовать ленивое сопоставление с образцом. Интересный момент из той же статьи:

Анализатор строгости также ищет случаи, когда подвыражения всегда требуются для внешнего выражения, и преобразует их в активное вычисление. Он может это сделать, потому что семантика (с точки зрения «дна») не меняется.

Давайте продолжим изучение кроличьей норы и посмотрим на документацию по оптимизации, выполненную GHC:

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

- Оптимизация GHC: анализ строгости .

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

… Больше невозможно выполнить оценку значения; говорят, что он находится в нормальной форме . Если мы находимся на каком-либо из промежуточных этапов, так что мы выполнили хотя бы некоторую оценку значения, оно находится в нормальной форме слабого заголовка (WHNF). (Существует также «нормальная форма головы», но она не используется в Haskell.) Полная оценка чего-либо в WHNF сводит это к чему-то в нормальной форме ...

- Викиучебник Haskell: лень

(Термин находится в нормальной форме заголовка, если в позиции заголовка 1 нет бета-редекса . Редекс - это редекс заголовка, если ему предшествуют только лямбда-абстракторы нередексов 2. ) Итак, когда вы начинаете форсировать преобразователь, вы работаете в WHNF; когда больше не нужно форсировать thunks, вы в нормальной форме. Еще один интересный момент:

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

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

Однако CA McCann правильно понял это в комментариях: единственное, что особенного в mainэтом, main- это то, что определено как особенное; сопоставления с образцом в конструкторе достаточно для обеспечения последовательности, налагаемой IOмонадой. Только в этом отношении seqи сопоставление с образцом являются фундаментальными.

Джон Парди
источник
4
На самом деле цитата «если бы в какой-то момент нам нужно было, скажем, распечатать z для пользователя, нам нужно было бы полностью оценить это» не совсем верна. Он такой же строгий, как и Showэкземпляр печатаемого значения.
nominolo
10

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

Хороший источник модели «лени» haskell можно найти здесь: http://en.wikibooks.org/wiki/Haskell/Laziness.

По сути, важно понимать разницу между преобразователем и нормальной формой слабого заголовка WHNF.

Насколько я понимаю, haskell выполняет вычисления в обратном порядке по сравнению с императивными языками. Это означает, что при отсутствии шаблонов "seq" и bang это, в конечном счете, будет побочным эффектом, который вынуждает оценивать преобразователь, что, в свою очередь, может вызвать предварительные оценки (истинная лень).

Поскольку это привело бы к ужасной утечке места, компилятор заранее выясняет, как и когда оценивать преобразователи, чтобы сэкономить место. Затем программист может поддержать этот процесс, предоставив аннотации строгости (en.wikibooks.org/wiki/Haskell/Strictness, www.haskell.org/haskellwiki/Performance/Strictness) для дальнейшего уменьшения использования пространства в виде вложенных преобразователей.

Я не разбираюсь в операционной семантике haskell, поэтому оставлю ссылку в качестве ресурса.

Еще несколько ресурсов:

http://www.haskell.org/haskellwiki/Performance/Laziness

http://www.haskell.org/haskellwiki/Haskell/Lazy_Evaluation

жидкий
источник
6

Ленивый не означает ничего не делать. Каждый раз, когда ваш программный шаблон соответствует caseвыражению, он что-то оценивает - в любом случае достаточно. В противном случае он не сможет определить, какой RHS использовать. Не видите в коде никаких case-выражений? Не волнуйтесь, компилятор переводит ваш код в урезанную форму Haskell, где их трудно избежать.

Основное практическое правило для новичков let- лениться, caseменьше лениться.

T_S_
источник
2
Обратите внимание, что, хотя caseвсегда принудительно выполняет оценку в GHC Core, в обычном Haskell этого не происходит. Например, попробуйте case undefined of _ -> 42.
hammar
2
caseв GHC Core оценивает свой аргумент для WHNF, в то время как caseв Haskell оценивает свой аргумент столько, сколько необходимо для выбора соответствующей ветви. В примере с hammar это совсем не так, но in case 1:undefined of x:y:z -> 42оценивает глубже, чем WHNF.
Макс
А также case something of (y,x) -> (x,y)вообще не нужно оценивать something. Это верно для всех типов продуктов.
Инго
@Ingo - это неправильно. somethingдолжен быть оценен как WHNF, чтобы достичь конструктора кортежа.
John L
Джон - Почему? Мы знаем, что это должен быть кортеж, так где же смысл его оценивать? Достаточно, если x и y связаны с кодом, который оценивает кортеж и извлекает соответствующий слот, если они сами когда-либо понадобятся.
Инго
4

Это не полный ответ, направленный на карму, а всего лишь часть головоломки - поскольку речь идет о семантике, имейте в виду, что существует несколько стратегий оценки, которые обеспечивают одинаковую семантику. Одним из хороших примеров здесь - и этот проект также говорит о том, как мы обычно думаем о семантике Haskell, - был проект Eager Haskell, который радикально изменил стратегии оценки при сохранении той же семантики: http://csg.csail.mit.edu/ pubs / haskell.html

sclv
источник
2

Компилятор Glasgow Haskell переводит ваш код на язык, похожий на лямбда-исчисление, который называется core . В этом языке что-то будет оцениваться всякий раз, когда вы сопоставляете его с шаблоном с помощью caseоператора. Таким образом, если функция вызывается, будет оцениваться самый внешний конструктор и только он (если нет принудительных полей). Все остальное консервируется в преобразователе. (Преобразователи вводятся letпривязками).

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

Если вы попытаетесь оценить функцию вручную, вы можете подумать:

  • Попробуйте оценить самый внешний конструктор возврата.
  • Если что-то еще необходимо для получения результата (но только если это действительно необходимо), также будет оценено. Порядок не имеет значения.
  • В случае ввода-вывода вы должны оценить результаты всех операторов от первого до последнего. Это немного сложнее, поскольку монада ввода-вывода выполняет некоторые трюки, чтобы принудительно выполнять вычисления в определенном порядке.
фуз
источник
0

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

Нет.

Haskell - не ленивый язык

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

Не совсем верно, что порядок оценки не имеет значения, потому что язык допускает бесконечные циклы. Если вы не будете осторожны, можно застрять в тупике, где вы навсегда оцениваете подвыражение, когда другой порядок оценки привел бы к завершению за конечное время. Так что точнее сказать:

  • Реализации Haskell должны оценивать программу таким образом, чтобы она завершалась, если есть какой-либо порядок оценки, который завершается. Только в том случае, если каждый возможный порядок оценки не завершается, реализация может не завершиться.

Это по-прежнему оставляет реализациям огромную свободу в оценке программы.

Программа Haskell - это одно выражение, а именно let {все привязки верхнего уровня.} in Main.main . Оценка может пониматься как последовательность сокращающих (небольших) шагов, которые изменяют выражение (которое представляет текущее состояние выполняющейся программы).

Вы можете разделить шаги редукции на две категории: те, которые доказуемо необходимы (доказуемо будут частью любой завершающей последовательности сокращений), и те, которые нет. Вы можете расплывчато разделить доказуемо необходимые сокращения на две подкатегории: те, которые «очевидно» необходимы, и те, которые требуют некоторого нетривиального анализа, чтобы доказать их необходимость.

Выполнение только явно необходимых сокращений - это то, что называется «ленивым вычислением». Я не знаю, существовала ли когда-либо реализация Haskell с чисто ленивыми оценками. Объятия, возможно, были одним из них. GHC определенно нет.

GHC выполняет шаги сокращения во время компиляции, которые не являются доказуемо необходимыми; например, он заменит 1+2::Intна, 3::Intдаже если не может доказать, что результат будет использован.

В некоторых случаях GHC может также выполнять необязательные сокращения во время выполнения. Например, при генерации кода для оценки f (x+y), если xи yимеют тип Intи их значения будут известны во время выполнения, но fне может быть доказано использование его аргумента, нет причин не вычислять x+yперед вызовом f. Он использует меньше места в куче и меньше места для кода и, вероятно, работает быстрее, даже если аргумент не используется. Однако я не знаю, действительно ли GHC использует такие возможности оптимизации.

GHC определенно выполняет этапы оценки во время выполнения, что доказано только в результате довольно сложного кросс-модульного анализа. Это чрезвычайно распространено и может составлять основную часть оценки реалистичных программ. Ленивая оценка - это последняя резервная стратегия оценки; это не то, что обычно бывает.

Была ветвь «оптимистической оценки» GHC, которая давала гораздо больше умозрительных оценок во время выполнения. От него отказались из-за его сложности и постоянного обслуживания, а не из-за того, что он плохо работал. Если бы Haskell был таким же популярным, как Python или C ++, я уверен, что были бы реализации с гораздо более сложными стратегиями оценки времени выполнения, поддерживаемыми крупными корпорациями. Неленивая оценка - это не изменение языка, это просто инженерная задача.

Снижение происходит за счет ввода-вывода верхнего уровня, и ничего больше

Вы можете моделировать взаимодействие с внешним миром с помощью специальных правил сокращения с побочными эффектами, например: «Если текущая программа имеет форму getChar >>= <expr>, тогда получите символ из стандартного ввода и уменьшите программу, чтобы <expr>применить к полученному вами персонажу».

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

Других правил о том, что и когда сокращать, нет. Есть только правила того, что к чему может сводиться.

Например, единственные правила для ifвыражений - это то, что if True then <expr1> else <expr2>может быть уменьшено до <expr1>, if False then <expr1> else <expr2>может быть уменьшено до <expr2>, и if <exc> then <expr1> else <expr2>, где <exc>является исключительным значением, может быть уменьшено до исключительного значения.

Если выражение, представляющее текущее состояние вашей программы, является ifвыражением, у вас нет другого выбора, кроме как выполнять сокращения для условия до тех пор, пока оно не станет Trueили Falseили <exc>, потому что это единственный способ избавиться от ifвыражения и иметь любую надежду достичь состояние, соответствующее одному из правил ввода-вывода. Но спецификация языка не говорит вам об этом во многих словах.

Такого рода неявные ограничения порядка - единственный способ «принудительного» выполнения оценки. Это частый источник путаницы для новичков. Например, люди иногда пытаются стать foldlстроже, foldl (\x y -> x `seq` x+y)вместо того чтобы писать foldl (+). Это не работает, и ничего подобного никогда не сработает, потому что никакое выражение не может вычислить само себя. Оценка может быть только «сверху». seqв этом плане нет ничего особенного.

Снижение происходит везде

Редукция (или оценка) в Haskell происходит только в точках строгости. [...] Моя интуиция подсказывает, что главные элементы, шаблоны seq / bang, сопоставление с образцом и любое действие ввода-вывода, выполняемое через main, являются основными пунктами строгости [...].

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

Для уменьшения функции приложения <expr1> <expr2>, вы должны оценить , <expr1>пока он не имеет формы , как (\x -> <expr1'>)и (getChar >>=)или что - то другое , что соответствует правилу. Но по какой-то причине приложение функции не появляется в списках выражений, которые якобы "вынуждают вычислять", хотя это caseвсегда происходит.

Вы можете увидеть это заблуждение в цитате из вики-страницы Haskell, найденной в другом ответе:

На практике Haskell - не просто ленивый язык: например, сопоставление с образцом обычно строгое

Я не понимаю, что можно квалифицировать как «чисто ленивый язык» для того, кто это написал, кроме, возможно, языка, на котором каждая программа зависает, потому что среда выполнения ничего не делает. Если сопоставление с образцом является особенностью вашего языка, тогда вам действительно нужно это сделать в какой-то момент. Для этого вы должны достаточно оценить проверяемого, чтобы определить, соответствует ли он шаблону. Это самый ленивый способ сопоставить шаблон, который в принципе возможен.

~-префиксные шаблоны программисты часто называют «ленивыми», но в спецификации языка они называются «неопровержимыми». Их определяющее свойство - они всегда совпадают. Поскольку они всегда совпадают, вам не нужно оценивать проверяемого, чтобы определить, совпадают они или нет, поэтому ленивая реализация не будет. Разница между обычными и неопровержимыми шаблонами заключается в том, какие выражения они соответствуют, а не в том, какую стратегию оценки вы должны использовать. В спецификации ничего не говорится о стратегиях оценки.


mainэто пункт строгости. Это специально обозначено как первичная точка строгости своего контекста: программа. Когда программа ( mainконтекст) оценивается, точка строгости main активируется. [...] Main обычно состоит из действий ввода-вывода, которые также являются точками строгости, контекст которых есть main.

Я не уверен, что все это имеет какое-то значение.

Глубина Main максимальна: ее нужно полностью оценить.

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

обсудить seqи сопоставление с образцом в этих условиях

Я уже говорил о сопоставлении с образцом. seqмогут быть определены правилами, аналогичными caseи application: например, (\x -> <expr1>) `seq` <expr2>сокращается до <expr2>. Это «принудительно оценивает» так же, как caseи приложение. WHNF - это просто название того, к чему эти выражения «принудительно вычисляют».

Разъясните нюансы применения функции: насколько строго? Как это не так?

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

О чем deepseq?

Это просто библиотечная функция, а не встроенная функция.

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

letа caseзаявления?

Я говорил о case. letпосле удаления сахара и проверки типа - это просто способ записи графа произвольного выражения в виде дерева. Вот статья об этом .

unsafePerformIO?

В некоторой степени это может быть определено правилами редукции. Например, case unsafePerformIO <expr> of <alts>сокращается до unsafePerformIO (<expr> >>= \x -> return (case x of <alts>))и только на верхнем уровне unsafePerformIO <expr>сокращается до <expr>.

Это не делает мемоизации. Вы можете попытаться имитировать мемоизацию, переписав каждое unsafePerformIOвыражение так, чтобы оно явным образом запомнилось, и создав IORefгде-нибудь связанный s ... Но вы никогда не сможете воспроизвести поведение мемоизации GHC, потому что оно зависит от непредсказуемых деталей процесса оптимизации и потому, что оно даже небезопасно по типу (как показывает печально известный полиморфный IORefпример в документации GHC).

Debug.Trace?

Debug.Trace.trace просто обертка вокруг unsafePerformIO .

Определения верхнего уровня?

Привязки переменных верхнего уровня аналогичны вложенным letпривязкам. data, class,import , И такие совершенно разные игры с мячом.

Строгие типы данных? Узоры взрыва?

Просто сахар для seq.

Benrg
источник