时间戳

首页 > 解决方案 > （新？）可折叠的模态运算符

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

问题描述

这篇文章从某种意义上来说是我之前的一篇。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

标签： haskellfoldablemodal-logic

解决方案

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

在更广泛的意义上，我所知道的在 Haskell 中表达模态的大多数方法在理论上都是由 Curry-Howard 同构介导的——请参阅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：一方面，可以使用图形来处理可能的世界语义，如本演示中所生动说明的那样。

推荐阅读