heyting-algebras 0.0.2.0 → 0.2.0.1

raw patch · 12 files changed

+180/−557 lines, 12 filesdep ~basedep ~free-algebrasdep ~hashablePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, free-algebras, hashable, lattices, universe-base

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• README.md +6/−7
• heyting-algebras.cabal +16/−16
• src/Algebra/Boolean.hs +50/−23
• src/Algebra/Boolean/Free.hs +10/−23
• src/Algebra/Boolean/Properties.hs +11/−6
• src/Algebra/Heyting.hs +0/−314
• src/Algebra/Heyting/BoolRing.hs +7/−5
• src/Algebra/Heyting/Free.hs +0/−83
• src/Algebra/Heyting/Layered.hs +15/−27
• src/Algebra/Heyting/Properties.hs +10/−11
• test/Main.hs +50/−42

@@ -1,5 +1,10 @@ # Revision history for heyting-algebra +## 0.1.0.0++* Swapped Boolean (now a type class) and BooleanAlgebra (now a data type)+* Reexport Algebra.Heyting and Algebra.Heyting.Free modules from lattices+ ## 0.0.2.0  * Added Algebra.Heyting.CounterExample

@@ -1,13 +1,12 @@ # Heyting Algebras [![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)-[![Travis Build Status](https://travis-ci.org/coot/heyting-algebras.svg?branch=master)](https://travis-ci.org/coot/heyting-algebras)+[![POSIX](https://github.com/coot/heyting-algebras/actions/workflows/posix.yml/badge.svg)](https://github.com/coot/heyting-algebras/actions/workflows/posix.yml) -This package contains type classes and instances for many Heyting algebras-which are in the Haskell eco-system.  It is build on top of-[lattices](https://hackage.haskell.org/package/lattices) and-[free-algebras](https://hackage.haskell.org/package/free-algebras) (to provide-combinators for free Heyting algebras).  The package also defines a type class-for Boolean algebras and comes with many useful instances.++This package now extends+[lattices](https://hackage.haskell.org/package/lattices) by providing more+Heyting algebras.  The package also defines a type class for Boolean algebras+and comes with many useful instances.  A note about notation: this package is based on [lattices](https://hackage.haskell.org/package/lattices), and both are using

@@ -1,5 +1,6 @@+cabal-version:       2.0 name:                heyting-algebras-version:             0.0.2.0+version:             0.2.0.1 synopsis:            Heyting and Boolean algebras description:   This package provides Heyting and Boolean operations together@@ -8,35 +9,34 @@ license-file:        LICENSE author:              Marcin Szamotulski maintainer:          profunctor@pm.me-copyright:           (c) 2018-2019 Marcin Szamotulski+copyright:           (c) 2018-2021 Marcin Szamotulski category:            Math build-type:          Simple extra-source-files:   ChangeLog.md   README.md-cabal-version:       >=1.10-tested-with:         GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.3+tested-with:         GHC==8.10.4  library-  exposed-modules:     Algebra.Heyting-                       Algebra.Heyting.Free-                       Algebra.Heyting.Layered+  exposed-modules:     Algebra.Heyting.Layered                        Algebra.Heyting.BoolRing                        Algebra.Heyting.CounterExample                        Algebra.Heyting.Properties                        Algebra.Boolean                        Algebra.Boolean.Free                        Algebra.Boolean.Properties-  build-depends:       base           >= 4.9      && < 4.13-                     , containers     >= 0.4.2    && < 0.7-                     , free-algebras  >= 0.0.4    && < 0.0.8-                     , hashable       >= 1.2.6.1  && < 1.3-                     , lattices       >= 1.0      && < 1.8+  reexported-modules:  lattices:Algebra.Heyting+                    ,  lattices:Algebra.Heyting.Free+  build-depends:       base            >= 4.9     && < 4.16+                     , containers      >= 0.4.2   && < 0.7+                     , free-algebras   >= 0.1.0.1 && < 0.1.1.0+                     , hashable        >= 1.2.6.1 && < 1.4+                     , lattices        >= 2.0     && < 2.1                      , semiring-simple >= 1.0     && < 1.2-                     , tagged         >= 0.8.5    && < 0.9+                     , tagged          >= 0.8.5   && < 0.9                      , unordered-containers-                                      >= 0.2.6.0  && < 0.3-                     , universe-base  >= 1.0      && < 1.1+                                       >= 0.2.6.0 && < 0.3+                     , universe-base   >= 1.0     && < 1.2   hs-source-dirs:      src   default-language:    Haskell2010   default-extensions:  FlexibleInstances@@ -44,7 +44,7 @@                        PackageImports   ghc-options:        -Wall -test-suite tests+test-suite test   type:                exitcode-stdio-1.0   hs-source-dirs:      test   main-is:             Main.hs

@@ -5,52 +5,79 @@ module Algebra.Boolean   ( BooleanAlgebra   , (==>)-  , not-  , iff-  , iff'+  , neg     -- * Adjunction between Boolean and Heyting algebras   , Boolean-  , runBoolean+  , runBooleanAlgebra   , boolean   ) where -import           Prelude hiding (not)-+import           Control.Applicative    (Const (..)) import           Data.Data              (Data, Typeable)+import           Data.Functor.Identity  (Identity (..))+import           Data.Proxy             (Proxy (..))+import           Data.Semigroup         ( All (..)+                                        , Any (..)+                                        , Endo (..)+                                        )+import           Data.Tagged            (Tagged (..)) import           GHC.Generics           (Generic) +import           Algebra.Heyting import           Algebra.Lattice        ( Lattice-                                        , BoundedLattice-                                        , JoinSemiLattice (..)                                         , BoundedJoinSemiLattice-                                        , MeetSemiLattice (..)                                         , BoundedMeetSemiLattice                                         ) -import           Algebra.Heyting        ( HeytingAlgebra (..)-                                        , BooleanAlgebra-                                        , iff-                                        , iff'-                                        , not-                                        , toBoolean-                                        )+class Heyting a => Boolean a +instance Boolean Bool++instance Boolean All++instance Boolean Any++instance Boolean ()++instance Boolean (Proxy a)++instance Boolean a => Boolean (Tagged t a)++instance Boolean b => Boolean (a -> b)++#if MIN_VERSION_base(4,8,0)+instance Boolean a => Boolean (Identity a)+#endif++instance Boolean a => Boolean (Const a b)++instance Boolean a => Boolean (Endo a)++-- | Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto+-- it; moreover it is a monad (Heyting algebra is a category as every poset is)+-- which preserves finite infima.+--+toBoolean :: Heyting a => a -> a+toBoolean = neg . neg+ -- | -- @'Boolean'@ is the left adjoint functor from the category of Heyting algebras -- to the category of Boolean algebras; its right adjoint is the inclusion.-newtype Boolean a = Boolean-    { runBoolean :: a -- ^ extract value from @'Boolean'@+newtype BooleanAlgebra a = BooleanAlgebra+    { runBooleanAlgebra :: a -- ^ extract value from @'Boolean'@     }   deriving-    ( JoinSemiLattice, BoundedJoinSemiLattice, MeetSemiLattice-    , BoundedMeetSemiLattice, Lattice, BoundedLattice, HeytingAlgebra+    ( BoundedJoinSemiLattice+    , BoundedMeetSemiLattice+    , Lattice+    , Heyting     , Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic     ) -instance HeytingAlgebra a => BooleanAlgebra (Boolean a)+instance Heyting a => Boolean (BooleanAlgebra a)  -- | -- Smart constructro of the @'Boolean'@ type.-boolean :: HeytingAlgebra a => a -> Boolean a-boolean = Boolean . toBoolean+boolean :: Heyting a => a -> BooleanAlgebra a+boolean = BooleanAlgebra . toBoolean 

@@ -5,58 +5,45 @@  import           Control.Monad     (ap) import           Algebra.Lattice   ( BoundedJoinSemiLattice (..)-                                   , JoinSemiLattice (..)                                    , BoundedMeetSemiLattice (..)-                                   , MeetSemiLattice (..)-                                   , BoundedLattice-                                   , Lattice+                                   , Lattice (..)                                    ) import           Data.Algebra.Free ( AlgebraType0                                    , AlgebraType                                    , FreeAlgebra (..)-                                   , proof                                    , fmapFree                                    , bindFree                                    ) -import           Algebra.Boolean   (BooleanAlgebra)-import           Algebra.Heyting   (HeytingAlgebra (..))+import           Algebra.Boolean   (Boolean)+import           Algebra.Heyting  -- | -- Free Boolean algebra.  @'FreeAlgebra'@ instance provides all the usual -- combinators for a free algebra. newtype FreeBoolean a = FreeBoolean-  { runFreeBoolean :: forall h . BooleanAlgebra h => (a -> h) -> h }--instance JoinSemiLattice (FreeBoolean a) where-  FreeBoolean f \/ FreeBoolean g = FreeBoolean (\inj -> f inj \/ g inj)+  { runFreeBoolean :: forall h . Boolean h => (a -> h) -> h }  instance BoundedJoinSemiLattice (FreeBoolean a) where   bottom = FreeBoolean (\_ -> bottom) -instance MeetSemiLattice (FreeBoolean a) where-  FreeBoolean f /\ FreeBoolean g = FreeBoolean (\inj -> f inj /\ g inj)- instance BoundedMeetSemiLattice (FreeBoolean a) where   top = FreeBoolean (\_ -> top) -instance Lattice (FreeBoolean a)--instance BoundedLattice (FreeBoolean a)+instance Lattice (FreeBoolean a) where+  FreeBoolean f /\ FreeBoolean g = FreeBoolean (\inj -> f inj /\ g inj)+  FreeBoolean f \/ FreeBoolean g = FreeBoolean (\inj -> f inj \/ g inj) -instance HeytingAlgebra (FreeBoolean a) where+instance Heyting (FreeBoolean a) where   FreeBoolean f ==> FreeBoolean g = FreeBoolean (\inj -> f inj ==> g inj) -instance BooleanAlgebra (FreeBoolean a)+instance Boolean (FreeBoolean a)  type instance AlgebraType0 FreeBoolean a = ()-type instance AlgebraType  FreeBoolean a = BooleanAlgebra a+type instance AlgebraType  FreeBoolean a = Boolean a instance FreeAlgebra FreeBoolean where   returnFree a = FreeBoolean (\inj -> inj a)   foldMapFree f (FreeBoolean inj) = inj f--  codom  = proof-  forget = proof  instance Functor FreeBoolean where   fmap = fmapFree

@@ -14,12 +14,17 @@  -- | -- Test that @'not'@ satisfies Boolean algebra axioms.-prop_not :: (HeytingAlgebra a, Ord a, Eq a, Ord e) => a -> CounterExample e-prop_not a =-     (not (not a) === a)-  /\ (not a /\ a === bottom)-  /\ (not a \/ a === top)+prop_neg :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e+prop_neg a =+     (neg (neg a) === a)+  /\ (neg a /\ a === bottom)+  /\ (neg a \/ a === top) +prop_not :: (Heyting a, Ord a, Eq a, Ord e) => a -> CounterExample e+prop_not = prop_neg++{-# DEPRECATED prop_not "Use prop_neg" #-}+ data BooleanAlgebraLawViolation a   = BALVHeytingAlgebraLawViolation (HeytingAlgebraLawViolation a)   | BALVNotLawViolation a@@ -29,7 +34,7 @@ -- Test that @a@ is satisfy both @'Algebra.Heyting.prop_HeytingAlgebra'@ and -- @'prop_not'@. prop_BooleanAlgebra-  :: (BooleanAlgebra a, Ord a, Eq a, Show a)+  :: (Boolean a, Ord a, Eq a, Show a)   => a -> a -> a -> CounterExample (BooleanAlgebraLawViolation a) prop_BooleanAlgebra a b c =      (fmapCounterExample BALVHeytingAlgebraLawViolation $ prop_HeytingAlgebra a b c)

@@ -1,314 +0,0 @@-{-# LANGUAGE CPP #-}--module Algebra.Heyting-  ( -- * Heyting algebras-    HeytingAlgebra (..)-  , implies-  , (<=>)-  , iff-  , iff'-  , toBoolean-    -- * Boolean algebras-  , BooleanAlgebra-  )-  where---import           Prelude hiding (not)-import qualified Prelude--import           Control.Applicative    (Const (..))-import           Data.Functor.Identity  (Identity (..))-import           Data.Hashable          (Hashable)-import           Data.Proxy             (Proxy (..))-import           Data.Semigroup         ( All (..)-                                        , Any (..)-                                        , Endo (..)-                                        )-import           Data.Tagged            (Tagged (..))-import           Data.Universe.Class    (Finite, universe)-import qualified Data.Map as M-import           Data.Set (Set)-import qualified Data.Set as Set-import qualified Data.HashMap.Lazy as HM-import qualified Data.HashSet      as HS--import           Algebra.Lattice ( BoundedJoinSemiLattice (..)-                                 , BoundedMeetSemiLattice (..)-                                 , BoundedLattice-                                 , Meet (..)-                                 , bottom-                                 , top-                                 , (/\)-                                 , (\/)-                                 )-import           Algebra.Lattice.Dropped    (Dropped (..))-import           Algebra.Lattice.Lifted     (Lifted (..))-import           Algebra.Lattice.Levitated  (Levitated)-import qualified Algebra.Lattice.Levitated as L-import           Algebra.Lattice.Ordered    (Ordered (..))-import           Algebra.Lattice.Op         (Op (..))-import           Algebra.PartialOrd         (leq)---- --- Heyting algebras------- |--- Heyting algebra is a bounded semi-lattice with implication which should--- satisfy the following law:------ prop> x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)------ We also require that a Heyting algebra is a distributive lattice, which--- means any of the two equivalent conditions holds:------ prop> a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c--- prop> a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)------ This means @a ⇒ b@ is an--- [exponential object](https://ncatlab.org/nlab/show/exponential%2Bobject),--- which makes any Heyting algebra--- a [cartesian--- closed category](https://ncatlab.org/nlab/show/cartesian%2Bclosed%2Bcategory).--- This means that Curry isomorphism holds (which takes a form of an actual--- equality):------ prop> a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c------ Some other useful properties of Heyting algebras:--- --- prop> (a ⇒ b) ∧ a ≤ b--- prop> b ≤ a ⇒ a ∧ b--- prop> a ≤ b  iff a ⇒ b = ⊤--- prop> b ≤ b' then a ⇒ b ≤ a ⇒ b'--- prop> a'≤ a  then a' ⇒ b ≤ a ⇒ b--- prop> not (a ∧ b) = not (a ∨ b)--- prop> not (a ∨ b) = not a ∧ not b-class BoundedLattice a => HeytingAlgebra a where-  -- |-  -- Default implementation: @a ==> b = not a \/ b@, it requires @not@ to-  -- satisfy Boolean axioms, which will make it into a Boolean algebra.-  ---  -- Fixity is less than fixity of both @'\/'@ and @'/\'@.-  (==>) :: a -> a -> a-  (==>) a b = not a \/ b--  -- |-  -- Default implementation: @not a = a '==>' 'bottom'@-  ---  -- It is useful for optimisation reasons.-  not :: a -> a-  not a = a ==> bottom--  {-# MINIMAL (==>) | not #-}--infixr 4 ==>---- |--- @'implies'@ is an alias for @'==>'@-implies :: HeytingAlgebra a => a -> a -> a-implies = (==>)--(<=>) :: HeytingAlgebra a => a -> a -> a-a <=> b = (a ==> b) /\ (b ==> a)---- |--- @'iff'@ is an alias for @'<=>'@-iff :: HeytingAlgebra a => a -> a -> a-iff = (<=>)--iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool-iff' a b = Meet top `leq` Meet (iff a b)-  --- |--- Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto it;--- moreover it is a monad (Heyting algebra is a category as every poset is) which--- preserves finite infima.-toBoolean :: HeytingAlgebra a => a -> a-toBoolean = not . not--instance HeytingAlgebra Bool where-  not = Prelude.not--instance HeytingAlgebra All where-  All a ==> All b = All (a ==> b)-  not (All a)     = All (not a)--instance HeytingAlgebra Any where-  Any a ==> Any b = Any (a ==> b)-  not (Any a)     = Any (not a)--instance HeytingAlgebra () where-  _ ==> _ = ()--instance HeytingAlgebra (Proxy a) where-  _ ==> _ = Proxy--instance HeytingAlgebra a => HeytingAlgebra (Tagged t a) where-  Tagged a ==> Tagged b = Tagged (a ==> b)--instance HeytingAlgebra b => HeytingAlgebra (a -> b) where-  f ==> g = \a -> f a ==> g a--#if MIN_VERSION_base(4,8,0)-instance HeytingAlgebra a => HeytingAlgebra (Identity a) where-  (Identity a) ==> (Identity b) = Identity (a ==> b)-#endif--instance HeytingAlgebra a => HeytingAlgebra (Const a b) where-  (Const a) ==> (Const b) = Const (a ==> b)--instance HeytingAlgebra a => HeytingAlgebra (Endo a) where-  (Endo f) ==> (Endo g) = Endo (f ==> g)--instance (HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (a, b) where-  (a0, b0) ==> (a1, b1) = (a0 ==> a1, b0 ==> b1)------- Dropped, Lifted, Levitated, Ordered------- |--- Subdirectly irreducible Heyting algebra.-instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a) where-  (Drop a) ==> (Drop b) | Meet a `leq` Meet b = Top-                        | otherwise           = Drop (a ==> b)-  Top      ==> a        = a-  _        ==> Top      = Top--instance HeytingAlgebra a => HeytingAlgebra (Lifted a) where-  (Lift a) ==> (Lift b) = Lift (a ==> b)-  Bottom   ==> _        = Lift top-  _        ==> Bottom   = Bottom--instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Levitated a) where-  (L.Levitate a) ==> (L.Levitate b) | Meet a `leq` Meet b = L.Top-                                    | otherwise           = L.Levitate (a ==> b)-  L.Top          ==> a              = a-  _              ==> L.Top          = L.Top-  L.Bottom       ==> _              = L.Top-  _              ==> L.Bottom       = L.Bottom--instance (Ord a, Bounded a) => HeytingAlgebra (Ordered a) where-  Ordered a ==> Ordered b | a <= b    = top-                          | otherwise = Ordered b------- containers------- |--- Power set: the canonical example of a Boolean algebra-instance (Ord a, Finite a) => HeytingAlgebra (Set a) where-  not a = Set.fromList universe `Set.difference` a--instance (Eq a, Finite a, Hashable a) => HeytingAlgebra (HS.HashSet a) where-  not a = HS.fromList universe `HS.difference` a---- |--- It is not a boolean algebra (even if values are).-instance (Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (M.Map k v) where-  -- _xx__-  -- __yy_-  -- T_iTT where i = x ==> y; T = top; _ missing (or removed key)-#if __GLASOW_HASKELL__ >= 804-  a ==> b =-    Merge.merge-      Merge.dropMissing                    -- drop if an element is missing in @b@-      (Merge.mapMissing (\_ _ -> top))     -- put @top@ if an element is missing in @a@-      (Merge.zipWithMatched (\_ -> (==>))) -- merge  matching elements with @==>@-      a b--    \/ M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b) ] -                            -- for elements which are not in a, nor in b add-                            -- a @top@ key-#else-  a ==> b =-    M.intersectionWith (==>) a b-      `M.union` M.map (const top) (M.difference b a)-      `M.union` M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b)]-#endif--instance (Eq k, Finite k, Hashable k, HeytingAlgebra v) => HeytingAlgebra (HM.HashMap k v) where-  a ==> b = HM.intersectionWith (==>) a b-    `HM.union` HM.map (const top) (HM.difference b a)-    `HM.union` HM.fromList [(k, top) | k <- universe, not (HM.member k a), not (HM.member k b)]---- --- Boolean algebras------ They are defined in the same module, to avoid module dependency: @Op a@ is--- a Boolean algebra (thus Heyting algebra in the first place), whenever @a@ is--- a Boolean algebra.------- |--- Boolean algebra is a Heyting algebra which negation satisfies the law of--- excluded middle, i.e. either of the following:------ prop> not . not == not------ or------ prop> x ∨ not x == top------ Another characterisation of Boolean algebras is as--- [complemented](https://en.wikipedia.org/wiki/Complemented_lattice)--- [distributive lattices](https://ncatlab.org/nlab/show/distributive+lattice)--- where the complement satisfies the following three properties:------ prop> (not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law--- prop> not (not a) == a                             -- involution law--- prop> a ≤ b ⇒ not b ≤ not a                        -- order-reversing-class HeytingAlgebra a => BooleanAlgebra a------- Instances-----instance BooleanAlgebra Bool--instance BooleanAlgebra All--instance BooleanAlgebra Any--instance BooleanAlgebra ()--instance BooleanAlgebra (Proxy a)--instance BooleanAlgebra a => BooleanAlgebra (Tagged t a)--instance BooleanAlgebra b => BooleanAlgebra (a -> b)--#if MIN_VERSION_base(4,8,0)-instance BooleanAlgebra a => BooleanAlgebra (Identity a)-#endif--instance BooleanAlgebra a => BooleanAlgebra (Const a b)--instance BooleanAlgebra a => BooleanAlgebra (Endo a)--instance (BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b)------- containers-----instance (Ord a, Finite a) => BooleanAlgebra (Set a)-------- Op------- | Whenever @a@ is a Boolean Algebra, @Op a@ is a Boolean algebra as well,--- which in particular means that it is a Heyting algebra in the first place.----instance BooleanAlgebra a => HeytingAlgebra (Op a) where-  (Op a) ==> (Op b) = Op (not a /\ b)---- | Every boolean algebra is isomorphic to power set @P(X)@ of some set @X@;--- then `not :: Op (P(X)) -> P(X)` is a lattice isomorphism, thus `Op (P(X))` is--- a boolean algebra, since @P(X)@ is.-instance BooleanAlgebra a => BooleanAlgebra (Op a)

@@ -5,9 +5,11 @@   , (<+>)   ) where -import           Prelude hiding (not)+import           Prelude +#if __GLASGOW_HASKELL__ < 808 import           Data.Monoid (Monoid (..))+#endif #if __GLASGOW_HASKELL__ < 804 import           Data.Semigroup (Semigroup (..)) #endif@@ -31,11 +33,11 @@ newtype BoolRing a = BoolRing { getBoolRing :: a }  -- | Sum is [symmetric differnce](https://en.wikipedia.org/wiki/Symmetric_difference).-instance HeytingAlgebra a => Semigroup (BoolRing a) where-  (BoolRing a) <> (BoolRing b) = BoolRing $ (not a /\ b) \/ (a /\ not b)+instance Heyting a => Semigroup (BoolRing a) where+  (BoolRing a) <> (BoolRing b) = BoolRing $ (neg a /\ b) \/ (a /\ neg b)  -- | In a Boolean ring @a + a = 0@, hence @negate = id@.-instance HeytingAlgebra a => Monoid (BoolRing a) where+instance Heyting a => Monoid (BoolRing a) where   mempty = BoolRing bottom  #if __GLASGOW_HASKELL__ <= 804@@ -43,6 +45,6 @@ #endif  -- |  Multiplication is given by @'/\'@-instance HeytingAlgebra a => Semiring (BoolRing a) where+instance Heyting a => Semiring (BoolRing a) where   BoolRing a <.> BoolRing b = BoolRing (a \/ b)   one = BoolRing top

@@ -1,83 +0,0 @@-{-# LANGUAGE TypeFamilies #-}-module Algebra.Heyting.Free-  ( FreeHeyting (..)-  , atom-  ) where--import           Prelude hiding (not)--import           Control.Monad     (ap)-import           Algebra.Lattice   ( BoundedJoinSemiLattice (..)-                                   , JoinSemiLattice (..)-                                   , BoundedMeetSemiLattice (..)-                                   , MeetSemiLattice (..)-                                   , BoundedLattice-                                   , Lattice-                                   )-import           Data.Algebra.Free ( AlgebraType0-                                   , AlgebraType-                                   , FreeAlgebra (..)-                                   , proof-                                   , fmapFree-                                   , bindFree-                                   )--import           Algebra.Heyting   (HeytingAlgebra (..))---- |--- Free Heyting algebra.  @'FreeAlgebra'@ instance provides all the usual--- combinators for a free algebra.------ The--- [graph](https://en.wikipedia.org/wiki/Heyting_algebra#/media/File:Rieger-Nishimura.svg)--- of free Heyting algebra with one generator\/atom, i.e. @'FreeHeyting' ()@.----newtype FreeHeyting a = FreeHeyting-  { runFreeHeyting :: forall h . HeytingAlgebra h => (a -> h) -> h }--instance JoinSemiLattice (FreeHeyting a) where-  FreeHeyting f \/ FreeHeyting g = FreeHeyting (\inj -> f inj \/ g inj)--instance BoundedJoinSemiLattice (FreeHeyting a) where-  bottom = FreeHeyting (\_ -> bottom)--instance MeetSemiLattice (FreeHeyting a) where-  FreeHeyting f /\ FreeHeyting g = FreeHeyting (\inj -> f inj /\ g inj)--instance BoundedMeetSemiLattice (FreeHeyting a) where-  top = FreeHeyting (\_ -> top)--instance Lattice (FreeHeyting a)--instance BoundedLattice (FreeHeyting a)--instance HeytingAlgebra (FreeHeyting a) where-  FreeHeyting f ==> FreeHeyting g = FreeHeyting (\inj -> f inj ==> g inj)-  not (FreeHeyting f)             = FreeHeyting (\inj -> not (f inj))---- |--- Construct an atom of the @'FreeHeyting'@ lattice (in the laguage of free--- algebra, it is called a generator, e.g. @atom = returnFree@).----atom :: a -> FreeHeyting a-atom = \a -> FreeHeyting $ \inj -> inj a--type instance AlgebraType0 FreeHeyting a = ()-type instance AlgebraType  FreeHeyting a = HeytingAlgebra a-instance FreeAlgebra FreeHeyting where-  returnFree = atom-  foldMapFree f (FreeHeyting inj) = inj f--  codom  = proof-  forget = proof--instance Functor FreeHeyting where-  fmap = fmapFree--instance Applicative FreeHeyting where-  pure = returnFree-  (<*>) = ap--instance Monad FreeHeyting where-  return = returnFree-  (>>=) = bindFree

@@ -6,14 +6,11 @@ import           Prelude  import           Algebra.Lattice ( BoundedJoinSemiLattice (..)-                                 , JoinSemiLattice (..)                                  , BoundedMeetSemiLattice (..)-                                 , MeetSemiLattice (..)-                                 , BoundedLattice-                                 , Lattice+                                 , Lattice (..)                                  ) -import           Algebra.Heyting (HeytingAlgebra (..))+import           Algebra.Heyting ( Heyting (..) )  -- | -- Layer one Heyting algebra on top of the other.  Note: this is not@@ -23,38 +20,29 @@   | Upper b   deriving (Show, Eq, Ord) -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (Layered a b) where+instance ( Lattice a+         , Lattice b+         ) => Lattice (Layered a b) where+  l@Lower{} /\ Upper _   = l+  Upper _   /\ l@Lower{} = l+  Lower l   /\ Lower l'  = Lower $ l /\ l'+  Upper u   /\ Upper u'  = Upper $ u /\ u'+   Lower _   \/ u@Upper{} = u   u@Upper{} \/ Lower _   = u   Lower l   \/ Lower l'  = Lower $ l \/ l'   Upper u   \/ Upper u'  = Upper $ u \/ u' -instance (BoundedJoinSemiLattice a, JoinSemiLattice b) => BoundedJoinSemiLattice (Layered a b) where+instance (BoundedJoinSemiLattice a, Lattice b) => BoundedJoinSemiLattice (Layered a b) where   bottom = Lower bottom -instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (Layered a b) where-  l@Lower{} /\ Upper _   = l-  Upper _   /\ l@Lower{} = l-  Lower l   /\ Lower l'  = Lower $ l /\ l'-  Upper u   /\ Upper u'  = Upper $ u /\ u'--instance (MeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where+instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where   top = Upper top -instance ( Lattice a-         , Lattice b-         ) => Lattice (Layered a b)--instance ( Lattice a-         , Lattice b-         , BoundedJoinSemiLattice a-         , BoundedMeetSemiLattice b-         ) => BoundedLattice (Layered a b)--instance ( HeytingAlgebra a-         , HeytingAlgebra b+instance ( Heyting a+         , Heyting b          , Eq a-         ) => HeytingAlgebra (Layered a b) where+         ) => Heyting (Layered a b) where   Lower _   ==> Upper _      = Upper top   Upper _   ==> l@Lower{}    = l   Upper u   ==> Upper u'     = Upper $ u ==> u'

@@ -4,10 +4,9 @@ -- module Algebra.Heyting.Properties where -import           Prelude hiding (not)+import           Prelude  import           Data.List (intersperse)-import           Data.Semigroup ((<>))  import           Algebra.Lattice ( Lattice                                  , BoundedJoinSemiLattice@@ -125,13 +124,13 @@       withArgs "x ∧ a ≤ b then x ≤ (a ⇒ b)" [x, a, b]    show (HAVNot a b) =-    withArgs "a ≤ b ⇏ not a" [a, b]+    withArgs "a ≤ b ⇏ neg a" [a, b]    show (HAVNotAndMeet a b) =-    withArgs "not (a ∧ b) ≠ not a ∨ not b" [a, b]+    withArgs "neg (a ∧ b) ≠ neg a ∨ neg b" [a, b]    show (HAVNotAndJoin a b) =-    withArgs "not (a ∨ b) ≠ not a ∧ not b" [a, b]+    withArgs "neg (a ∨ b) ≠ neg a ∧ neg b" [a, b]    show (HAVImplicationAndOrd a b) =     withArgs "(a ⇒ b) ∧ a ≰ b" [a, b]@@ -144,7 +143,7 @@ -- Verifies the Heyting algebra law for @==>@: -- for all @a@: @_ /\ a@ is left adjoint to  @a ==>@ -- and some other properties that are a consequence of that.-prop_implies :: (HeytingAlgebra a, Ord a, Eq a, Show a)+prop_implies :: (Heyting a, Ord a, Eq a, Show a)              => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_implies x a b =     fromBool@@ -155,25 +154,25 @@       (Meet (x /\ a) `leq` Meet b ==> (Meet x `leq` Meet (a ==> b)))   /\ fromBool       (HAVNot a b)-      (Meet a `leq` Meet b ==> (Meet (not b) `leq` Meet (not a)))+      (Meet a `leq` Meet b ==> (Meet (neg b) `leq` Meet (neg a)))   /\ annotate       (HAVNotAndMeet a b)-      (not (a /\ b) === (not a \/ not b))+      (neg (a /\ b) === (neg a \/ neg b))   /\ annotate       (HAVNotAndJoin a b)-      (not (a \/ b) === (not a /\ not b))+      (neg (a \/ b) === (neg a /\ neg b))   /\ fromBool       (HAVImplicationAndOrd a a)       (Meet ((a ==> b) /\ a) `leq` Meet b)  -- |--- Useful for testing valid instances of @'HeytingAlgebra'@ type class. It+-- Useful for testing valid instances of @'Heyting'@ type class. It -- validates: -- -- * bounded lattice laws -- * @'prop_implies'@ prop_HeytingAlgebra-  :: (HeytingAlgebra a, Ord a, Eq a, Show a)+  :: (Heyting a, Ord a, Eq a, Show a)   => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) prop_HeytingAlgebra a b c = 

@@ -1,6 +1,9 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE PackageImports             #-} +{-# OPTIONS_GHC -Wno-orphans #-}+ module Main where  import           Data.Universe.Class (Universe (..), Finite)@@ -9,12 +12,12 @@ import           Data.Map (Map) import qualified Data.Map as Map -import           Algebra.Lattice ( JoinSemiLattice-                                 , BoundedJoinSemiLattice-                                 , MeetSemiLattice+import           Algebra.Lattice ( BoundedJoinSemiLattice                                  , BoundedMeetSemiLattice-                                 , Lattice-                                 , BoundedLattice+                                 , Lattice (..)+                                 , Meet (..)+                                 , bottom+                                 , top                                  ) import           Algebra.Lattice.Dropped (Dropped (..)) import           Algebra.Lattice.Lifted (Lifted (..))@@ -29,9 +32,10 @@ import           Algebra.Heyting.CounterExample import           Algebra.Heyting.Properties import           Algebra.Heyting.Layered+import           Algebra.PartialOrd (leq)  import           Test.Tasty-import           Test.Tasty.QuickCheck hiding (Ordered)+import           Test.Tasty.QuickCheck hiding (Ordered, (==>))  main :: IO () main = defaultMain tests@@ -42,6 +46,33 @@   -> Property counterExampleProperty = maybe (property True) (flip counterexample False) . fromCounterExample' +--+-- Orphan instances+-- issue: https://github.com/haskellari/lattices/pull/112+--++instance Heyting a => Heyting (Lifted a) where+  (Lift a) ==> (Lift b) = Lift (a ==> b)+  Bottom   ==> _        = Lift top+  _        ==> Bottom   = Bottom++instance (Eq a, Heyting a) => Heyting (Dropped a) where+  (Drop a) ==> (Drop b) | Meet a `leq` Meet b = Top+                        | otherwise           = Drop (a ==> b)+  Top      ==> a        = a+  _        ==> Top      = Top++instance Boolean a => Heyting (Op a) where+  (Op a) ==> (Op b) = Op (neg a /\ b)++instance (Eq a, Heyting a) => Heyting (Levitated a) where+  (L.Levitate a) ==> (L.Levitate b) | Meet a `leq` Meet b = L.Top+                                    | otherwise           = L.Levitate (a ==> b)+  L.Top          ==> a              = a+  _              ==> L.Top          = L.Top+  L.Bottom       ==> _              = L.Top+  _              ==> L.Bottom       = L.Bottom+ --  -- List of tast cases --@@ -51,7 +82,6 @@   testGroup "heyting-algebras tests"     [ testGroup "Boolean algebras"         [ testProperty "Bool"                                         prop_boolean_Bool-        , testProperty "(Bool, Bool)"                                 prop_boolean_BoolBool         , testProperty "Boolean (Lifted Bool)"                        prop_boolean_LiftedBool         , testProperty "Boolean (Dropped Bool)"                       prop_boolean_DroppedBool         , testProperty "(Set S5)"                                     prop_boolean_Set@@ -68,12 +98,10 @@         , testProperty "Levitated Bool"                               prop_heyting_LevitatedBool         , testProperty "Sum (Lifted Bool) (Dropped Bool)"             prop_heyting_LayeredLiftedDropped         , testProperty "Levitated (Ordered Int)"                      prop_heyting_LevitatedOrderedInt-        , testProperty "Map S5 Bool"                                  prop_heyting_MapS5Bool         , testProperty "Dropped (Lifted Bool)"                        prop_heyting_DroppedLiftedBool         , testProperty "Lifted (Dropped Bool)"                        prop_heyting_LiftedDroppedBool         , testProperty "Lifted (Lifted Bool)"                         prop_heyting_LiftedLiftedBool         , testProperty "Dropped (Dropped Bool)"                       prop_heyting_DroppedDroppedBool-        , testProperty "CounterExample"                               prop_heyting_CounterExample         ]     ] @@ -88,18 +116,13 @@ prop_boolean_Bool =   (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra -prop_boolean_BoolBool-  :: BooleanProp (Bool, Bool)-prop_boolean_BoolBool =-  (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra- prop_boolean_LiftedBool-  :: BooleanProp (Arb (Boolean (Arb (Lifted Bool))))+  :: BooleanProp (Arb (BooleanAlgebra (Arb (Lifted Bool)))) prop_boolean_LiftedBool =   (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra  prop_boolean_DroppedBool-  :: BooleanProp (Arb (Boolean (Arb (Dropped Bool))))+  :: BooleanProp (Arb (BooleanAlgebra (Arb (Dropped Bool)))) prop_boolean_DroppedBool =   (fmap . fmap) counterExampleProperty . prop_BooleanAlgebra @@ -119,21 +142,21 @@ prop_non_boolean_LiftedBool =     expectFailure   . counterExampleProperty @String-  . prop_not+  . prop_neg  prop_non_boolean_DroppedBool   :: NonBooleanProp (Arb (Dropped Bool)) prop_non_boolean_DroppedBool =     expectFailure   . counterExampleProperty @String-  . prop_not+  . prop_neg  prop_non_boolean_LevitatedOrderedInt   :: NonBooleanProp (Arb (Levitated (Arb (Ordered Int)))) prop_non_boolean_LevitatedOrderedInt =     expectFailure   . counterExampleProperty @String-  . prop_not+  . prop_neg  -- -- Heyting algebra tests@@ -171,11 +194,6 @@ prop_heyting_LevitatedOrderedInt =   (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra -prop_heyting_MapS5Bool-  :: HeytingProp (Arb (Map S5 Bool))-prop_heyting_MapS5Bool =-  (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra- prop_heyting_DroppedLiftedBool   :: HeytingProp (Composed Dropped Lifted Bool) prop_heyting_DroppedLiftedBool =@@ -196,22 +214,15 @@ prop_heyting_DroppedDroppedBool =   (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra -prop_heyting_CounterExample-  :: HeytingProp (Composed Lifted Op (Set S5))-prop_heyting_CounterExample =-  (fmap . fmap) counterExampleProperty . prop_HeytingAlgebra  -- | Arbitrary wrapper for varous lattices. -- newtype Arb a = Arb a-  deriving ( JoinSemiLattice-           , BoundedJoinSemiLattice-           , MeetSemiLattice+  deriving ( BoundedJoinSemiLattice            , BoundedMeetSemiLattice            , Lattice-           , BoundedLattice-           , BooleanAlgebra-           , HeytingAlgebra+           , Boolean+           , Heyting            , Eq            , Ord            )@@ -252,9 +263,9 @@     : [ Arb (L.Levitate a') | a' <- shrink a ]   shrink (Arb L.Top) = [] -instance (Arbitrary a, HeytingAlgebra a, Eq a) => Arbitrary (Arb (Boolean a)) where+instance (Arbitrary a, Heyting a, Eq a) => Arbitrary (Arb (BooleanAlgebra a)) where   arbitrary = Arb . boolean <$> arbitrary-  shrink (Arb a) = filter (/= Arb a) (Arb . boolean <$> shrink (runBoolean a))+  shrink (Arb a) = filter (/= Arb a) (Arb . boolean <$> shrink (runBooleanAlgebra a))    instance Arbitrary a => Arbitrary (Arb (Ordered a)) where@@ -287,14 +298,11 @@ -- | Arbitrary newtype wrapper for compositions of heigher kinded types. -- newtype Composed f g a = Composed (f (g a))-  deriving ( JoinSemiLattice-           , BoundedJoinSemiLattice-           , MeetSemiLattice+  deriving ( BoundedJoinSemiLattice            , BoundedMeetSemiLattice            , Lattice-           , BoundedLattice-           , BooleanAlgebra-           , HeytingAlgebra+           , Boolean+           , Heyting            , Eq            , Ord            )