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

Stability | experimental |

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

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

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

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