Documentation

>>> :seti -XDataKinds >>> :seti -XTypeApplications >>> :seti -XTypeOperators >>> :seti -XFlexibleContexts >>> :seti -XTypeFamilies >>> :seti -XPatternSynonyms >>> :seti -XDeriveFunctor >>> :seti -XGADTs >>> :seti -XPolyKinds >>> :seti -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