Почему существует только одна нестрогая функция от Int до Int?
В соответствии с этой статьей о денотационной семантике для Haskell существует только одна нестрогая функция (non-bottom prreserving) от Int до Int.
:
бывает, что существует только один прототип нестрогой функции типа Integer → Integer:
один x = 1
Его варианты constk x = k для каждого конкретного числа k. Почему это единственные возможности? Помните, что один n может быть не менее определенным, чем один ⊥. Поскольку Integer является плоской областью, оба должны быть равны.
По сути, это говорит о том, что единственными нестрогими функциями сигнатуры этого типа могут быть только постоянные функции. Я не следую этому аргументу. Я также не уверен, что подразумевается под плоской областью, остальная часть статьи приводит к мнению, что это просто означает, что у poset значений есть только один node: bottom.
Что-то подобное происходит для функции, идущей от A- > A, или A- > B? То есть они должны быть постоянными функциями?
Ответы
Ответ 1
Интуиция заключается в том, что ленивая функция не может проверить свой аргумент здесь, не заставляя ее (и, следовательно, становиться строгой). Если вы не проверяете свой аргумент, вы должны быть const
Реальный ответ в монотонности. Если вы думаете о семантических доменах как о позициях, где отношения упорядочения являются "определенными", все функции сохраняются в порядке. Зачем? Поскольку все днища созданы равными, а цикл навсегда - это то же самое, что и нижнее, то немонотонная функция будет той, которая решает проблему остановки.
Хорошо, так почему же это означает, что const создает только ленивые функции? Ну, скажем, выберите произвольную функцию f такую, что
f :: Integer -> Integer
f ⊥ = y
поскольку ⊥ <= x для всех x, это должно быть y <= f x. Если y - не нижнее значение, то единственным решением этого неравенства является f x = y
Изменить: причина этого аргумента в отношении таких типов, как Integer и Bool, но не для таких типов, как [a], является последним: Integer в некотором смысле имеет только один ⊥. То есть, все целые числа определены одинаково, за исключением ⊥. С другой стороны, ⊥ < (⊥:⊥) в то время как (⊥:⊥) < (⊥:[]) и (⊥:⊥) < (⊥:(⊥:⊥)) < (⊥:(⊥:(⊥:⊥))) < ... больше, (⊥:⊥) < ('a':⊥). То есть семантическая область [a] достаточно богата, что y <= f x с y =/= ⊥ не означает, что f x = y.
Ответ 2
Любая функция на Integer, которая не является const k для некоторой константы k, должна проверять ее аргумент. Вы не можете частично проверить Integer, который может быть - это то, что означает "плоский домен". Это является следствием того, как семантика Integer определена в спецификациях Haskell, а не что-то, что следует из семантики основного языка.
В отличие от этого, для каждого типа a существует бесконечно много нестрогих функций типа [a] -> [a], например. take1:
take1 (x:_) = [x]
Чтобы показать не строгость, определите
ones = 1 : ones
В терминах денотационной семантики [[ ones]] = ⊥. Но take1 ones оценивается как [1], поэтому take1 является нестрогим. Так что take2 (x:y:_) = [x,y], take10 и т.д.
Если вам нужны нестрогие непостоянные функции для целых чисел, вам нужно другое представление целых чисел, чем Integer, например:
data Bit = Zero | One
newtype BinaryInt = I [Bit]
Если мы интерпретируем список в I как "двоичное" двоичное целое число, то функция
mod2 (I []) = I []
mod2 (I (lsb:_)) = I [lsb]
является нестрогим.
