heyting-algebras: Heyting and Boolean algebras

[ library, logic, math ] [ Propose Tags ]

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


[Skip to Readme]
Versions 0.0.1.0, 0.0.1.1, 0.0.1.2 (info)
Change log ChangeLog.md
Dependencies base (>=4.9 && <4.13), containers (>=0.4.2 && <0.7), free-algebras (>=0.0.4 && <0.0.6), hashable (>=1.2.6.1 && <1.3), lattices (>=1.0 && <1.11), QuickCheck (>=2.10 && <2.13), tagged (>=0.8.5 && <0.9), universe-base (==1.0.*), unordered-containers (>=0.2.6.0 && <0.3) [details]
License MPL-2.0
Copyright (c) 2018 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 Fri Oct 5 23:11:37 UTC 2018
Distributions NixOS:0.0.1.2
Downloads 75 total (75 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI

Modules

[Index]

Flags

NameDescriptionDefaultType
export-properties

Export quickcheck properties from library; this adds QuickCheck as a dependency.

EnabledAutomatic

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for heyting-algebras-0.0.1.2

[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 a handful of instances.

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 exluded 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.

The most important operation is implication (==>) :: HeytingAlgebra a => a -> a -> a; since 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 basic examples of Heyting algebras:

  • Bool is a Boolean algebra
  • (Ord a, Bounded a) => a; the implication is defined as: if a ≤ b then a ⇒ b = maxBound; otherwise a ⇒ b = b; e.g. integers with both ±∞ (it can be represented by Levitated Int. This type 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 require a to be finite though, otherwise not (not empty) might be undefined rather than empty).
  • More generally every type (Ord k, Finite k, HeytingAlgebra v) => Map k a is a Heyting algebra (though in general not a Boolean one).