Skip to content

Commit 495b1be

Browse files
garybgaryb
committed
Go back to a simpler class for BooleanAlgebra
1 parent ddeaf42 commit 495b1be

File tree

3 files changed

+60
-219
lines changed

3 files changed

+60
-219
lines changed

‎docs/Prelude.md‎

Lines changed: 23 additions & 125 deletions
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,6 @@ instance numUnit :: Num Unit
1717
instance eqUnit :: Eq Unit
1818
instance ordUnit :: Ord Unit
1919
instance boundedUnit :: Bounded Unit
20-
instance latticeUnit :: Lattice Unit
21-
instance boundedLatticeUnit :: BoundedLattice Unit
22-
instance complementedLatticeUnit :: ComplementedLattice Unit
23-
instance distributiveLatticeUnit :: DistributiveLattice Unit
2420
instance booleanAlgebraUnit :: BooleanAlgebra Unit
2521
instance showUnit :: Show Unit
2622
```
@@ -809,148 +805,50 @@ Instances should satisfy the following law in addition to the `Ord` laws:
809805

810806
- Ordering: `bottom <= a <= top`
811807

812-
#### `Lattice`
808+
#### `BooleanAlgebra`
813809

814810
``` purescript
815-
class (Ord a) <= Lattice a where
816-
sup :: a -> a -> a
817-
inf :: a -> a -> a
811+
class (Bounded a) <= BooleanAlgebra a where
812+
conj :: a -> a -> a
813+
disj :: a -> a -> a
814+
not :: a -> a
818815
```
819816

820817
##### Instances
821818
``` purescript
822-
instance latticeBoolean :: Lattice Boolean
823-
instance latticeUnit :: Lattice Unit
819+
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
820+
instance booleanAlgebraUnit :: BooleanAlgebra Unit
824821
```
825822

826-
The `Lattice` type class represents types that are partially ordered
827-
sets with a supremum (`sup` or `||`) and infimum (`inf` or `&&`).
823+
The `BooleanAlgebra` type class represents types that behave like boolean
824+
values.
828825

829-
Instances should satisfy the following laws in addition to the `Ord`
826+
Instances should satisfy the following laws in addition to the `Bounded`
830827
laws:
831828

832-
- Supremum:
833-
- `a || b >= a`
834-
- `a || b >= b`
835-
- Infimum:
836-
- `a && b <= a`
837-
- `a && b <= b`
838829
- Associativity:
839830
- `a || (b || c) = (a || b) || c`
840831
- `a && (b && c) = (a && b) && c`
841832
- Commutativity:
842833
- `a || b = b || a`
843834
- `a && b = b && a`
844-
- Absorption:
845-
- `a || (a && b) = a`
846-
- `a && (a || b) = a`
847-
- Idempotent:
848-
- `a || a = a`
849-
- `a && a = a`
850-
851-
#### `(||)`
852-
853-
``` purescript
854-
(||) :: forall a. (Lattice a) => a -> a -> a
855-
```
856-
857-
The `sup` operator.
858-
859-
#### `(&&)`
860-
861-
``` purescript
862-
(&&) :: forall a. (Lattice a) => a -> a -> a
863-
```
864-
865-
The `inf` operator.
866-
867-
#### `BoundedLattice`
868-
869-
``` purescript
870-
class (Bounded a, Lattice a) <= BoundedLattice a
871-
```
872-
873-
##### Instances
874-
``` purescript
875-
instance boundedLatticeBoolean :: BoundedLattice Boolean
876-
instance boundedLatticeUnit :: BoundedLattice Unit
877-
```
878-
879-
The `BoundedLattice` type class represents types that are finite
880-
lattices.
881-
882-
Instances should satisfy the following law in addition to the `Lattice`
883-
and `Bounded` laws:
884-
835+
- Distributivity:
836+
- `a && (b || c) = (a && b) || (a && c)`
837+
- `a || (b && c) = (a || b) && (a || c)`
885838
- Identity:
886839
- `a || bottom = a`
887840
- `a && top = a`
888-
- Annihiliation:
841+
- Idempotent:
842+
- `a || a = a`
843+
- `a && a = a`
844+
- Absorption:
845+
- `a || (a && b) = a`
846+
- `a && (a || b) = a`
847+
- Annhiliation:
889848
- `a || top = top`
890-
- `a && bottom = bottom`
891-
892-
#### `ComplementedLattice`
893-
894-
``` purescript
895-
class (BoundedLattice a) <= ComplementedLattice a where
896-
not :: a -> a
897-
```
898-
899-
##### Instances
900-
``` purescript
901-
instance complementedLatticeBoolean :: ComplementedLattice Boolean
902-
instance complementedLatticeUnit :: ComplementedLattice Unit
903-
```
904-
905-
The `ComplementedLattice` type class represents types that are lattices
906-
where every member is also uniquely complemented.
907-
908-
Instances should satisfy the following law in addition to the
909-
`BoundedLattice` laws:
910-
911-
- Complemented:
912-
- `not a || a == top`
913-
- `not a && a == bottom`
914-
- Double negation:
915-
- `not <<< not == id`
916-
917-
#### `DistributiveLattice`
918-
919-
``` purescript
920-
class (Lattice a) <= DistributiveLattice a
921-
```
922-
923-
##### Instances
924-
``` purescript
925-
instance distributiveLatticeBoolean :: DistributiveLattice Boolean
926-
instance distributiveLatticeUnit :: DistributiveLattice Unit
927-
```
928-
929-
The `DistributiveLattice` type class represents types that are lattices
930-
where the `&&` and `||` distribute over each other.
931-
932-
Instances should satisfy the following law in addition to the `Lattice`
933-
laws:
934-
935-
- Distributivity: `x && (y || z) = (x && y) || (x && z)`
936-
937-
#### `BooleanAlgebra`
938-
939-
``` purescript
940-
class (ComplementedLattice a, DistributiveLattice a) <= BooleanAlgebra a
941-
```
942-
943-
##### Instances
944-
``` purescript
945-
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
946-
instance booleanAlgebraUnit :: BooleanAlgebra Unit
947-
```
948-
949-
The `BooleanAlgebra` type class represents types that are Boolean
950-
algebras, also known as Boolean lattices.
951-
952-
Instances should satisfy the `ComplementedLattice` and
953-
`DistributiveLattice` laws.
849+
- Complementation:
850+
- `a && not a = bottom`
851+
- `a || not a = top`
954852

955853
#### `Show`
956854

‎package.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"gulp-jscs": "^1.6.0",
66
"gulp-jshint": "^1.10.0",
77
"gulp-plumber": "^1.0.0",
8-
"gulp-purescript": "^0.5.0",
8+
"gulp-purescript": "^0.5.0-rc.1",
99
"gulp-run": "~1.6.7"
1010
}
1111
}

‎src/Prelude.purs‎

Lines changed: 36 additions & 93 deletions
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,7 @@ module Prelude
2121
, Eq, eq, (==), (/=)
2222
, Ordering(..), Ord, compare, (<), (>), (<=), (>=)
2323
, Bounded, top, bottom
24-
, Lattice, sup, inf, (||), (&&)
25-
, BoundedLattice
26-
, ComplementedLattice, not
27-
, DistributiveLattice
28-
, BooleanAlgebra
24+
, BooleanAlgebra, conj, disj, not
2925
, Show, show
3026
) where
3127

@@ -729,118 +725,65 @@ instance boundedInt :: Bounded Int where
729725
top = 2147483647
730726
bottom = -2147483648
731727

732-
-- | The `Lattice` type class represents types that are partially ordered
733-
-- | sets with a supremum (`sup` or `||`) and infimum (`inf` or `&&`).
728+
-- | The `BooleanAlgebra` type class represents types that behave like boolean
729+
-- | values.
734730
-- |
735-
-- | Instances should satisfy the following laws in addition to the `Ord`
731+
-- | Instances should satisfy the following laws in addition to the `Bounded`
736732
-- | laws:
737733
-- |
738-
-- | - Supremum:
739-
-- | - `a || b >= a`
740-
-- | - `a || b >= b`
741-
-- | - Infimum:
742-
-- | - `a && b <= a`
743-
-- | - `a && b <= b`
744734
-- | - Associativity:
745735
-- | - `a || (b || c) = (a || b) || c`
746736
-- | - `a && (b && c) = (a && b) && c`
747737
-- | - Commutativity:
748738
-- | - `a || b = b || a`
749739
-- | - `a && b = b && a`
750-
-- | - Absorption:
751-
-- | - `a || (a && b) = a`
752-
-- | - `a && (a || b) = a`
740+
-- | - Distributivity:
741+
-- | - `a && (b || c) = (a && b) || (a && c)`
742+
-- | - `a || (b && c) = (a || b) && (a || c)`
743+
-- | - Identity:
744+
-- | - `a || bottom = a`
745+
-- | - `a && top = a`
753746
-- | - Idempotent:
754747
-- | - `a || a = a`
755748
-- | - `a && a = a`
756-
class (Ord a) <= Lattice a where
757-
sup :: a -> a -> a
758-
inf :: a -> a -> a
749+
-- | - Absorption:
750+
-- | - `a || (a && b) = a`
751+
-- | - `a && (a || b) = a`
752+
-- | - Annhiliation:
753+
-- | - `a || top = top`
754+
-- | - Complementation:
755+
-- | - `a && not a = bottom`
756+
-- | - `a || not a = top`
757+
class (Bounded a) <= BooleanAlgebra a where
758+
conj :: a -> a -> a
759+
disj :: a -> a -> a
760+
not :: a -> a
759761

760-
instance latticeBoolean :: Lattice Boolean where
761-
sup = boolOr
762-
inf = boolAnd
762+
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean where
763+
conj = boolAnd
764+
disj = boolOr
765+
not = boolNot
763766

764-
instance latticeUnit :: Lattice Unit where
765-
sup _ _ = unit
766-
inf _ _ = unit
767+
instance booleanAlgebraUnit :: BooleanAlgebra Unit where
768+
conj _ _ = unit
769+
disj _ _ = unit
770+
not _ = unit
767771

768772
infixr 2 ||
769773
infixr 3 &&
770774

771-
-- | The `sup` operator.
772-
(||) :: forall a. (Lattice a) => a -> a -> a
773-
(||) = sup
775+
-- | The `conj` operator.
776+
(||) :: forall a. (BooleanAlgebra a) => a -> a -> a
777+
(||) = conj
774778

775-
-- | The `inf` operator.
776-
(&&) :: forall a. (Lattice a) => a -> a -> a
777-
(&&) = inf
779+
-- | The `disj` operator.
780+
(&&) :: forall a. (BooleanAlgebra a) => a -> a -> a
781+
(&&) = disj
778782

779783
foreign import boolOr :: Boolean -> Boolean -> Boolean
780784
foreign import boolAnd :: Boolean -> Boolean -> Boolean
781-
782-
-- | The `BoundedLattice` type class represents types that are finite
783-
-- | lattices.
784-
-- |
785-
-- | Instances should satisfy the following law in addition to the `Lattice`
786-
-- | and `Bounded` laws:
787-
-- |
788-
-- | - Identity:
789-
-- | - `a || bottom = a`
790-
-- | - `a && top = a`
791-
-- | - Annihiliation:
792-
-- | - `a || top = top`
793-
-- | - `a && bottom = bottom`
794-
class (Bounded a, Lattice a) <= BoundedLattice a
795-
796-
instance boundedLatticeBoolean :: BoundedLattice Boolean
797-
798-
instance boundedLatticeUnit :: BoundedLattice Unit
799-
800-
-- | The `ComplementedLattice` type class represents types that are lattices
801-
-- | where every member is also uniquely complemented.
802-
-- |
803-
-- | Instances should satisfy the following law in addition to the
804-
-- | `BoundedLattice` laws:
805-
-- |
806-
-- | - Complemented:
807-
-- | - `not a || a == top`
808-
-- | - `not a && a == bottom`
809-
-- | - Double negation:
810-
-- | - `not <<< not == id`
811-
class (BoundedLattice a) <= ComplementedLattice a where
812-
not :: a -> a
813-
814-
instance complementedLatticeBoolean :: ComplementedLattice Boolean where
815-
not = boolNot
816-
817-
instance complementedLatticeUnit :: ComplementedLattice Unit where
818-
not _ = unit
819-
820785
foreign import boolNot :: Boolean -> Boolean
821786

822-
-- | The `DistributiveLattice` type class represents types that are lattices
823-
-- | where the `&&` and `||` distribute over each other.
824-
-- |
825-
-- | Instances should satisfy the following law in addition to the `Lattice`
826-
-- | laws:
827-
-- |
828-
-- | - Distributivity: `x && (y || z) = (x && y) || (x && z)`
829-
class (Lattice a) <= DistributiveLattice a
830-
831-
instance distributiveLatticeBoolean :: DistributiveLattice Boolean
832-
instance distributiveLatticeUnit :: DistributiveLattice Unit
833-
834-
-- | The `BooleanAlgebra` type class represents types that are Boolean
835-
-- | algebras, also known as Boolean lattices.
836-
-- |
837-
-- | Instances should satisfy the `ComplementedLattice` and
838-
-- | `DistributiveLattice` laws.
839-
class (ComplementedLattice a, DistributiveLattice a) <= BooleanAlgebra a
840-
841-
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
842-
instance booleanAlgebraUnit :: BooleanAlgebra Unit
843-
844787
-- | The `Show` type class represents those types which can be converted into
845788
-- | a human-readable `String` representation.
846789
-- |

0 commit comments

Comments
 (0)