Type-safe Interpreter in Idris

interp.idr

tyFun : Set -> Set -> Set;
tyFun A T = A -> T;

using (G:Vect Set n) {

  data Expr : Vect Set n -> Set -> Set where
    Var : (i:Fin n) -> Expr G (vlookup i G)
  | Val : T -> Expr G T
  | Lam : Expr (A::G) T -> Expr G (tyFun A T) -- using `A -> T` directly fails
  | App : Expr G (A -> T) -> Expr G A -> Expr G T
  | If  : Expr G Bool -> Expr G A -> Expr G A -> Expr G A
  | Op  : (Int -> Int -> C) -> Expr G Int -> Expr G Int -> Expr G C;

  data Env : Vect Set n -> Set where
    Empty  : Env VNil
  | Extend : T -> Env G -> Env (T::G);

  envLookup : (i:Fin n) -> Env G -> vlookup i G;
  envLookup fO     (Extend t env) = t;
  envLookup (fS i) (Extend t env) = envLookup i env;

  interp : Env G -> Expr G T -> T;
  interp env (Var i)     = envLookup i env;
  interp env (Val x)     = x;
  interp env (Lam scope) = \x => interp (Extend x env) scope;
  interp env (App f a)   = interp env f (interp env a);
  interp env (If v t e)  = if (interp env v) then (interp env t)
                                             else (interp env e);
  interp env (Op op l r) = op (interp env l) (interp env r);

}