From 4d193562f4dd9fbf184f8245d47e061f0d2f9087 Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Sat, 13 Mar 2021 16:05:08 +0100 Subject: [PATCH] Heyting instances for Dropped, Lifted and Levitated --- src/Algebra/Lattice/Dropped.hs | 7 +++++++ src/Algebra/Lattice/Levitated.hs | 11 +++++++++++ src/Algebra/Lattice/Lifted.hs | 6 ++++++ 3 files changed, 24 insertions(+) diff --git a/src/Algebra/Lattice/Dropped.hs b/src/Algebra/Lattice/Dropped.hs index df33f5f..7d5729b 100644 --- a/src/Algebra/Lattice/Dropped.hs +++ b/src/Algebra/Lattice/Dropped.hs @@ -25,6 +25,7 @@ module Algebra.Lattice.Dropped ( import Prelude () import Prelude.Compat +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd @@ -88,6 +89,12 @@ instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where instance Lattice a => BoundedMeetSemiLattice (Dropped a) where top = Top +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 + -- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a retractDropped = foldDropped top id diff --git a/src/Algebra/Lattice/Levitated.hs b/src/Algebra/Lattice/Levitated.hs index 3163e05..57d1819 100644 --- a/src/Algebra/Lattice/Levitated.hs +++ b/src/Algebra/Lattice/Levitated.hs @@ -25,6 +25,7 @@ module Algebra.Lattice.Levitated ( import Prelude () import Prelude.Compat +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd @@ -100,6 +101,16 @@ instance Lattice a => BoundedJoinSemiLattice (Levitated a) where instance Lattice a => BoundedMeetSemiLattice (Levitated a) where top = Top +instance (Eq a, Heyting a) => Heyting (Levitated a) where + (Levitate a) ==> (Levitate b) | Meet a `leq` Meet b + = Top + | otherwise + = Levitate (a ==> b) + Top ==> a = a + _ ==> Top = Top + Bottom ==> _ = Top + _ ==> Bottom = Bottom + -- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@. retractLevitated :: (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) => Levitated a -> a retractLevitated = foldLevitated bottom id top diff --git a/src/Algebra/Lattice/Lifted.hs b/src/Algebra/Lattice/Lifted.hs index fe96dd7..d7852bb 100644 --- a/src/Algebra/Lattice/Lifted.hs +++ b/src/Algebra/Lattice/Lifted.hs @@ -25,6 +25,7 @@ module Algebra.Lattice.Lifted ( import Prelude () import Prelude.Compat +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd @@ -88,6 +89,11 @@ instance Lattice a => BoundedJoinSemiLattice (Lifted a) where instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where top = Lift top +instance Heyting a => Heyting (Lifted a) where + (Lift a) ==> (Lift b) = Lift (a ==> b) + Bottom ==> _ = Lift top + _ ==> Bottom = Bottom + -- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a retractLifted = foldLifted bottom id