Верно ли мое понимание приводимого выражения, т. Е. Переопределения?
Программирование в Хаскеле Хаттоном говорит:
Выражение, имеющее форму функции, примененной к одному или нескольким аргументам, которые могут быть "сокращены" при выполнении приложения, называется приводимым выражением или, для краткости, redex.
Является приводимым выражением т.е.
приложение функции, где функция не является результатом другого приложения функции,
эквивалентно, приложение функции, где функция является либо именем функции, либо лямбда-выражением?
Является ли какой-либо из вышеперечисленных пунктов ответом на мой предыдущий вопрос о том, как внешняя стратегия оценки оценивает частичное применение функции и применение функции с карри?
2 ответа
То, что считается переопределением, обычно зависит от языка. Синтаксис выражений представлен парами форм введения и исключения различных конструкций; переопределение - это когда формы ввода и исключения определенного вида конструкции сопоставляются надлежащим образом.
Для функций лямбда-выражения представляют собой введение (они являются каноническим способом создания функции, когда ее еще не было), а приложения - исключения (они являются каноническим способом использования функции). Таким образом, функция redex - это применение лямбды к чему-либо, например к чему-либо (\x -> e1) e2, (И только это! Применение переменной к чему-либо не является функцией redex. Обычно я предполагаю, что это подразумевается, но ваш вопрос явно спрашивает об этом, так что...)
Для объявлений, let-привязки или аналогичные являются введениями (они являются каноническим способом объявить, что имя имеет заданное значение), а переменные являются исключениями (они являются каноническим способом использования объявленного значения). Таким образом, декларация redex является термином в рамках let обязательный, который ссылается на letпеременная, например что-то в форме let x = e1 in e2 где e2 упоминает x,
Для алгебраических типов данных конструкторы данных типа являются введением (они являются каноническим способом создания значения в типе) и case Выражения - это исключения (они являются каноническим способом использования значения алгебраического типа). Таким образом, переопределение алгебраического типа данных является case чья проверка является полностью насыщенным конструктором приложения, например case Constructor arg1 arg2 arg3 ... of pat1 -> e1; pat2 -> e2; ...,
Это всего лишь несколько примеров пар. Не все языки имеют все три из этих конструкций; и существуют языки с дополнительными конструкциями (например, изменяемые ссылки, исключения и т. п., каждый со своими формами введения и исключения). Но я думаю, что это должно дать вам представление о том, что подразумевается под "переопределением": это конструкция, в которой могут быть сделаны некоторые вычисления, чтобы продвинуться вперед в выяснении значения выражения.
Вы также спрашиваете ( в комментариях к связанной записи) "Разве mult(3) не является частичным приложением, так что имеет смысл?"
Я думал, что ответил на эту проблему в своем ответе на один из ваших предыдущих вопросов.
Нет, тип mult является (Int, Int) -> Int т.е. его аргумент должен иметь тип (Int, Int), Но 3 не может иметь этот тип; его тип просто Int, Для расчета результата mult 3 определение
mult :: (Int, Int) -> Int
mult (x, y) = x * y
консультируется, и расчет происходит следующим образом:
mult 3
= case 3 of (x, y) -> x * y
***error: pattern match failure
На самом деле, это было бы так, если бы Haskell был нетипизированным языком. Поскольку у него есть типы, несоответствие типов 3 а также (Int, Int) обнаружен во время компиляции, и программа отклонена. (*)
(*) 3 :: Num a => a т.е. его тип может быть Int , Float и т.д., но, конечно, это не может быть кортеж... ну, без Num экземпляр, определенный для кортежей, не может, но допустим, что его нет. Это также означает, что программа будет фактически отклонена во время выполнения после того, как обнаружится, что ни в одном из импортированных модулей не было определено ни одного экземпляра Num для каких-либо типов кортежей... но давайте оставим это в качестве сноски.