Skip to content

Commit

Permalink
Involution implies Noncontradiction and ExcludedMiddle (#1242)
Browse files Browse the repository at this point in the history
  • Loading branch information
sideeffffect authored Jan 16, 2024
1 parent 14d825c commit 9a77df1
Show file tree
Hide file tree
Showing 6 changed files with 13 additions and 21 deletions.
12 changes: 5 additions & 7 deletions docs/abstraction-diagrams.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,10 @@ sidebar_label: "Abstraction Diagrams"
```mermaid
classDiagram
Absorption~A~ <|-- DistributiveAbsorption~A~
Absorption~A~ <|-- Involution~A~
Absorption~A~ <|-- Noncontradiction~A~
Absorption~A~ <|-- ExcludedMiddle~A~
ExcludedMiddle~A~ <|-- Involution~A~
Noncontradiction~A~ <|-- Involution~A~
class Absorption~A~{
() or(=> A, => A): A
() and(=> A, => A): A
Expand All @@ -20,20 +21,17 @@ classDiagram
Boolean
Set[A]
}
class Involution~A~{
Boolean
() complement(=> A): A
}
class Noncontradiction~A~{
Boolean
() complement(=> A): A
() bottom: A
}
class ExcludedMiddle~A~{
Boolean
() complement(=> A): A
() top: A
}
class Involution~A~{
Boolean
}
```


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,6 @@ object InvolutionLaws extends Lawful[InvolutionEqual] {
* The set of all laws that instances of `Involution` must satisfy.
*/
lazy val laws: Laws[InvolutionEqual] =
AbsorptionLaws.laws + involutionLaw
ExcludedMiddleLaws.laws + NoncontradictionLaws.laws + involutionLaw

}
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,8 @@ object Absorption {
*/
def apply[A](implicit absorption: Absorption[A]): Absorption[A] = absorption

implicit lazy val BoolInstance: DistributiveAbsorption[Boolean]
with ExcludedMiddle[Boolean]
with Involution[Boolean]
with Noncontradiction[Boolean] =
new DistributiveAbsorption[Boolean]
with ExcludedMiddle[Boolean]
with Involution[Boolean]
with Noncontradiction[Boolean] {
implicit lazy val BoolInstance: DistributiveAbsorption[Boolean] with Involution[Boolean] =
new DistributiveAbsorption[Boolean] with Involution[Boolean] {
override def complement(a: => Boolean): Boolean = !a
override val bottom: Boolean = false
override val top: Boolean = true
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ trait ExcludedMiddle[A] extends Complement[A] {
object ExcludedMiddle {

/**
* Summons an implicit `Complement[A]`.
* Summons an implicit `ExcludedMiddle[A]`.
*/
def apply[A](implicit excludedMiddle: ExcludedMiddle[A]): ExcludedMiddle[A] = excludedMiddle
}
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package zio.prelude
package experimental

trait Involution[A] extends Complement[A]
trait Involution[A] extends ExcludedMiddle[A] with Noncontradiction[A]

object Involution {

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ object ExcludedMiddleEqual {
}
}

trait InvolutionEqual[A] extends AbsorptionEqual[A] with Involution[A]
trait InvolutionEqual[A] extends ExcludedMiddleEqual[A] with NoncontradictionEqual[A] with Involution[A]

object InvolutionEqual {
implicit def derive[A](implicit involution0: Involution[A], equal0: Equal[A]): InvolutionEqual[A] =
Expand All @@ -77,9 +77,9 @@ object InvolutionEqual {

override def and(l: => A, r: => A): A = involution0.and(l, r)

override def Or: Associative[OrF[A]] = involution0.Or
override def Or: Identity[OrF[A]] = involution0.Or

override def And: Associative[AndF[A]] = involution0.And
override def And: Identity[AndF[A]] = involution0.And

protected def checkEqual(l: A, r: A): Boolean = equal0.equal(l, r)
}
Expand Down

0 comments on commit 9a77df1

Please sign in to comment.