RepLib-0.5.2: Generic programming library with representation types

Safe HaskellNone






Basic infrastructure

Basic Representations of types

Parameterized Representations of types

Representations of Prelude Types

Template Haskell for deriving representations

Libraries for defining Generic Operations

Library code for defining generic operations

Scrap your boilerplate operations

Generic Utilities and Applications

Library of generic operations

Derivable type classes written as generic operations

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.


Refl :: :=: a a 


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 a :=: a, not a :=: b since that is not true, in general. We just parse the string Refl, optionally surrounded with parentheses, and return Refl.

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) 

class EqT f where

A type class for constructing equality proofs. This is as close as we can get to decidable equality on types. Note that f must be a GADT to be able to define eqT.


eqT :: f a -> f b -> Maybe (:=: a b)


EqT R 
EqT (:=: a)