Description
This package contains type classes and instances for many Heyting algebras which are in the Haskell ecosystem. It is build on top of lattices and freealgebras (to provide combinators for free Heyting algebras). The package also defines a type class for Boolean algebras and comes with a handful of instances.
A note about notation: this package is based on lattices, and both are using notation and names common in lattice theory and logic. Where && becomes ∧ and is called meet and  is denoted by ∨ and is usually called as join. The lattice package provides \/ and /\ operators.
A very good introduction to Heyting algebras can be found at ncatlab. Heyting algebras are the crux of intuitionistic logic, which drops the axiom of excluded middle. From categorical point of view, Heyting algebras are posets (categories with at most one arrow between any objects), which are also Cartesian closed (and finitely (co)complete). Note that this makes any Heyting algebra a simply typed lambda calculus; hence one more incentive to learn how to use them. For example currying holds in Heyting algebras: `a => (b ⇒ c)` is equal to `(a ∧ b) ⇒ c`.
Heyting Algebras alternatives and similar packages
Based on the "Logic" category.
Alternatively, view Heyting Algebras alternatives based on common mentions on social networks and blogs.

tamarinprover
Main source code repository of the Tamarin prover for security protocol verification. 
atphaskell
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning" 
hout
A noninteractive proof assistant using the Haskell type system 
logicclasses
Framework for propositional and first order logic, theorem proving 
obdd
pure Haskell implementation of reduced ordered binary decision diagrams 
structuralinduction
SII: Structural Induction Instantiator over any strictlypositive algebraic data type. 
g4ipprover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip 
tpdb
parser and prettyprinter for TPDB syntax (termination problem data base) 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Static code analysis for 29 languages.
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of Heyting Algebras or a related project?
README
Heyting Algebras
This package contains type classes and instances for many Heyting algebras which are in the Haskell ecosystem. It is build on top of lattices and freealgebras (to provide combinators for free Heyting algebras). The package also defines a type class for Boolean algebras and comes with many useful instances.
A note about notation: this package is based on
lattices, and both are using
notation and names common in lattice theory and logic. Where &&
becomes ∧
and is called meet
and 
is denoted by ∨
and is usually called
join
. The lattice
package provides \/
and /\
operators as well as type
classes for various flavors of posets and lattices.
A very good introduction to Heyting algebras can be found at
ncatlab. Heyting algebras
are the crux of intuitionistic
logic, which drops the
axiom of excluded middle. From categorical point of view, Heyting algebras are
posets (categories with at most one arrow between any objects), which are also
Cartesian closed (and finitely (co)complete). Note that this makes any
Heyting algebra a simply typed lambda calculus; hence one more incentive to
learn about them. For example currying holds in every Heyting algebra:
a => (b ⇒ c)
is equal to (a ∧ b) ⇒ c
The most important operation is implication (==>) :: HeytingAlgebra a => a >
a > a
(which we might also write as ⇒ in documentation). Every Boolean
algebra is a Heyting algebra via a ==> b = not a \/ b
(using the lattice
notation for or
). It is very handy in expression conditional logic.
Some examples of Heyting algebras:
Bool
is a Boolean algebra(Ord a, Bounded a) => a
; the implication is defined as: ifa ≤ b
thena ⇒ b = maxBound
, otherwisea ⇒ b = b
; e.g. integers with both±∞
(it can be represented byLevitated Int
. Note that it is not a Boolean algebra. The power set is a Boolean algebra, in Haskell it can be represented by
Set a
(one might need to requirea
to be finite though, otherwisenot (not empty)
might beundefined
rather thanempty
). It is a well known fact that every Boolean algebra is isomorphic to a power set. haskell type CounterExample a = Lifted (Op (Set a))
is a Heyting algebra; it is useful for gathering counter examples in a similar way thatProperty
fromQuickCheck
library does (put pure). This library provides some useful functions for this type, see theAlgebra.Heyting.Properties
and tests for example usage. * More generally every type(Ord k, Finite k, HeytingAlgebra v) => Map k a
is a Heyting algebra (though in general not a Boolean one).