Typed Lambda Calculus

tlc.v

Require Import List.

Inductive Error : Set :=
  | NotImplemented : Error
  | NotDeclared : Error
  | NotApplicable : Error
  | NotExpectedType : Error
  | SomethingWrong : Error
.

Inductive LType : Set :=
  | ErrorType : Error -> LType
  | BaseType : nat -> LType
  | FuncType : LType -> LType -> LType
.

Inductive Var : Set :=
  | VarOf : nat -> Var
.

Inductive Decl : Set :=
  | DeclOf : Var -> LType -> Decl
.

Inductive Term : Set :=
  | VarTerm : Var -> Term
  | ApplyTerm : Term -> Term -> Term
  | AbstTerm : Decl -> Term -> Term
.

Definition EqualVar (x y: Var) : bool :=
  match (x, y) with
    | (VarOf n, VarOf m) => Nat.eqb n m
  end
.

Fixpoint EqualType (x y: LType) : bool :=
  match (x, y) with
    | (BaseType n, BaseType m) => Nat.eqb n m
    | (FuncType F X, FuncType G Y) => andb (EqualType F G) (EqualType X Y)
    | (_, _) => false
  end
.

Fixpoint lookup (env: list Decl) (v: Var) : LType :=
  match env with
    | head :: tail => (
      match head with
        | DeclOf u T => (
          if (EqualVar u v)
          then T
          else (lookup tail v)
        )
      end
    )
    | nil => ErrorType NotDeclared
  end
.

Fixpoint LCheck (env: list Decl) (t: Term) : LType :=
  match t with
    | VarTerm v => lookup env v
    | ApplyTerm f a => (
      match (LCheck env f) with
        | ErrorType e => ErrorType e
        | BaseType _ => ErrorType NotApplicable
        | FuncType X Y => (
          match X with
            | ErrorType e => ErrorType e
            | _ => (
              if (EqualType X (LCheck env a))
              then Y
              else ErrorType NotExpectedType
            )
          end
        )
      end
    )
    | AbstTerm (DeclOf dv dt) a => (
      FuncType dt (LCheck ((DeclOf dv dt) :: env) a)
    )
  end
.

(*
  
  Test Data
  
  Variables:
    x <-> VarOf 1
    y <-> VarOf 2
    z <-> VarOf 3
  Base Types:
    T <-> BaseType 1
    S <-> BaseType 2
  
  Test 1:
    Term:
      \x:T.\y:T->S.yx
    Environment:
      []
    Correct Answer:
      T->(T->S)->S
  
  Test 2:
    Term:
      (\x:T.\y:T->S.yx)z
    Environment:
      [z:T]
    Correct Answer:
      (T->S)->S
  
*)

Definition testenv1 : (list Decl) := nil.

Definition testterm1 : Term :=
  (AbstTerm
    (DeclOf
      (VarOf 1)
      (BaseType 1)
    )
    (AbstTerm
      (DeclOf
        (VarOf 2)
        (FuncType
          (BaseType 1)
          (BaseType 2)
        )
      )
      (ApplyTerm
        (VarTerm (VarOf 2))
        (VarTerm (VarOf 1))
      )
    )
  )
.

Eval compute in LCheck testenv1 testterm1.

Definition testenv2 : (list Decl) :=
  (DeclOf (VarOf 3) (BaseType 1)) ::
  nil
.

Definition testterm2 : Term :=
  (ApplyTerm
    testterm1
    (VarTerm (VarOf 3))
  )
.

Eval compute in LCheck testenv2 testterm2.