（新？）可折叠模态运算符

Question

post 在某种意义上遵循 . HTNW, , defined the data type Same and the function allEq. So I thought that by defining the data type AllDifferent, the function allDiff and the derived ones someEq and someDiff, I would have obtained a kind of modal square Foldable 结构。

如果我的工作结果是正确的，如何才能恰当地表征这组数据类型和函数？

import qualified Data.Set as S
import qualified Data.Matrix as MT  -- only for exemplification

-- EXAMPLES --
-- allEq    $ MT.fromLists ["aaa","aaa"] -> True
-- allEq    $ MT.fromLists ["aaa","daa"] -> False
-- someEq   $ MT.fromLists ["abc","dea"] -> True
-- someEq   $ MT.fromLists ["abc","def"] -> False
-- allDiff  $ MT.fromLists ["abc","def"] -> True
-- allDiff  $ MT.fromLists ["abc","dea"] -> False
-- someDiff $ MT.fromLists ["aaa","daa"] -> True
-- someDiff $ MT.fromLists ["aaa","aaa"] -> False

-- ====================== allEq ======================
-- produced by HTNW in response to my previous post.

data Same a = Vacuous | Fail | Same a
instance Eq a => Semigroup (Same a) where
    Vacuous    <> x       = x
    Fail       <> _       = Fail
    s@(Same l) <> Same r  = if l == r then s else Fail
    x          <> Vacuous = x
    _          <> Fail    = Fail

instance Eq a => Monoid (Same a) where
    mempty = Vacuous
allEq :: (Foldable f, Eq a) => f a -> Bool
allEq xs = case foldMap Same xs of
                Fail -> False
                _    -> True

-- ====================== allDiff ======================

data AllDifferent a = VacuousAD | FailAD | AllDifferent (S.Set a)
--  The lazy construction avoids taking the last union when it's not necessary, which can 
-- save a significant amount of time when folding over large trees that are 
-- pretty balanced at their roots.

instance (Eq a, Ord a) => Semigroup (AllDifferent a) where
    VacuousAD      <> x       = x
    FailAD         <> _       = FailAD
    AllDifferent l <> AllDifferent r  = if S.disjoint l r 
                                        then AllDifferent (S.union l r)
                                        else FailAD
    x              <> VacuousAD = x
    _              <> FailAD    = FailAD

instance (Eq a, Ord a) => Monoid (AllDifferent a) where
    mempty = VacuousAD
allDiff :: (Foldable f, Eq a, Ord a) => f a -> Bool
allDiff xs = case foldMap (AllDifferent . S.singleton)  xs of
                FailAD -> False
                _    -> True

-- ====================== someEq ======================

someEq :: (Foldable f, Eq a, Ord a) => f a -> Bool
someEq = not . allDiff

 -- ====================== someDiff ======================

someDiff :: (Foldable f, Eq a) => f a -> Bool 
someDiff = not . allEq

Answer 1

我会说你的函数形成了一个对立方，因为它们表达了量化——更具体地说，是对可折叠容器中成对元素的某个谓词的量化[注 1]。从这个角度来看，涉及模态算子的对立方块反映了如何将模态理解为局部量化的形式。我没有看到从您的功能到传统模式更直接的 link。

从更广泛的角度来看，我所知道的在 Haskell 中表达模态的大多数方法在理论层面上都是由 Curry-Howard 同构介导的——参见中的一些对此的参考。我从来没有听说过有人试图从模态的角度来思考数据结构的属性。但是，我认为这并非不可能以某种方式有意义 [注 2]。

注1：我说"pairs of elements"是从将关系视为成对集合的角度出发的。具体来说，我正在考虑 allEq...

的赛外实施

allEq :: (Foldable f, Eq a) => f a -> Bool
allEq xs = all (uncurry (==)) (liftA2 (,) xs' xs')
    where
    xs' = toList xs

... 其中我们检查某个属性，即 uncurry (==) 是否适用于 xs.

的所有元素对

注 2： 首先，可能世界语义可以使用图来处理，如 this demo.

中生动说明的那样

（新？）可折叠模态运算符

(New?) Modal Operators for Foldable

haskell

foldable

modal-logic