module Main where



data Term =
  Variable String |
  Abstraction String Type Term |
  Application Term Term |
  Record [(Label, Term)] |
  Projection Term Label |
  Number Integer
    deriving (Show, Eq, Ord)

type Label = String

data Type =
  Top |
  FunctionType Type Type |
  RecordType [(Label, Type)] |
  Natural
    deriving (Show, Eq, Ord)


type Context = [(String, Type)]


typeCheck :: Context -> Term -> Type

subType :: Type -> Type -> Bool

main :: IO ()
main = do
  print (typeCheck [] term)

term = Application (Abstraction "r" (RecordType [("x", Natural)]) (Projection (Variable "r") "x")) (Record [("x", Number 0), ("y", Number 1)])