lattices-2.1: Fine-grained library for constructing and manipulating lattices
Safe Haskell Safe
Language Haskell2010

Algebra.Heyting.Free

Synopsis

Documentation

data Free a Source #

Free Heyting algebra.

Note: Eq and PartialOrd instances aren't structural. 

>>> Top == (Var 'x' ==> Var 'x')
True

>>> Var 'x' == Var 'y'
False

You can test for taulogogies: 

>>> leq Top $ (Var 'A' /\ Var 'B' ==> Var 'C') <=>  (Var 'A' ==> Var 'B' ==> Var 'C')
True

>>> leq Top $ (Var 'A' /\ neg (Var 'A')) <=> Bottom
True

>>> leq Top $ (Var 'A' \/ neg (Var 'A')) <=> Top
False

Constructors

Var a
Bottom
Top
( Free a) :/\: ( Free a) infixr 6
( Free a) :\/: ( Free a) infixr 5
( Free a) :=>: ( Free a) infixr 4

Instances

Instances details
Monad Free Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

(>>=) :: Free a -> (a -> Free b) -> Free b Source #

(>>) :: Free a -> Free b -> Free b Source #

return :: a -> Free a Source #

Functor Free Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

fmap :: (a -> b) -> Free a -> Free b Source #

(<$) :: a -> Free b -> Free a Source #

Applicative Free Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

pure :: a -> Free a Source #

(<*>) :: Free (a -> b) -> Free a -> Free b Source #

liftA2 :: (a -> b -> c) -> Free a -> Free b -> Free c Source #

(*>) :: Free a -> Free b -> Free b Source #

(<*) :: Free a -> Free b -> Free a Source #

Foldable Free Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

fold :: Monoid m => Free m -> m Source #

foldMap :: Monoid m => (a -> m) -> Free a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Free a -> m Source #

foldr :: (a -> b -> b) -> b -> Free a -> b Source #

foldr' :: (a -> b -> b) -> b -> Free a -> b Source #

foldl :: (b -> a -> b) -> b -> Free a -> b Source #

foldl' :: (b -> a -> b) -> b -> Free a -> b Source #

foldr1 :: (a -> a -> a) -> Free a -> a Source #

foldl1 :: (a -> a -> a) -> Free a -> a Source #

toList :: Free a -> [a] Source #

null :: Free a -> Bool Source #

length :: Free a -> Int Source #

elem :: Eq a => a -> Free a -> Bool Source #

maximum :: Ord a => Free a -> a Source #

minimum :: Ord a => Free a -> a Source #

sum :: Num a => Free a -> a Source #

product :: Num a => Free a -> a Source #

Traversable Free Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

traverse :: Applicative f => (a -> f b) -> Free a -> f ( Free b) Source #

sequenceA :: Applicative f => Free (f a) -> f ( Free a) Source #

mapM :: Monad m => (a -> m b) -> Free a -> m ( Free b) Source #

sequence :: Monad m => Free (m a) -> m ( Free a) Source #

Ord a => Eq ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

(==) :: Free a -> Free a -> Bool Source #

(/=) :: Free a -> Free a -> Bool Source #

Data a => Data ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

gfoldl :: ( forall d b. Data d => c (d -> b) -> d -> c b) -> ( forall g. g -> c g) -> Free a -> c ( Free a) Source #

gunfold :: ( forall b r. Data b => c (b -> r) -> c r) -> ( forall r. r -> c r) -> Constr -> c ( Free a) Source #

toConstr :: Free a -> Constr Source #

dataTypeOf :: Free a -> DataType Source #

dataCast1 :: Typeable t => ( forall d. Data d => c (t d)) -> Maybe (c ( Free a)) Source #

dataCast2 :: Typeable t => ( forall d e. ( Data d, Data e) => c (t d e)) -> Maybe (c ( Free a)) Source #

gmapT :: ( forall b. Data b => b -> b) -> Free a -> Free a Source #

gmapQl :: (r -> r' -> r) -> r -> ( forall d. Data d => d -> r') -> Free a -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> ( forall d. Data d => d -> r') -> Free a -> r Source #

gmapQ :: ( forall d. Data d => d -> u) -> Free a -> [u] Source #

gmapQi :: Int -> ( forall d. Data d => d -> u) -> Free a -> u Source #

gmapM :: Monad m => ( forall d. Data d => d -> m d) -> Free a -> m ( Free a) Source #

gmapMp :: MonadPlus m => ( forall d. Data d => d -> m d) -> Free a -> m ( Free a) Source #

gmapMo :: MonadPlus m => ( forall d. Data d => d -> m d) -> Free a -> m ( Free a) Source #

Show a => Show ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

showsPrec :: Int -> Free a -> ShowS Source #

show :: Free a -> String Source #

showList :: [ Free a] -> ShowS Source #

Generic ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Associated Types

type Rep ( Free a) :: Type -> Type Source #

Methods

from :: Free a -> Rep ( Free a) x Source #

to :: Rep ( Free a) x -> Free a Source #

Arbitrary a => Arbitrary ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

arbitrary :: Gen ( Free a) Source #

shrink :: Free a -> [ Free a] Source #

Ord a => PartialOrd ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

leq :: Free a -> Free a -> Bool Source #

comparable :: Free a -> Free a -> Bool Source #

BoundedMeetSemiLattice ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

top :: Free a Source #

BoundedJoinSemiLattice ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

bottom :: Free a Source #

Lattice ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

(\/) :: Free a -> Free a -> Free a Source #

(/\) :: Free a -> Free a -> Free a Source #

Heyting ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

Methods

(==>) :: Free a -> Free a -> Free a Source #

neg :: Free a -> Free a Source #

(<=>) :: Free a -> Free a -> Free a Source #

Generic1 Free Source #
Instance details

Defined in Algebra.Heyting.Free

Associated Types

type Rep1 Free :: k -> Type Source #

Methods

from1 :: forall (a :: k). Free a -> Rep1 Free a Source #

to1 :: forall (a :: k). Rep1 Free a -> Free a Source #

type Rep ( Free a) Source #
Instance details

Defined in Algebra.Heyting.Free

type Rep ( Free a) = D1 (' MetaData "Free" "Algebra.Heyting.Free" "lattices-2.1-Aj77JapAM1ZIiO74F5gL5i" ' False ) (( C1 (' MetaCons "Var" ' PrefixI ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 a)) :+: ( C1 (' MetaCons "Bottom" ' PrefixI ' False ) ( U1 :: Type -> Type ) :+: C1 (' MetaCons "Top" ' PrefixI ' False ) ( U1 :: Type -> Type ))) :+: ( C1 (' MetaCons ":/\\:" (' InfixI ' RightAssociative 6) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a)) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a))) :+: ( C1 (' MetaCons ":\\/:" (' InfixI ' RightAssociative 5) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a)) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a))) :+: C1 (' MetaCons ":=>:" (' InfixI ' RightAssociative 4) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a)) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Free a))))))
type Rep1 Free Source #
Instance details

Defined in Algebra.Heyting.Free

type Rep1 Free = D1 (' MetaData "Free" "Algebra.Heyting.Free" "lattices-2.1-Aj77JapAM1ZIiO74F5gL5i" ' False ) (( C1 (' MetaCons "Var" ' PrefixI ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) Par1 ) :+: ( C1 (' MetaCons "Bottom" ' PrefixI ' False ) ( U1 :: Type -> Type ) :+: C1 (' MetaCons "Top" ' PrefixI ' False ) ( U1 :: Type -> Type ))) :+: ( C1 (' MetaCons ":/\\:" (' InfixI ' RightAssociative 6) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free ) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free )) :+: ( C1 (' MetaCons ":\\/:" (' InfixI ' RightAssociative 5) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free ) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free )) :+: C1 (' MetaCons ":=>:" (' InfixI ' RightAssociative 4) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free ) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Free )))))

liftFree :: a -> Free a Source #

lowerFree :: Heyting b => (a -> b) -> Free a -> b Source #

retractFree :: Heyting a => Free a -> a Source #

substFree :: Free a -> (a -> Free b) -> Free b Source #

toExpr :: Free a -> Expr a Source #