I've been implementing mini languages that fall into each corner of the Lambda Cube. My main reference for this has been Types and Programming Languages.
The latest one I finished is System Omega. I only included Bools and Unit as base types:
data Term = Var String | Abs String Type Term | App Term Term | Unit | T | F | If Term Term Term deriving Show infixr 0 :-> data Type = Type :-> Type | TVar String | TyAbs String Kind Type | TyApp Type Type | UnitT | BoolT deriving (Show, Eq) infixr 0 :=> data Kind = Star | Kind :=> Kind deriving (Show, Eq)
kindcheck and type normalization functions appear to be working as expected:
> let hkt = TyAbs "F" (Star :=> Star) (TyApp (TVar "F") BoolT) > pretty <$> runTypecheckM (kindcheck hkt) Right "((* -> *) -> *)" > idT TyAbs "X" Star (TVar "X") > pretty <$> runTypecheckM (kindcheck idT) Right "(* -> *)" > unify  (TyApp idT BoolT) BoolT True
However I am unsure how to construct actual
Terms that would test my implementation of Type Operators. All of the examples in TAPL are actually System FOmega examples which also utilize polymorphism. What are some sample terms in System Omega which I could use to test my typechecker and evaluator?