heyting-algebras: Heyting and Boolean algebras

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


This package provides Heyting and Boolean operations together with various constructions of Heyting algebras.

[Skip to ReadMe]


Change logChangeLog.md
Dependenciesbase (>=4.9 && <4.13), containers (>=0.4.2 && <0.7), free-algebras (>=0.0.4 && <0.0.8), hashable (>= && <1.3), lattices (>=1.0 && <1.8), semiring-simple (>=1.0 && <1.2), tagged (>=0.8.5 && <0.9), universe-base (==1.0.*), unordered-containers (>= && <0.3) [details]
Copyright(c) 2018-2019 Marcin Szamotulski
AuthorMarcin Szamotulski
Source repositoryhead: git clone https://github.com/coot/heyting-algebras
UploadedSat Feb 16 10:38:44 UTC 2019 by coot




Maintainers' corner

For package maintainers and hackage trustees

Readme for heyting-algebras-

[back to package description]

Heyting Algebras

Maintainer: coot Travis Build Status

This package contains type classes and instances for many Heyting algebras which are in the Haskell eco-system. It is build on top of lattices and free-algebras (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: