Skip to content

Heyting instances for Dropped, Lifted and Levitated #112

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Heyting instances for Dropped, Lifted and Levitated #112

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/Algebra/Lattice/Dropped.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ module Algebra.Lattice.Dropped (
import Prelude ()
import Prelude.Compat

import Algebra.Heyting
import Algebra.Lattice
import Algebra.PartialOrd

Expand Down Expand Up @@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not so sure about this. Why this and not requiring PartialOrd? tough choice. Probably that why I just didn't add an instance.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PartialOrd must be compatible with Lattice instance which means that both leq :: Meet a -> Meet a -> Bool and leq :: a -> a -> Bool must be give the same result. The argument for using ParitalOrd is that it is be more explicit, and putting Eq a only looks like it is requiring less: having Heyting implies that there is a partial order (the one given by Meet or Join which are the same). In a sense this is indifferent what one would use, and I'd be fine with either of the two, thinking about it now, maybe ParitalOrd would be slightly nicer.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Potential incompatibility of PartialOrd a and Heyting a is indeed a good point. I have to think this through.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The first chapter of Burris & Sankappanavar might help you. It explains that lattices can be defined either as posests with all finite suprema and infima or algebraic structures (as in here). Please excuse me if I am point something that you're well familiar with.

| 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
Expand Down
11 changes: 11 additions & 0 deletions src/Algebra/Lattice/Levitated.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ module Algebra.Lattice.Levitated (
import Prelude ()
import Prelude.Compat

import Algebra.Heyting
import Algebra.Lattice
import Algebra.PartialOrd

Expand Down Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions src/Algebra/Lattice/Lifted.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ module Algebra.Lattice.Lifted (
import Prelude ()
import Prelude.Compat

import Algebra.Heyting
import Algebra.Lattice
import Algebra.PartialOrd

Expand Down Expand Up @@ -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
Expand Down