(Новое?) Модальные операторы для складных - PullRequest
Новая
       34

(Новое?) Модальные операторы для складных

2 голосов
/ 24 апреля 2019

Этот пост следует в некотором смысле мой предыдущий . HTNW, в своем ответе там , определили тип данных Same и функцию allEq. Поэтому я подумал, что, определив тип данных AllDifferent, функцию allDiff и производные someEq и someDiff, я бы получил вид модального квадрата для 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

1 Ответ

3 голосов
/ 25 апреля 2019

Я бы сказал, что ваши функции образуют квадрат противоположностей, потому что они выражают количественную оценку, точнее - количественную оценку определенного предиката по парам элементов из складного контейнера [примечание 1]. С этой точки зрения наличие оппозиционных квадратов с участием модальных операторов отражает то, как модальности можно понимать как формы локального количественного определения. Я не вижу более прямой связи между вашими функциями и традиционными методами.

В более широком смысле, большинство подходов к выражению модальности в Haskell, о которых я знаю, опосредовано на теоретическом уровне изоморфизмом Карри-Говарда - см. Интересные операторы в Haskell, которые подчиняются модальным аксиомам за несколько ссылок на это. Я никогда не слышал о попытках думать о свойствах структур данных с точки зрения модальностей; однако я не думаю, что это как-то имеет смысл [примечание 2].

Примечание 1: Я говорю «пары элементов» с точки зрения, которая рассматривает отношения как наборы пар. Конкретно, я думаю об этой внеконкурсной реализации allEq ... 

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

... в которой мы проверяем, выполняется ли определенное свойство, а именно uncurry (==), для всех пар элементов xs.

Примечание 2: Например, возможная семантика мира может быть проработана с использованием графиков, как наглядно показано в этой демонстрации .

...