Well Typed Interpreter using generic structures of context and environment.

Interp.idr

||| You need latest version of my containers package:
|||     https://github.com/jfdm/idris-containers/
module Interp

import Data.DList
import Data.DeBruijn


data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Integer
interpTy TyBool      = Bool
interpTy (TyFun A T) = interpTy A -> interpTy T


data Expr : (ctxt : List Ty) -> (t : Ty) -> Type where
    Var : Index Ty ctxt t -> Expr ctxt t

    Val : (x : Integer) -> Expr ctxt TyInt

    Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)

    App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t

    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr ctxt a -> Expr ctxt b -> Expr ctxt c
    If  : Expr ctxt TyBool ->
          Lazy (Expr ctxt a) ->
          Lazy (Expr ctxt a) -> Expr ctxt a

interp : Env Ty interpTy ctxt -> Expr ctxt t -> interpTy t
interp env (Var i)     = read i env
interp env (Val x)     = x
interp env (Lam sc)    = \x => interp (x :: env) sc
interp env (App f s)   = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e)  = if interp env x then interp env t
                                         else interp env e

fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var First) (Val 0))
               (Val 1)
               (Op (*) (App fact (Op (-) (Var First) (Val 1)))
                       (Var First)))

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          printLn (interp [] fact (cast x))