最不严格(*)

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.

它非常慢.显然这是因为它的参数大小(至少)是指数的,在每次递归时都会下降到两个分支.它需要更精细才能让它在合理的时间内运行.

最不严格的编程是相对未开发的领域,在实现和实际应用中都需要进行更多的研究.我很兴奋,并认为它有前途的领土.