Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Patrick Bahr <paba@diku.dk> |
Safe Haskell | None |
This module defines the central notion of terms and its generalisation to contexts.
- data Cxt where
- data Hole
- data NoHole
- type Context = Cxt Hole
- type Term f = Cxt NoHole f ()
- type PTerm f = forall h a. Cxt h f a
- type Const f = f ()
- unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)
- simpCxt :: Functor f => f a -> Context f a
- toCxt :: Functor f => Term f -> Cxt h f a
- constTerm :: Functor f => Const f -> Term f
Documentation
This data type represents contexts over a signature. Contexts are
terms containing zero or more holes. The first type parameter is
supposed to be one of the phantom types Hole
and NoHole
. The
second parameter is the signature of the context. The third parameter
is the type of the holes.
Functor f => Monad (Context f) | |
ArbitraryF f => Arbitrary (Term f) | This lifts instances of |
ArbitraryF f => ArbitraryF (Context f) | This lifts instances of |
Functor f => Functor (Cxt h f) | |
Foldable f => Foldable (Cxt h f) | |
Traversable f => Traversable (Cxt h f) | |
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) | This lifts instances of |
(Functor f, ShowF f) => ShowF (Cxt h f) | |
EqF f => EqF (Cxt h f) | |
OrdF f => OrdF (Cxt h f) | |
(EqF f, Eq a) => Eq (Cxt h f a) | From an |
(OrdF f, Ord a) => Ord (Cxt h f a) | From an |
(Functor f, ShowF f, Show a) => Show (Cxt h f a) | |
(NFDataF f, NFData a) => NFData (Cxt h f a) |
Phantom type that signals that a Cxt
might contain holes.
Functor f => Monad (Context f) | |
ArbitraryF f => ArbitraryF (Context f) | This lifts instances of |
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) | This lifts instances of |
Phantom type that signals that a Cxt
does not contain holes.
ArbitraryF f => Arbitrary (Term f) | This lifts instances of |
type PTerm f = forall h a. Cxt h f aSource
Polymorphic definition of a term. This formulation is more
natural than Term
, it leads to impredicative types in some cases,
though.
unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)Source
This function unravels the given term at the topmost layer.