haskell - 最不严格 (*)

Question

是否可以(*)在 Haskell 中使用最不严格的语义来实现（首选标准化的 Haskell，但扩展是可以的。使用编译器内部是作弊）？例如，这样的定义应该导致以下情况为真：

0 * ⊥ = 0
⊥ * 0 = 0

并且只有：

⊥ * ⊥ = ⊥

我可以构建满足上述情况之一的模式匹配，但不能同时满足这两种情况，因为零检查会强制该值。

Answer 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如果*是可交换的，则正确。*如果在一个参数中不严格，则它是“最不严格的” 。

有关更多信息，请参阅Conal 的博客

Answer 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.

它慢得可怕。很明显，这是因为它的参数大小（至少）呈指数级，在每次递归时下降到两个分支。要让它在合理的时间内运行，还需要更多的技巧。

最不严格的编程是相对未开发的领域，无论是在实现上还是在实际应用中，都需要进行更多的研究。我对此感到兴奋，并认为它很有前景。