Самый строгий (*)

Ответ 1

Да, но только с использованием ограниченной примеси.

laziestMult :: Num a => a -> a -> a
laziestMult a b = (a * b) `unamb` (b * a)

здесь unamb - это чистый вариант Conal Elliott amb. Оперативно amb выполняет два вычисления параллельно, возвращаясь к тому, что когда-либо наступит раньше. Денотационно unamb принимает два значения, где один строго больше (в смысле теории области), чем другой, и возвращает более высокий. Изменить: также это unamb, а не lub, поэтому вам нужно, чтобы они были равны, если никто не был внизу. Таким образом, у вас есть семантическое требование, которое должно выполняться, даже если оно не может быть принудительно введено типом система. Это реализовано по существу:

unamb a b = unsafePerformIO $ amb a b

Большая работа заключается в том, чтобы все это правильно работало с исключениями/управлением ресурсами/безопасностью потоков.

laziestMult верна, если * коммутативна. Это "наименее строгий", если * не является строгим в одном аргументе.

Подробнее см. в блоге.

Ответ 2

Ответ Phillip JF применим только к плоским доменам, но существуют экземпляры Num, которые не являются плоскими, например, ленивыми натуралами. Когда вы идете на эту арену, все становится довольно тонким.

data Nat = Zero | Succ Nat
    deriving (Show)

instance Num Nat where
    x + Zero = x
    x + Succ y = Succ (x + y)

    x * Zero = Zero
    x * Succ y = x + x * y

    fromInteger 0 = Zero
    fromInteger n = Succ (fromInteger (n-1))

    -- we won't need the other definitions

Для ленивых натуралей особенно важно, чтобы операции были наименее строгими, поскольку это область их использования; например мы используем их для сравнения длин возможно бесконечных списков, и если его операции не являются наименее строгими, тогда это будет расходиться, когда будет найдена полезная информация.

Как и ожидалось, (+) не является коммутативным:

ghci> undefined + Succ undefined
Succ *** Exception: Prelude.undefined
ghci> Succ undefined + undefined
*** Exception: Prelude.undefined

Итак, мы применим стандартный трюк, чтобы сделать так:

laxPlus :: Nat -> Nat -> Nat
laxPlus a b = (a + b) `unamb` (b + a)

который, кажется, работает, сначала

 ghci> undefined `laxPlus` Succ undefined
 Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` undefined
 Succ *** Exception: Prelude.undefined

но на самом деле это не

 ghci> Succ (Succ undefined) `laxPlus` Succ undefined
 Succ (Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` Succ (Succ undefined)
 Succ *** Exception: Prelude.undefined

Это связано с тем, что Nat не является плоской областью, а unamb применяется только к плоским доменам. Именно по этой причине я рассматриваю unamb примитив низкого уровня, который не следует использовать, кроме как для определения концепций более высокого уровня, - должно быть, не имеет значения, является ли домен плоским. Использование unamb будет чувствительным к рефакторам, которые изменяют структуру домена - та же самая причина seq является семантически уродливой. Нам нужно обобщить unamb так же, как seq обобщается на deeqSeq: это делается в модуле Data.Lub. Сначала нам нужно написать экземпляр HasLub для Nat:

instance HasLub Nat where
    lub a b = unambs [
                  case a of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb),
                  case b of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb)
              ]
        where
        Succ pa = a
        Succ pb = b

Предполагая, что это правильно, что не обязательно имеет место (это моя третья попытка до сих пор), теперь мы можем написать laxPlus':

laxPlus' :: Nat -> Nat -> Nat
laxPlus' a b = (a + b) `lub` (b + a)

и он действительно работает:

ghci> Succ undefined `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: Prelude.undefined
ghci> Succ (Succ undefined) `laxPlus'` Succ undefined
Succ (Succ *** Exception: Prelude.undefined

Итак, мы вынуждены обобщить, что наименее строгий шаблон для коммутативных двоичных операторов:

leastStrict :: (HasLub a) => (a -> a -> a) -> a -> a -> a
leastStrict f x y = f x y `lub` f y x

По крайней мере, гарантируется, что он будет коммутативным. Но, увы, есть и другие проблемы:

ghci> Succ (Succ undefined) `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: BothBottom

Мы ожидаем, что сумма двух чисел, по крайней мере, 2 должна быть не менее 4, но здесь мы получим число, которое должно быть не менее 2. Я не могу придумать способ изменить leastStrict, чтобы дать нам результат, который мы хотим, по крайней мере, не без введения нового ограничения класса. Чтобы исправить эту проблему, нам нужно выкопать в рекурсивное определение и одновременно сопоставить шаблон по обоим аргументам на каждом шаге:

laxPlus'' :: Nat -> Nat -> Nat
laxPlus'' a b = lubs [
    case a of
        Zero -> b
        Succ a' -> Succ (a' `laxPlus''` b),
    case b of
        Zero -> a
        Succ b' -> Succ (a `laxPlus''` b')
    ]

И, наконец, мы получаем тот, который дает как можно больше информации, я полагаю:

ghci> Succ (Succ undefined) `laxPlus''` Succ (Succ undefined)
Succ (Succ (Succ (Succ *** Exception: BothBottom

Если мы применим один и тот же шаблон к временам, мы получим что-то, что тоже работает:

laxMult :: Nat -> Nat -> Nat
laxMult a b = lubs [
    case a of
        Zero -> Zero
        Succ a' -> b `laxPlus''` (a' `laxMult` b),
    case b of
        Zero -> Zero
        Succ b' -> a `laxPlus''` (a `laxMult` b')
    ]

ghci> Succ (Succ undefined) `laxMult` Succ (Succ (Succ undefined))
Succ (Succ (Succ (Succ (Succ (Succ *** Exception: BothBottom

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

asLeast :: Nat -> Nat
atLeast Zero = undefined
atLeast (Succ n) = Succ (atLeast n)

ghci> atLeast 7 `laxMult` atLeast 7
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ ^CInterrupted.

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

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