Safe Haskell	Safe
Language	Haskell2010

Algebra.Heyting.Free

Synopsis

newtype FreeHeyting a = FreeHeyting {
- runFreeHeyting :: forall h. HeytingAlgebra h => (a -> h) -> h
}
atom :: a -> FreeHeyting a

Documentation

newtype FreeHeyting a Source #

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 Source #
Instance details 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 Source #
Instance details Defined in Algebra.Heyting.Free Methods fmap :: (a -> b) -> FreeHeyting a -> FreeHeyting b # (<$) :: a -> FreeHeyting b -> FreeHeyting a #
Applicative FreeHeyting Source #
Instance details 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 Source #
Instance details 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) Source #
Instance details Defined in Algebra.Heyting.Free Methods (\/) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a # join :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a #
MeetSemiLattice (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free Methods (/\) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a # meet :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a #
Lattice (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free
BoundedJoinSemiLattice (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free Methods bottom :: FreeHeyting a #
BoundedMeetSemiLattice (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free Methods top :: FreeHeyting a #
BoundedLattice (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free
HeytingAlgebra (FreeHeyting a) Source #
Instance details Defined in Algebra.Heyting.Free Methods (==>) :: FreeHeyting a -> FreeHeyting a -> FreeHeyting a Source # not :: FreeHeyting a -> FreeHeyting a Source #
type AlgebraType FreeHeyting (a :: Type) Source #
Instance details Defined in Algebra.Heyting.Free type AlgebraType FreeHeyting (a :: Type) = HeytingAlgebra a
type AlgebraType0 FreeHeyting (a :: Type) Source #
Instance details Defined in Algebra.Heyting.Free type AlgebraType0 FreeHeyting (a :: Type) = ()

atom :: a -> FreeHeyting a Source #

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