Copyright | (c) 2010-2011 Patrick Bahr, Tom Hvitved |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | None |
Language | Haskell98 |
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
data Cxt :: * -> (* -> *) -> * -> * where Source
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) | |
Functor f => Applicative (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) | |
(Functor f, ShowF f) => ShowF (Cxt h f) | |
(ArbitraryF f, Arbitrary a) => Arbitrary (Context f a) | This lifts instances of |
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) | |
Functor f => Applicative (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 a Source
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.