Bound.Term

Documentation

substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a

substitute a p w replaces the free variable a with p in w.

>>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]

substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a

substituteVar a b w replaces a free variable a with another free variable b in w.

>>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
["Bob","Bob","Charlie"]

isClosed :: Foldable f => f a -> Bool

A closed term has no free variables.

>>> isClosed []
True

>>> isClosed [1,2,3]
False

closed :: Traversable f => f a -> Maybe (f b)

If a term has no free variables, you can freely change the type of free variables it is parameterized on.

>>> closed [12]
Nothing

>>> closed ""
Just []

>>> :t closed ""
closed "" :: Maybe [b]