Лемма: Предполагая, что эта эквивалентность у нас есть (\x -> ⊥) = ⊥ :: A -> B
.
Доказательство: ⊥ = (\x -> ⊥ x)
по eta-эквивалентности и (\x -> ⊥ x) = (\x -> ⊥)
по сокращению под лямбду.
В отчете Haskell 2010, раздел 6.2, seq
функция определяется двумя уравнениями:
seq :: a -> b -> b seq ⊥ b = ⊥ seq ab = b, если a ≠ ⊥
Затем он заявляет: «Как следствие, ⊥ - это не то же самое, что \ x -> ⊥, поскольку для их различения можно использовать seq».
У меня вопрос, действительно ли это является следствием определения seq
?
Кажется, что неявный аргумент был seq
бы не вычислимым, если seq (\x -> ⊥) b = ⊥
. Однако я не смог доказать, что такое seq
было бы неисчислимо. Мне кажется, что такое seq
является как монотонным, так и непрерывным, что ставит его в область вычислимости.
Алгоритм, реализующий такие как сл может работать, пытаясь найти для некоторых , x
где f x ≠ ⊥
, перечисляя область f
начиная с ⊥. Хотя такая реализация, даже если это вообще возможно, становится довольно волосатой, когда мы хотим сделать ее seq
полиморфной.
Есть ли доказательство того, что нет вычислимого, seq
который идентифицирует себя (\x -> ⊥)
с ⊥ :: A -> B
? Кроме того , есть некоторые строительства , seq
что делает идентифицировать (\x -> ⊥)
с ⊥ :: A -> B
?
источник
seq
seq
Обратите внимание , что спецификация для
seq
которых вы цитируете это не его определение. Процитируем отчет Haskell «Функция seq определяется уравнениями : [а затем уравнениями, которые вы даете]».Такое поведение будет нарушать спецификацию
seq
.Важно отметить, что, поскольку он
seq
является полиморфным,seq
его нельзя определить в терминах деконструкторов (проекции / сопоставление с образцом и т. Д.) Ни по одному из двух параметров.Если
seq' (\x -> ⊥) b
кто-то может подумать, что мы могли бы применить первый параметр (который является функцией) к некоторому значению, а затем выйти. Но,seq
никогда не может отождествить первый параметр со значением функции (даже если это один для некоторого использованияseq
) из-за его параметрического полиморфного типа. Параметричность означает, что мы ничего не знаем о параметрах. Кроме того,seq
никогда не может взять выражение и решить "это this?" (см. проблему Остановки),seq
можно только попытаться оценить ее, а сама расходиться до ⊥.Что
seq
нужно сделать, это оценить первый параметр (не полностью, а как «слабую головную нормальную форму» [1], то есть для самого верхнего конструктора), а затем вернуть второй параметр. Если первый параметр оказывается⊥
(то есть, не завершающее вычисление), то его оценка приводитseq
к тому, что он не завершается, и, таким образомseq ⊥ a = ⊥
.[1] Бесплатные теоремы в присутствии seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf
источник
f : forall a . a -> T
(гдеT
есть некоторый другой тип), тогдаf
не может применить никакие деконструкторы к своему первому аргументу, так как она не знает, какие деконструкторы применить. Мы не можем сделать "случай" на типах. Я попытался улучшить ответ выше (в том числе цитируя информацию о том, какseq
оценивать нормальную форму головы).Самсон Абрамский давно обдумал этот вопрос и написал статью под названием « Ленивое лямбда-исчисление ». Итак, если вы хотите формальные определения, это то, где вы можете посмотреть.
источник
Доказательство того, что λ x. Ω ≠ Ω в является одной из целей, которые Абрамский ставит перед своей теорией ленивого лямбда-исчисления (страница 2 своей статьи , уже цитируемой Удаем Редди), потому что они оба находятся в нормальной форме со слабой головой. Что касается определения 2.7, он явно обсуждает, что эта-редукция λ x. M x → M, как правило, недопустимо, но это возможно, если M заканчивается в каждой среде. Это не означает, что M должна быть полной функцией - только то, что вычисление M должно завершиться (например, путем сокращения до лямбды).
Ваш вопрос, кажется, мотивирован практическими проблемами (производительность). Однако, хотя отчет по Хаскеллу может быть не совсем ясен, я сомневаюсь, что приравнивать λ x. with produce создаст полезную реализацию Haskell; реализует ли он Haskell '98 или нет, остается спорным, но, учитывая замечание, ясно, что авторы предполагали, что это так.
Наконец, как seq генерировать элементы для произвольного типа ввода? (Я знаю, что QuickCheck определяет для этого произвольный класс типов, но вы не можете добавлять такие ограничения здесь). Это нарушает параметричность.
Обновлено : мне не удалось закодировать это право (потому что я не очень бегло говорю на Хаскеле), и для исправления этого требуются вложенные
runST
области. Я попытался использовать одну ячейку ссылки (в монаде ST), чтобы сохранить такие произвольные элементы, прочитать их позже и сделать их общедоступными. Параметричность доказывает, чтоbreak_parametricity
ниже не может быть определено (за исключением возврата bottom, например, ошибки), в то время как он может восстановить элементы, которые сгенерирует ваш предложенный seq.Я должен признать, что я немного нечетко формализирую доказательство параметричности, необходимое здесь, но это неформальное использование параметричности является стандартным в Haskell; но из работ Дерека Дрейера я узнал, что необходимая теория быстро разрабатывается в последние годы.
правок:
источник
(\x -> writeSTRef cell (Just x) >> return x)
на случайных входах не выполняет запись в ячейку. Выполняются только те команды ST, которые превращают его в последовательность, переданную вrunST
. Точно так же, бегmain = (putStrLn "Hello") `seq` (return ())
не печатает ничего на дисплее.