(New?) Modal Operators for Foldable

Question

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

Side note: use `disjoint l r` instead of `null (intersection l r)` to improve performance. The former doesn't have to build a result set. — dfeuer, Apr 24 '19 at 16:52
I don't really understand what you're asking. You seem to have a problem and a solution. What remains? — dfeuer, Apr 24 '19 at 16:55
Also, you should include a comment explaining that making the `AllDifferent` constructor lazy 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. Defend your code against careless "optimization"! — dfeuer, Apr 24 '19 at 17:30
@dfeuer Thank for the suggestions; I've just modified the code. My question is a theoretical question about the kind of this modal operators. Are true modal operator like: Necessity - Possibility; Obligatory - Permissible; ecc. ? — Alberto Capitani, Apr 24 '19 at 19:58

score 3 · Accepted Answer · answered Apr 24 '19 at 23:50

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.

Wheh you write (liftA2 (,) xs' xs') you intend (liftA2 (,) (init xs') (tail xs')? — Alberto Capitani, Apr 25 '19 at 07:22
@AlbertoCapitani Not really. If you wanted to exploit transitivity, you might write `zip (drop 1 xs') xs'` (note that is a different list applicative). My implementation above, though, is merely illustrative, and in any case if we were concerned about performance we would have to generate the pairs in a single pass through `xs` (otherwise memory retention woes await). On a mostly unrelated note, an analogous implementation of `allDifferent` wouldn't be quite as straightforward, as `(/=)` is neither reflexive nor transitive. — duplode, Apr 25 '19 at 10:41

(New?) Modal Operators for Foldable

1 Answers1