0
$\begingroup$

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)

My 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?

$\endgroup$
  • 1
    $\begingroup$ For example: \(f : Bool -> Bool) (x : (\(t : *). t) Bool). f x $\endgroup$ – Labbekak Mar 10 at 6:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.