Haskell и лень

Question

Я только начал изучать Haskell, и мне сказали, что Haskell ленив, т. Е. Он делает как можно меньше работы при оценке выражений, но я не думаю, что это правда.

Рассмотрим это:

und :: Bool -> Bool -> Bool 
und False y = False 
und y False = False 

non_term x = non_term (x+1) 

Оценка und (non_term 1) False никогда не заканчивается, но ясно, что результат, если значение False.

Есть ли способ реализации und (т.е. and на немецком языке) правильно (а не только частично, как указано выше), так что оба

und (non_term 1) False 

и

und False (non_term 1) 

возвращение Ложные?

Answer 1

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

Чтобы сделать эту работу, вам нужно собственное определение Bool, что делает явную задержку в любом вычислении:

import Prelude hiding (Bool(..)) 
data Bool = True | False | Delay Bool 
    deriving (Show, Eq) 

Тогда всякий раз, когда вы определяете значение типа Bool, вы должны сдерживать себя совместно рекурсию, где задержки сделаны явно с Delay конструктора, а не с помощью рекурсии, где вы должны оцените подвыражение , чтобы найти конструктор для возвращаемого значения верхнего уровня.

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

nonTerm :: Bool 
nonTerm = Delay nonTerm 

Тогда und становится:

und :: Bool -> Bool -> Bool 
und False y = False 
und x False = False 
und True y = y 
und x True = x 
und (Delay x) (Delay y) = Delay $ und x y 

, который работает просто отлично:

λ und True False 
False 
λ und False nonTerm 
False 
λ und nonTerm False 
False 
λ case und nonTerm nonTerm of Delay _ -> "delayed" ; _ -> "not delayed" 
"delayed" 

---

Продолжение на dfeuer's comment, это выглядит как то, что вы ищете может быть сделано с unamb

λ :m +Data.Unamb 
λ let undL False _ = False ; undL _ a = a 
λ let undR _ False = False ; undR a _ = a 
λ let und a b = undL a b `unamb` undR a b 
λ und True False 
False 
λ und False False 
False 
λ und False True 
False 
λ und True True 
True 
λ und undefined False 
False 
λ und False undefined 
False 

Answer 2

Haskell действительно ленивы. Лень означает, что выражение не оценивается, если это не требуется. Однако лень не означает, что два выражения могут быть оценены в произвольном порядке. Порядок оценки выражений в Haskell имеет значение. Например, рассмотрим вашу und функцию:

und :: Bool -> Bool -> Bool 
und False y = False 
und y False = False 

Во-первых, я хотел бы отметить, что эта функция является неполной.Полная функция:

und :: Bool -> Bool -> Bool 
und False y = False 
und y False = False 
und y True = True   -- you forgot this case 

В самом деле, функция und можно записать более кратко (и более лениво) следующим образом:

-- if the first argument is False then the result is False 
-- otherwise the result is the second argument 
-- note that the second argument is never inspected 

und :: Bool -> Bool -> Bool 
und False _ = False 
und _  x = x 

В любом случае, шаблон сопоставления синтаксиса в Haskell просто синтаксический сахар для выражений case. Например, исходная функция (неполный) будет обессахаренная до (до альфа-эквивалентности):

und :: Bool -> Bool -> Bool 
und x y = case x of False -> False 
        True -> case y of False -> False 
             True -> undefined 

Из этого мы можем видеть:

1. Ваша функция является неполной, поскольку последний случай undefined.
2. Ваша функция вычисляет второй аргумент, если первый аргумент равен True, хотя ему это не нужно. Помните, что выражения case всегда заставляют оценивать проверяемое выражение.
3. Ваша функция сначала проверяет x, а затем проверяет y, если x - True. Следовательно, здесь действительно существует явный порядок оценки. Обратите внимание, что если x оценивается до False, то y никогда не оценивается (доказательство того, что und действительно лениво).

Именно из-за этого порядка оценки, что ваше выражение und (non_term 1) False расходящимся:

und (non_term 1) False 
= case non_term 1 of False -> False 
        True -> case False of False -> False 
              True -> undefined 
= case non_term 2 of False -> False 
        True -> case False of False -> False 
              True -> undefined 
= case non_term 3 of False -> False 
        True -> case False of False -> False 
              True -> undefined 
       . 
       . 
       . 
       . 

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

und :: Bool -> Bool -> Bool 
und x y = case y of False -> False 
        True -> x  -- note that x is never inspected 

Теперь выражение und (non_term 1) False оценивается в False. Однако выражение und False (non_term 1) все еще расходится. Таким образом, ваш главный вопрос:

Есть ли способ реализации und (на немецком языке, т.е. and) правильно (а не только частично, как указано выше), так что оба

und (non_term 1) False 

и

und False (non_term 1) 

return False?

Короткий ответ: нет. Вам всегда нужен определенный порядок оценки; и в зависимости от порядка оценки либо und (non_term 1) False, либо und False (non_term 1) расходятся.

Означает ли это, что Haskell ошибочен/неисправен? Нет. Хаскелл поступает правильно и просто не дает никакого ответа. Для человека (который может оценивать оба выражения параллельно) казалось бы, что результат und (non_term 1) False должен быть False. Однако компьютеры всегда должны иметь порядок оценки.

Итак, в чем же проблема?По моему скромному мнению, актуальной проблемой является либо/или:

1. Параллельная оценка. Haskell должен вычислить выражение в обоих направлениях параллельно и выбрать тот, который заканчивается первым:

   import Data.Unamb (unamb) 
   
   type Endo a = a -> a 
   
   bidirectional :: Endo (a -> a -> b) 
   bidirectional = unamb <*> flip 
   
   und :: Bool -> Bool -> Bool 
   und = bidirectional (&&) 
   

2. Общая рекурсию. По моему скромному мнению, общая рекурсия слишком сильна для большинства случаев использования: она позволяет писать абсурдные функции, такие как non_term x = non_term (x + 1). Такие функции совершенно бесполезны. Если мы не будем рассматривать такие бесполезные функции, как исходные данные, то ваша оригинальная функция und является отличной функцией для использования (просто используйте последний случай или используйте &&).

Надеюсь, что это поможет.

Answer 3

Есть ли способ реализации унд (то есть и на немецком языке) правильно (не только частично, как указано выше), так что оба

und (non_term 1) False 

и

und False (non_term 1) 

возвращение Ложные?

Если вы заинтересованы в теории, есть классический теоретический результат, который гласит, что функция выше в ленивой лямбда-исчисления с рекурсией (который называется PCF) невозможно. Это было связано с Плоткиным в 1977 году. Вы можете найти обсуждение в Winskel's notes on denotational demantics в главе 8 «Полная абстракция».

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

Как уже упоминалось, в Haskell есть библиотека, определяющая unamb с помощью не последовательных средств, то есть с использованием некоторого параллелизма под ним, следовательно, выходящего за пределы PCF. С этим вы можете определить свою параллель or или and.