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.

[maintain] [Publish]

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

[Skip to Readme]


Change log ChangeLog.md
Dependencies base (>=4.9 && <4.16), containers (>=0.4.2 && <0.7), free-algebras (>= && <, hashable (>= && <1.4), lattices (>=2.0 && <2.1), semiring-simple (>=1.0 && <1.2), tagged (>=0.8.5 && <0.9), universe-base (>=1.0 && <1.2), unordered-containers (>= && <0.3) [details]
License BSD-3-Clause
Copyright (c) 2018-2021 Marcin Szamotulski
Author Marcin Szamotulski
Maintainer profunctor@pm.me
Category Math
Source repo head: git clone https://github.com/coot/heyting-algebras
Uploaded by coot at 2021-03-27T13:34:22Z



Maintainer's Corner

For package maintainers and hackage trustees

Readme for heyting-algebras-

[back to package description]

Heyting Algebras

Maintainer: coot POSIX

This package now extends lattices by providing more 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: