Copyright	(c) 2011 Patrick Bahr Tom Hvitved
License	BSD3
Maintainer	Tom Hvitved <[email protected]>
Stability	experimental
Portability	non-portable (GHC Extensions)
Safe Haskell	None
Language	Haskell98

Data.Comp.Param.Multi.Term

Description

This module defines the central notion of generalised parametrised terms and their generalisation to generalised parametrised contexts.

Synopsis

data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where
- In :: f a (Cxt h f a b) i -> Cxt h f a b i
- Hole :: b i -> Cxt Hole f a b i
- Var :: a i -> Cxt h f a b i
data Hole
data NoHole
newtype Term f i = Term {
- unTerm :: forall a. Trm f a i
}
type Trm f a = Cxt NoHole f a (K ())
type Context = Cxt Hole
simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b
hfmapCxt :: forall h f a b b'. HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'
hdimapMCxt :: forall h f a b b' m. (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')
class ParamFunctor m where

Documentation

data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where Source #

This data type represents contexts over a signature. Contexts are terms containing zero or more holes, and zero or more parameters. The first parameter is a phantom type indicating whether the context has holes. The second paramater is the signature of the context, in the form of a Data.Comp.Param.Multi.HDifunctor. The third parameter is the type of parameters, the fourth parameter is the type of holes, and the fifth parameter is the GADT type.

Constructors

In :: f a (Cxt h f a b) i -> Cxt h f a b i
Hole :: b i -> Cxt Hole f a b i
Var :: a i -> Cxt h f a b i

Instances

(HDifunctor f, ShowHD f) => ShowHD (Cxt h f) Source #	From an `ShowHD` higher-order difunctor an `ShowHD` instance of the corresponding term type can be derived.
Instance details Defined in Data.Comp.Param.Multi.Show Methods showHD :: Cxt h f Name (K (FreshM String)) i -> FreshM String Source #
EqHD f => EqHD (Cxt h f) Source #	From an `EqHD` difunctor an `Eq` instance of the corresponding term type can be derived.
Instance details Defined in Data.Comp.Param.Multi.Equality Methods eqHD :: PEq a => Cxt h f Name a i -> Cxt h f Name a j -> FreshM Bool Source #
OrdHD f => OrdHD (Cxt h f) Source #	From an `OrdHD` difunctor an `Ord` instance of the corresponding term type can be derived.
Instance details Defined in Data.Comp.Param.Multi.Ordering Methods compareHD :: POrd a => Cxt h f Name a i -> Cxt h f Name a j -> FreshM Ordering Source #
(EqHD f, PEq a) => PEq (Cxt h f Name a) Source #
Instance details Defined in Data.Comp.Param.Multi.Equality Methods peq :: Cxt h f Name a i -> Cxt h f Name a j -> FreshM Bool Source #
(OrdHD f, POrd a) => POrd (Cxt h f Name a) Source #
Instance details Defined in Data.Comp.Param.Multi.Ordering Methods pcompare :: Cxt h f Name a i -> Cxt h f Name a j -> FreshM Ordering Source #

data Hole Source #

Phantom type used to define Context.

data NoHole Source #

Phantom type used to define Term.

newtype Term f i Source #

A term is a context with no holes, where all occurrences of the contravariant parameter is fully parametric.

Constructors

Term
Fields unTerm :: forall a. Trm f a i

Instances

(HDifunctor f, EqHD f) => Eq (Term f i) #	Equality on terms.
Instance details Defined in Data.Comp.Param.Multi.Equality Methods (==) :: Term f i -> Term f i -> Bool # (/=) :: Term f i -> Term f i -> Bool #
(HDifunctor f, OrdHD f) => Ord (Term f i) #	Ordering of terms.
Instance details Defined in Data.Comp.Param.Multi.Ordering Methods compare :: Term f i -> Term f i -> Ordering # (<) :: Term f i -> Term f i -> Bool # (<=) :: Term f i -> Term f i -> Bool # (>) :: Term f i -> Term f i -> Bool # (>=) :: Term f i -> Term f i -> Bool # max :: Term f i -> Term f i -> Term f i # min :: Term f i -> Term f i -> Term f i #
(HDifunctor f, ShowHD f) => Show (Term f i) #	Printing of terms.
Instance details Defined in Data.Comp.Param.Multi.Show Methods showsPrec :: Int -> Term f i -> ShowS # show :: Term f i -> String # showList :: [Term f i] -> ShowS #

type Trm f a = Cxt NoHole f a (K ()) Source #

"Preterms" |

type Context = Cxt Hole Source #

A context may contain holes.

simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b Source #

Convert a difunctorial value into a context.

toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b Source #

hfmapCxt :: forall h f a b b'. HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b' Source #

This is an instance of hfmap for Cxt.

hdimapMCxt :: forall h f a b b' m. (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b') Source #

This is an instance of hdimapM for Cxt.

class ParamFunctor m where Source #

Monads for which embedded Trm values, which are parametric at top level, can be made into monadic Term values, i.e. "pushing the parametricity inwards".

Minimal complete definition

termM

Methods

termM :: (forall a. m (Trm f a i)) -> m (Term f i) Source #

Instances

ParamFunctor [] Source #
Instance details Defined in Data.Comp.Param.Multi.Term Methods termM :: (forall (a :: * -> *). [Trm f a i]) -> [Term f i] Source #
ParamFunctor Maybe Source #
Instance details Defined in Data.Comp.Param.Multi.Term Methods termM :: (forall (a :: * -> *). Maybe (Trm f a i)) -> Maybe (Term f i) Source #
ParamFunctor (Either a) Source #
Instance details Defined in Data.Comp.Param.Multi.Term Methods termM :: (forall (a0 :: * -> *). Either a (Trm f a0 i)) -> Either a (Term f i) Source #