This post follows in a sense my previous one. HTNW, in their answer there, 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 for Foldable structures.
If the result of my work is correct, how can one appropriately characterise this set of data types and functions?
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
I'd say that your functions form a square of oppositions because they express quantification -- more specifically, quantification of a certain predicate over pairs of elements from the foldable container [note 1]. From this point of view, there being squares of oppositions involving modal operators reflects how modalities can be understood as forms of local quantification. I don't see a more direct link from your functions to the traditional modalities.
On a broader note, most approaches towards expressing modality in Haskell that I know of are mediated, on a theoretical level, by the Curry-Howard isomorphism -- see Interesting operators in Haskell that obey modal axioms for a few references on that. I have never heard about attempts to think about properties of data structures in terms of modalities; however, I don't think it is impossible for that to make sense somehow [note 2].
Note 1: I say "pairs of elements" from the vantage point that regards relations as sets of pairs. In concrete terms, I'm thinking of this out-of-competition implementation of allEq...
allEq :: (Foldable f, Eq a) => f a -> Bool
allEq xs = all (uncurry (==)) (liftA2 (,) xs' xs')
where
xs' = toList xs
... in which we check whether a certain property, namely uncurry (==), holds for all pairs of elements of xs.
Note 2: For one, possible world semantics can be worked with using graphs, as vividly illustrated in this demo.