Safe Haskell	Safe-Inferred
Language	Haskell2010

Unbound.Generics.LocallyNameless.Kind.Example

Description

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

Synopsis

type Var t = Name (Expr t)
data Expr t where
- 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
eval :: Typeable t => Expr t -> FreshM (Expr t)
example :: forall a. Typeable a => Expr (a -> a)

Documentation

type Var t = Name (Expr t) Source #

Variables stand for expressions

data Expr t where Source #

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

Instances details

GenericK (Expr t :: Type) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Kind.Example Associated Types type RepK (Expr t) :: LoT k -> Type # Methods fromK :: forall (x :: LoT k). (Expr t :@@: x) -> RepK (Expr t) x # toK :: forall (x :: LoT k). RepK (Expr t) x -> Expr t :@@: x #
Show (Expr t) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 # substBvs :: AlphaCtx -> [Expr small] -> Expr big -> Expr big #
GenericK Expr Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Kind.Example Associated Types type RepK Expr :: LoT k -> Type # Methods fromK :: forall (x :: LoT k). (Expr :@@: x) -> RepK Expr x # toK :: forall (x :: LoT k). RepK Expr x -> Expr :@@: x #
type RepK (Expr t :: Type) Source #
Instance details 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.1-6CD7uiK6fbPLv9WZrEOzxW" '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 LiftedRep -> TYPE LiftedRep -> Type) (Type -> Constraint)) :@: ((('Kon (->) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> TYPE LiftedRep -> Type)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :@: (Var1 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep)))) :&: ((('Kon (Typeable :: TYPE LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :&: (('Kon (Typeable :: TYPE LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var1 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))))) :=>: 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 LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var0 :: Atom (TYPE LiftedRep -> Type) (TYPE LiftedRep))) :=>: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon Expr :: Atom (TYPE LiftedRep -> Type) (Type -> Type)) :@: ((('Kon (->) :: Atom (TYPE LiftedRep -> Type) (TYPE LiftedRep -> TYPE LiftedRep -> Type)) :@: (Var0 :: Atom (TYPE LiftedRep -> Type) (TYPE LiftedRep))) :@: ('Kon t :: Atom (TYPE LiftedRep -> 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 Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Kind.Example type RepK Expr = D1 ('MetaData "Expr" "Unbound.Generics.LocallyNameless.Kind.Example" "unbound-kind-generics-0.2.1.1-6CD7uiK6fbPLv9WZrEOzxW" '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 LiftedRep -> Type -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Type -> Constraint)) :@: (Var2 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :@: ((('Kon (->) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> TYPE LiftedRep -> Type)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :@: (Var1 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep)))) :&: ((('Kon (Typeable :: TYPE LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :&: (('Kon (Typeable :: TYPE LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var1 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))))) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon Bind :: Atom (Type -> Type -> TYPE LiftedRep -> Type) (Type -> Type -> Type)) :@: (('Kon Name :: Atom (Type -> Type -> TYPE LiftedRep -> Type) (Type -> Type)) :@: (('Kon Expr :: Atom (Type -> Type -> TYPE LiftedRep -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> Type -> TYPE LiftedRep -> Type) Type)))) :@: (('Kon Expr :: Atom (Type -> Type -> TYPE LiftedRep -> Type) (Type -> Type)) :@: (Var1 :: Atom (Type -> Type -> TYPE LiftedRep -> Type) Type))))))) :+: C1 ('MetaCons "App" 'PrefixI 'False) (Exists Type ((('Kon (Typeable :: TYPE LiftedRep -> Constraint) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> Constraint)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :=>: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon Expr :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (Type -> Type)) :@: ((('Kon (->) :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep -> TYPE LiftedRep -> Type)) :@: (Var0 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))) :@: (Var1 :: Atom (TYPE LiftedRep -> TYPE LiftedRep -> Type) (TYPE LiftedRep))))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon Expr :: Atom (Type -> TYPE LiftedRep -> Type) (Type -> Type)) :@: (Var0 :: Atom (Type -> TYPE LiftedRep -> Type) Type))))))))

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

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