Unbound.Generics.LocallyNameless.Kind.Example

Example of how to use `unbound-kind-generics`

Documentation

type Var t = Name (Expr t)

Variables stand for expressions

data Expr t where

Well-typed lambda expressions

Constructors

V :: Var t -> Expr t

Lam :: (Typeable a, Typeable b) => Bind (Var a) (Expr b) -> Expr (a -> b)

App :: Typeable a => Expr (a -> b) -> Expr a -> Expr b

Instances

GenericK (Expr t :: Type)

Defined in Unbound.Generics.LocallyNameless.Kind.Example

Associated Types

type RepK (Expr t) :: LoT k -> Type

Methods

fromK :: (Expr t :@@: x) -> RepK (Expr t) x

toK :: RepK (Expr t) x -> Expr t :@@: x

Show (Expr t)

Defined in Unbound.Generics.LocallyNameless.Kind.Example

Methods

showsPrec :: Int -> Expr t -> ShowS

show :: Expr t -> String

showList :: [Expr t] -> ShowS

Typeable t => Alpha (Expr t)

Defined in Unbound.Generics.LocallyNameless.Kind.Example

Methods

aeq' :: AlphaCtx -> Expr t -> Expr t -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Expr t -> f (Expr t)

close :: AlphaCtx -> NamePatFind -> Expr t -> Expr t

open :: AlphaCtx -> NthPatFind -> Expr t -> Expr t

isPat :: Expr t -> DisjointSet AnyName

isTerm :: Expr t -> All

isEmbed :: Expr t -> Bool

nthPatFind :: Expr t -> NthPatFind

namePatFind :: Expr t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Expr t -> Expr t

lfreshen' :: LFresh m => AlphaCtx -> Expr t -> (Expr t -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Expr t -> m (Expr t, Perm AnyName)

acompare' :: AlphaCtx -> Expr t -> Expr t -> Ordering

(Typeable small, Typeable big) => Subst (Expr small) (Expr big)

Defined in Unbound.Generics.LocallyNameless.Kind.Example

Methods

isvar :: Expr big -> Maybe (SubstName (Expr big) (Expr small))

isCoerceVar :: Expr big -> Maybe (SubstCoerce (Expr big) (Expr small))

subst :: Name (Expr small) -> Expr small -> Expr big -> Expr big

substs :: [(Name (Expr small), Expr small)] -> Expr big -> Expr big

GenericK Expr

Defined in Unbound.Generics.LocallyNameless.Kind.Example

Associated Types

type RepK Expr :: LoT k -> Type

Methods

fromK :: (Expr :@@: x) -> RepK Expr x

toK :: RepK Expr x -> Expr :@@: x

type RepK (Expr t :: Type)

Defined in Unbound.Generics.LocallyNameless.Kind.Example

type RepK (Expr t :: Type) = D1 (MetaData "Expr" "Unbound.Generics.LocallyNameless.Kind.Example" "unbound-kind-generics-0.2.1.0-LxW8gVDWHKNLqm6T4hUV14" False) (C1 (MetaCons "V" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field (Kon (Name (Expr t)) :: Atom Type Type))) :+: (C1 (MetaCons "Lam" PrefixI False) (Exists Type (Exists Type ((((Kon ((~~) t :: Type -> Constraint) :: Atom (Type -> Type -> Type) (Type -> Constraint)) :@: (((Kon ((->) :: Type -> Type -> Type) :: Atom (Type -> Type -> Type) (Type -> Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type) Type)) :@: (Var1 :: Atom (Type -> Type -> Type) Type))) :&: (((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type -> Type) (Type -> Constraint)) :@: (Var0 :: Atom (Type -> Type -> Type) Type)) :&: ((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type -> Type) (Type -> Constraint)) :@: (Var1 :: Atom (Type -> Type -> Type) Type)))) :=>: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field (((Kon Bind :: Atom (Type -> Type -> Type) (Type -> Type -> Type)) :@: ((Kon Name :: Atom (Type -> Type -> Type) (Type -> Type)) :@: ((Kon Expr :: Atom (Type -> Type -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type) Type)))) :@: ((Kon Expr :: Atom (Type -> Type -> Type) (Type -> Type)) :@: (Var1 :: Atom (Type -> Type -> Type) Type))))))) :+: C1 (MetaCons "App" PrefixI False) (Exists Type (((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type) (Type -> Constraint)) :@: (Var0 :: Atom (Type -> Type) Type)) :=>: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field ((Kon Expr :: Atom (Type -> Type) (Type -> Type)) :@: (((Kon ((->) :: Type -> Type -> Type) :: Atom (Type -> Type) (Type -> Type -> Type)) :@: (Var0 :: Atom (Type -> Type) Type)) :@: (Kon t :: Atom (Type -> Type) Type)))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field ((Kon Expr :: Atom (Type -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type) Type))))))))

type RepK Expr

Defined in Unbound.Generics.LocallyNameless.Kind.Example

type RepK Expr = D1 (MetaData "Expr" "Unbound.Generics.LocallyNameless.Kind.Example" "unbound-kind-generics-0.2.1.0-LxW8gVDWHKNLqm6T4hUV14" False) (C1 (MetaCons "V" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field ((Kon Name :: Atom (Type -> Type) (Type -> Type)) :@: ((Kon Expr :: Atom (Type -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type) Type))))) :+: (C1 (MetaCons "Lam" PrefixI False) (Exists Type (Exists Type (((((Kon ((~~) :: Type -> Type -> Constraint) :: Atom (Type -> Type -> Type -> Type) (Type -> Type -> Constraint)) :@: (Var2 :: Atom (Type -> Type -> Type -> Type) Type)) :@: (((Kon ((->) :: Type -> Type -> Type) :: Atom (Type -> Type -> Type -> Type) (Type -> Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :@: (Var1 :: Atom (Type -> Type -> Type -> Type) Type))) :&: (((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type -> Type -> Type) (Type -> Constraint)) :@: (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :&: ((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type -> Type -> Type) (Type -> Constraint)) :@: (Var1 :: Atom (Type -> Type -> Type -> Type) Type)))) :=>: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field (((Kon Bind :: Atom (Type -> Type -> Type -> Type) (Type -> Type -> Type)) :@: ((Kon Name :: Atom (Type -> Type -> Type -> Type) (Type -> Type)) :@: ((Kon Expr :: Atom (Type -> Type -> Type -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type -> Type) Type)))) :@: ((Kon Expr :: Atom (Type -> Type -> Type -> Type) (Type -> Type)) :@: (Var1 :: Atom (Type -> Type -> Type -> Type) Type))))))) :+: C1 (MetaCons "App" PrefixI False) (Exists Type (((Kon (Typeable :: Type -> Constraint) :: Atom (Type -> Type -> Type) (Type -> Constraint)) :@: (Var0 :: Atom (Type -> Type -> Type) Type)) :=>: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field ((Kon Expr :: Atom (Type -> Type -> Type) (Type -> Type)) :@: (((Kon ((->) :: Type -> Type -> Type) :: Atom (Type -> Type -> Type) (Type -> Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type) Type)) :@: (Var1 :: Atom (Type -> Type -> Type) Type)))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Field ((Kon Expr :: Atom (Type -> Type -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> Type) Type))))))))

eval :: Typeable t => Expr t -> FreshM (Expr t)

example :: forall a. Typeable a => Expr (a -> a)