Portability | non-portable |
---|---|

Stability | experimental |

Maintainer | sweirich@cis.upenn.edu |

- module Generics.RepLib.R
- module Generics.RepLib.R1
- module Generics.RepLib.PreludeReps
- module Generics.RepLib.Derive
- module Generics.RepLib.RepAux
- module Generics.RepLib.SYB.Aliases
- module Generics.RepLib.SYB.Schemes
- module Generics.RepLib.Lib
- module Generics.RepLib.PreludeLib
- data a :=: b where
- class EqT f where

# Basic infrastructure

## Basic Representations of types

module Generics.RepLib.R

## Parameterized Representations of types

module Generics.RepLib.R1

## Representations of Prelude Types

module Generics.RepLib.PreludeReps

## Template Haskell for deriving representations

module Generics.RepLib.Derive

# Libraries for defining Generic Operations

## Library code for defining generic operations

module Generics.RepLib.RepAux

## Scrap your boilerplate operations

module Generics.RepLib.SYB.Aliases

module Generics.RepLib.SYB.Schemes

# Generic Utilities and Applications

## Library of generic operations

module Generics.RepLib.Lib

## Derivable type classes written as generic operations

module Generics.RepLib.PreludeLib

data a :=: b where

Type equality. A value of `a :=: b`

is a proof that types `a`

and
`b`

are equal. By pattern matching on `Refl`

this fact is
introduced to the type checker.

Category :=: | |

(Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => Rep1 ctx (:=: a b) | |

EqT (:=: a) | |

Read (:=: a a) | We can only read values if the result is |

Show (:=: a b) | Any value is just shown as Refl, but this cannot be derived for a GADT, so it is defined here manually. |

(Rep a, Rep b) => Rep (:=: a b) |