Portability | non-portable (GHC Extensions) |
---|---|

Stability | experimental |

Maintainer | Tom Hvitved <hvitved@diku.dk> |

Safe Haskell | None |

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

- data Cxt where
- data Hole
- data NoHole
- newtype Term f = Term {}
- type Trm f a = Cxt NoHole f a ()
- type Context = Cxt Hole
- simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
- toCxt :: Difunctor f => Trm f a -> Cxt h f a b
- cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c
- class ParamFunctor m where

# Documentation

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.Difunctor. The third parameter is the type of parameters, and the fourth parameter is the type of holes.

EqD f => EqD (Cxt h f) | From an |

OrdD f => OrdD (Cxt h f) | From an |

(Difunctor f, ShowD f) => ShowD (Cxt h f) | From an |

(EqD f, PEq a) => PEq (Cxt h f Name a) | |

(OrdD f, POrd a) => POrd (Cxt h f Name a) |

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

cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a cSource

This combinator maps a function over a context by applying the function to each hole.

class ParamFunctor m whereSource

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".