Documentation

>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> :set -XTypeOperators
>>> :set -XFlexibleContexts
>>> :set -XTypeFamilies
>>> :set -XPatternSynonyms
>>> :set -XDeriveFunctor
>>> :set -XGADTs
>>> :set -XPolyKinds
>>> :set -XPartialTypeSignatures
>>> 
>>> :{
>>> data LamF (ast :: Type -> Type) t where
>>> LamF :: ( ast a -> ast b ) -> LamF ast ( a -> b )
>>> 
>>> data AppF ast t where
>>> AppF :: ast ( a -> b ) -> ast a -> AppF ast b
>>> 
>>> data VarF ast t where
>>> VarF :: String -> VarF ast Int
>>> 
>>> type AST a = EGADT '[LamF,AppF,VarF] a
>>> 
>>> :}

>>> let y = VF @(AST Int) (VarF "a")
>>> :t y
y :: EGADT '[LamF, AppF, VarF] Int

>>> :{
>>> case y of
>>> VF (VarF x) -> print x
>>> _           -> putStrLn "Not a VarF"
>>> :}
"a"

>>> :{
>>> f :: AST Int -> AST Int
>>> f (VF (VarF x)) = VF (VarF "zz")
>>> f _             = error "Unhandled case"
>>> :}

>>> let z = VF (AppF (VF (LamF f)) (VF (VarF "a")))
>>> :t z
z :: EGADT '[LamF, AppF, VarF] Int