unbound-generics-0.2: Support for programming with names and binders using GHC Generics

Copyright(c) 2014, Aleksey Kliger
LicenseBSD3 (See LICENSE)
MaintainerAleksey Kliger
Safe HaskellNone



The pattern Rec p binds the names in p like p itself would, but additionally, the names in p are scope over p.

The term TRec p is shorthand for Bind (Rec p) ()



data Rec p Source

If p is a pattern type, then Rec p is also a pattern type, which is recursive in the sense that p may bind names in terms embedded within itself. Useful for encoding e.g. lectrec and Agda's dot notation.


Subst c p => Subst c (Rec p) 
Eq p => Eq (Rec p) 
Show a => Show (Rec a) 
Generic (Rec p) 
NFData p => NFData (Rec p) 
Alpha p => Alpha (Rec p) 
type Rep (Rec p) 

rec :: Alpha p => p -> Rec p Source

Constructor for recursive patterns.

unrec :: Alpha p => Rec p -> p Source

Destructor for recursive patterns.

newtype TRec p Source

TRec is a standalone variant of Rec: the only difference is that whereas Rec p is a pattern type, TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Note that TRec corresponds to Pottier's abstraction construct from alpha-Caml. In this context, Embed t corresponds to alpha-Caml's inner t, and Shift (Embed t) corresponds to alpha-Caml's outer t.


TRec (Bind (Rec p) ()) 


(Alpha p, Subst c p) => Subst c (TRec p) 
Show a => Show (TRec a) 
Generic (TRec p) 
Alpha p => Alpha (TRec p) 
type Rep (TRec p)