Heyting instances for Dropped, Lifted and Levitated #112
Conversation
| @@ -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 | |||
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Potential incompatibility of PartialOrd a and Heyting a is indeed a good point. I have to think this through.
There was a problem hiding this comment.
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.
No description provided.