Algebra.Heyting.Free

Documentation

newtype FreeHeyting a

Free Heyting algebra. FreeAlgebra instance provides all the usual combinators for a free algebra.

The graph of free Heyting algebra with one generator/atom, i.e. FreeHeyting ().

Constructors

FreeHeyting

Fields

• runFreeHeyting :: forall h. HeytingAlgebra h => (a -> h) -> h

Instances

Monad FreeHeyting

Defined in Algebra.Heyting.Free

Methods

(>>=) :: FreeHeyting a -> (a -> FreeHeyting b) -> FreeHeyting b

(>>) :: FreeHeyting a -> FreeHeyting b -> FreeHeyting b

return :: a -> FreeHeyting a

fail :: String -> FreeHeyting a

Functor FreeHeyting

Defined in Algebra.Heyting.Free

Methods

fmap :: (a -> b) -> FreeHeyting a -> FreeHeyting b

(<$) :: a -> FreeHeyting b -> FreeHeyting a

Applicative FreeHeyting

Defined in Algebra.Heyting.Free

Methods

pure :: a -> FreeHeyting a

(<*>) :: FreeHeyting (a -> b) -> FreeHeyting a -> FreeHeyting b

liftA2 :: (a -> b -> c) -> FreeHeyting a -> FreeHeyting b -> FreeHeyting c

(*>) :: FreeHeyting a -> FreeHeyting b -> FreeHeyting b

(<*) :: FreeHeyting a -> FreeHeyting b -> FreeHeyting a

FreeAlgebra FreeHeyting

Defined in Algebra.Heyting.Free

Methods

returnFree :: a -> FreeHeyting a

foldMapFree :: (AlgebraType FreeHeyting d, AlgebraType0 FreeHeyting a) => (a -> d) -> FreeHeyting a -> d

codom :: AlgebraType0 FreeHeyting a => Proof (AlgebraType FreeHeyting (FreeHeyting a)) (FreeHeyting a)

forget :: AlgebraType FreeHeyting a => Proof (AlgebraType0 FreeHeyting a) (FreeHeyting a)

JoinSemiLattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

(\/) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

join :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

MeetSemiLattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

(/\) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

meet :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

Lattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

BoundedJoinSemiLattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

bottom :: FreeHeyting a

BoundedMeetSemiLattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

top :: FreeHeyting a

BoundedLattice (FreeHeyting a)

Defined in Algebra.Heyting.Free

HeytingAlgebra (FreeHeyting a)

Defined in Algebra.Heyting.Free

Methods

(==>) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a

not :: FreeHeyting a -> FreeHeyting a

type AlgebraType FreeHeyting (a :: Type)

Defined in Algebra.Heyting.Free

type AlgebraType FreeHeyting (a :: Type) = HeytingAlgebra a

type AlgebraType0 FreeHeyting (a :: Type)

Defined in Algebra.Heyting.Free

type AlgebraType0 FreeHeyting (a :: Type) = ()

atom :: a -> FreeHeyting a

Construct an atom of the FreeHeyting lattice (in the laguage of free algebra, it is called a generator, e.g. atom = returnFree).