generics-mrsop-2.0.0: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellNone




Provide a generic alpha equality decider for the lambda calculus.



data Term Source #

Standard Lambda Calculus.


Var String 
Abs String Term 
App Term Term 

type FamTerm = '[Term] Source #

type CodesTerm = '['['[K KString], '[K KString, I Z], '[I Z, I Z]]] Source #

pattern App_ :: phi Z -> phi Z -> View kon phi (Lkup Z CodesTerm) Source #

pattern Abs_ :: kon KString -> phi Z -> View kon phi (Lkup Z CodesTerm) Source #

pattern Var_ :: kon KString -> View kon phi (Lkup Z CodesTerm) Source #

pattern IdxTerm :: forall (a :: Nat). () => (~#) Nat Nat a Z => SNat a Source #

The alpha-eq monad

We will use an abstract monad for keeping track of scopes and name equivalences

class Monad m => MonadAlphaEq m where Source #

Interface needed for deciding alpha equivalence.

Minimal complete definition

onNewScope, addRule, (=~=)


onNewScope :: m a -> m a Source #

Runs a computation under a new scope.

addRule :: String -> String -> m () Source #

Registers a name equivalence under the current scope.

(=~=) :: String -> String -> m Bool Source #

Checks for a name equivalence under all scopes.


MonadAlphaEq (State [[(String, String)]]) Source #

One of the simplest monads that implement MonadAlphaEq

onHead :: (a -> a) -> [a] -> [a] Source #

onScope :: String -> String -> [[(String, String)]] -> Bool Source #

Given a list of scopes, which consist in a list of pairs each, checks whether or not two names are equivalent.

runAlpha :: State [[(String, String)]] a -> a Source #

Runs a computation.

Alpha equivalence for Lambda terms

alphaEq :: Term -> Term -> Bool Source #

Decides whether or not two terms are alpha equivalent.


Orphan instances