Skip to content
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.

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

Involution implies Noncontradiction and ExcludedMiddle #1242

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
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
Loading