Какие правила существуют для функции a -> (), вычисляемой в Haskell?

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

f :: a -> ()
f _ = undefined

Оценка f 1выдает ошибку из-за наличия undefined, поэтому определенная оценка обязательно произойдет. Однако не ясно, насколько глубока оценка; иногда кажется, что все идет так глубоко, как необходимо для оценки всех обращений к функциям, которые возвращаются (). Пример:

g :: [a] -> ()
g [] = ()
g (_:xs) = g xs

Этот код зацикливается бесконечно, если представлен с g (let x = 1:x in x). Но потом

f :: a -> ()
f _ = undefined
h :: a -> ()
h _ = ()

может использоваться, чтобы показать, что h (f 1)возвращается (), поэтому в этом случае не все подвыражения с единичными значениями оцениваются. Какое общее правило здесь?

ЭТА: конечно, я знаю о лени. Я спрашиваю, что мешает авторам компиляторов сделать этот конкретный случай еще более ленивым, чем обычно возможно.

ETA2: краткое изложение примеров: GHC выглядит ()точно так же, как и любой другой тип, т. Е. Как если бы возник вопрос о том, какое регулярное значение, населяющее тип, должно быть возвращено из функции. Тот факт, что есть только одно такое значение, кажется, (ab) не используется алгоритмами оптимизации.

ETA3: когда я говорю «Haskell», я имею в виду «Haskell как определено отчетом», а не «Haskell-H-in-GHC». Кажется, это предположение не разделяется так широко, как я себе представлял (это было «на 100% читателей»), иначе я, вероятно, смог бы сформулировать более четкий вопрос. Тем не менее, я сожалею об изменении названия вопроса, так как он изначально спрашивал, какие есть гарантии для вызова такой функции.

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

Я столкнулся с реальной проблемой при портировании приложения OCaml на Haskell. Исходное приложение имело взаимно рекурсивную структуру многих типов, и код объявлял ряд функций, вызванных assert_structureN_is_correctдля N в 1..6 или 7, каждая из которых возвращала единицу, если структура действительно была правильной, и выдает исключение, если это не так. , Кроме того, эти функции вызывали друг друга, поскольку они разлагали условия корректности. В Haskell это лучше обрабатывается с помощью Either Stringмонады, поэтому я расшифровал ее таким образом, но вопрос как теоретический вопрос остался. Спасибо за все вклады и ответы.

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

Это не то, как работает Haskell. Каждый тип имеет еще одно значение в Haskell, а именно: нет значения, ошибки или так называемого «нижнего» значения, закодированного с помощью undefined. Таким образом, оценка на самом деле происходит:

main = print (f 1)

эквивалентно базовому языку

main = _Case (f 1) _Of x -> print x   -- pseudocode illustration

или даже ^(*)

main = _Case (f 1) _Of x -> putStr "()"

и сердечника _Caseявляется принуждение :

«Оценка %case[выражения] вызывает оценку тестируемого выражения (« проверяющий »). Значение проверяемого связано с переменной, следующей за %ofключевым словом, ...».

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

Haskell не является декларативным языком программирования.

^(*) print x = putStr (show x) и show () = "()", таким образом, showвызов может быть полностью скомпилирован.

Значение действительно известно заранее как (), и даже значение show ()заранее известно как "()". Тем не менее, принятая семантика Haskell требует, чтобы значение было (f 1)вынуждено ослабить нормальную форму головы перед тем, как приступить к печати заранее известной строки "()".

редактировать: рассмотреть concat (repeat []). Должно ли это быть [], или это должен быть бесконечный цикл?

Ответ "декларативного языка" на это наиболее вероятно []. Ответ Хаскелла - бесконечный цикл .

Лень - это «декларативное программирование бедняков», но это все же не настоящая вещь .

edit2 : print $ h (f 1) == _Case (h (f 1)) _Of () -> print ()и только hпринудительно, не f; и производить его ответ hне имеет ничего форсировать, в соответствии с ее определением h _ = ().

напутствие: у лени может быть смысл, но это не его определение. Лень это то, что она есть. Он определяется как все ценности, которые изначально были благими, которые принуждаются к WHNF в соответствии с требованиями main. Если это помогает избежать дна в определенном конкретном случае в соответствии с его конкретными обстоятельствами, то это делает. Если нет, то нет. Это все.

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

Исходя из отчета , мы имеем

f :: a -> ()
f = \_ -> (undefined :: ())

тогда

print (f 1)
 = print ((\ _ ->  undefined :: ()) 1)
 = print          (undefined :: ())
 = putStrLn (show (undefined :: ()))

и с

instance Show () where
    show :: () -> String
    show x = case x of () -> "()"

это продолжается

 = putStrLn (case (undefined :: ()) of () -> "()")

Теперь в разделе 3.17.3 Формальная семантика сопоставления с образцом отчета

Семантика caseвыражений [дана] на рисунках 3.1–3.3. Любая реализация должна вести себя так, чтобы эти идентичности содержали [...].

и случай (r)на рисунке 3.2 заявляет

(r)     case ⊥ of { K x1 … xn -> e; _ -> e′ } =  ⊥
        where K is a data constructor of arity n 

() является конструктором данных Arity 0, так что он такой же, как

(r)     case ⊥ of { () -> e; _ -> e′ } =  ⊥

и общий результат оценки, таким образом ⊥.