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
Phantom type that signals that a Cxt
might contain holes.
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.